diff --git a/src/Doc/ROOT b/src/Doc/ROOT --- a/src/Doc/ROOT +++ b/src/Doc/ROOT @@ -1,517 +1,518 @@ chapter Doc session Classes (doc) in "Classes" = HOL + options [document_variants = "classes", quick_and_dirty] theories [document = false] Setup theories Classes document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files "build" "root.tex" "style.sty" session Codegen (doc) in "Codegen" = HOL + options [document_variants = "codegen", print_mode = "no_brackets,iff"] sessions "HOL-Library" theories [document = false] Setup theories Introduction Foundations Refinement Inductive_Predicate Evaluation Computations Adaptation Further document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files "build" "root.tex" "style.sty" session Corec (doc) in "Corec" = Datatypes + options [document_variants = "corec"] theories Corec document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files "build" "root.tex" "style.sty" session Datatypes (doc) in "Datatypes" = HOL + options [document_variants = "datatypes"] sessions "HOL-Library" theories [document = false] Setup theories Datatypes document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files "build" "root.tex" "style.sty" session Eisbach (doc) in "Eisbach" = HOL + options [document_variants = "eisbach", quick_and_dirty, print_mode = "no_brackets,iff", show_question_marks = false] sessions "HOL-Eisbach" theories [document = false] Base theories Preface Manual document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "ttbox.sty" "underscore.sty" "manual.bib" document_files "build" "root.tex" "style.sty" session Functions (doc) in "Functions" = HOL + options [document_variants = "functions", skip_proofs = false, quick_and_dirty] theories Functions document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files "build" "conclusion.tex" "intro.tex" "mathpartir.sty" "root.tex" "style.sty" session How_to_Prove_it (no_doc) in "How_to_Prove_it" = HOL + options [document_variants = "how_to_prove_it", show_question_marks = false] theories How_to_Prove_it document_files "root.tex" "root.bib" "prelude.tex" session Intro (doc) in "Intro" = Pure + options [document_variants = "intro"] document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "ttbox.sty" "manual.bib" document_files "advanced.tex" "build" "foundations.tex" "getting.tex" "root.tex" session Implementation (doc) in "Implementation" = HOL + options [document_variants = "implementation", quick_and_dirty] theories Eq Integration Isar Local_Theory "ML" Prelim Proof Syntax Tactic theories [parallel_proofs = 0] Logic document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "ttbox.sty" "underscore.sty" "manual.bib" document_files "build" "root.tex" "style.sty" session Isar_Ref (doc) in "Isar_Ref" = HOL + options [document_variants = "isar-ref", quick_and_dirty, thy_output_source] sessions "HOL-Library" theories Preface Synopsis Framework First_Order_Logic Outer_Syntax Document_Preparation Spec Proof Proof_Script Inner_Syntax Generic HOL_Specific Quick_Reference Symbols document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "ttbox.sty" "underscore.sty" "manual.bib" document_files "build" "isar-vm.pdf" "isar-vm.svg" "root.tex" "showsymbols" "style.sty" session JEdit (doc) in "JEdit" = HOL + options [document_variants = "jedit", thy_output_source] theories JEdit document_files (in "..") "extra.sty" "iman.sty" "isar.sty" "manual.bib" "pdfsetup.sty" "prepare_document" "ttbox.sty" "underscore.sty" document_files (in "../Isar_Ref/document") "style.sty" document_files "auto-tools.png" "bibtex-mode.png" "build" "cite-completion.png" "isabelle-jedit-hdpi.png" "isabelle-jedit.png" "markdown-document.png" "ml-debugger.png" "output-and-state.png" "output-including-state.png" "output.png" "popup1.png" "popup2.png" "query.png" "root.tex" "scope1.png" "scope2.png" "sidekick-document.png" "sidekick.png" "sledgehammer.png" "theories.png" session Sugar (doc) in "Sugar" = HOL + options [document_variants = "sugar"] sessions "HOL-Library" theories Sugar document_files (in "..") "prepare_document" "pdfsetup.sty" document_files "build" "mathpartir.sty" "root.bib" "root.tex" session Locales (doc) in "Locales" = HOL + options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false] theories Examples1 Examples2 Examples3 document_files (in "..") "prepare_document" "pdfsetup.sty" document_files "build" "root.bib" "root.tex" session Logics (doc) in "Logics" = Pure + options [document_variants = "logics"] document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "ttbox.sty" "manual.bib" document_files "CTT.tex" "HOL.tex" "LK.tex" "Sequents.tex" "build" "preface.tex" "root.tex" "syntax.tex" session Logics_ZF (doc) in "Logics_ZF" = ZF + options [document_variants = "logics-ZF", print_mode = "brackets", thy_output_source] sessions FOL theories IFOL_examples FOL_examples ZF_examples If ZF_Isar document_files (in "..") "prepare_document" "pdfsetup.sty" "isar.sty" "ttbox.sty" "manual.bib" document_files (in "../Logics/document") "syntax.tex" document_files "FOL.tex" "ZF.tex" "build" "logics.sty" "root.tex" session Main (doc) in "Main" = HOL + options [document_variants = "main"] theories Main_Doc document_files (in "..") "prepare_document" "pdfsetup.sty" document_files "build" "root.tex" session Nitpick (doc) in "Nitpick" = Pure + options [document_variants = "nitpick"] document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "manual.bib" document_files "build" "root.tex" session Prog_Prove (doc) in "Prog_Prove" = HOL + options [document_variants = "prog-prove", show_question_marks = false] theories Basics Bool_nat_list MyList Types_and_funs Logic Isar document_files (in ".") "MyList.thy" document_files (in "..") "prepare_document" "pdfsetup.sty" document_files "bang.pdf" "build" "intro-isabelle.tex" "mathpartir.sty" "prelude.tex" "root.bib" "root.tex" "svmono.cls" session Sledgehammer (doc) in "Sledgehammer" = Pure + options [document_variants = "sledgehammer"] document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "manual.bib" document_files "build" "root.tex" session System (doc) in "System" = Pure + options [document_variants = "system", thy_output_source] sessions "HOL-Library" theories Environment Sessions Presentation Server Scala + Phabricator Misc document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "ttbox.sty" "underscore.sty" "manual.bib" document_files (in "../Isar_Ref/document") "style.sty" document_files "build" "root.tex" session Tutorial (doc) in "Tutorial" = HOL + options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr" "Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types" theories [threads = 1] "ToyList/ToyList_Test" theories [thy_output_indent = 5] "ToyList/ToyList" "Ifexpr/Ifexpr" "CodeGen/CodeGen" "Trie/Trie" "Datatype/ABexpr" "Datatype/unfoldnested" "Datatype/Nested" "Datatype/Fundata" "Fun/fun0" "Advanced/simp2" "CTL/PDL" "CTL/CTL" "CTL/CTLind" "Inductive/Even" "Inductive/Mutual" "Inductive/Star" "Inductive/AB" "Inductive/Advanced" "Misc/Tree" "Misc/Tree2" "Misc/Plus" "Misc/case_exprs" "Misc/fakenat" "Misc/natsum" "Misc/pairs2" "Misc/Option2" "Misc/types" "Misc/prime_def" "Misc/simp" "Misc/Itrev" "Misc/AdvancedInd" "Misc/appendix" theories "Protocol/NS_Public" "Documents/Documents" theories [document = false] "Types/Setup" theories [thy_output_margin = 64, thy_output_indent = 0] "Types/Numbers" "Types/Pairs" "Types/Records" "Types/Typedefs" "Types/Overloading" "Types/Axioms" "Rules/Basic" "Rules/Blast" "Rules/Force" theories [thy_output_margin = 64, thy_output_indent = 5] "Rules/TPrimes" "Rules/Forward" "Rules/Tacticals" "Rules/find2" "Sets/Examples" "Sets/Functions" "Sets/Relations" "Sets/Recur" document_files (in "ToyList") "ToyList1.txt" "ToyList2.txt" document_files (in "..") "pdfsetup.sty" "ttbox.sty" "manual.bib" document_files "advanced0.tex" "appendix0.tex" "basics.tex" "build" "cl2emono-modified.sty" "ctl0.tex" "documents0.tex" "fp.tex" "inductive0.tex" "isa-index" "Isa-logics.pdf" "numerics.tex" "pghead.pdf" "preface.tex" "protocol.tex" "root.tex" "rules.tex" "sets.tex" "tutorial.sty" "typedef.pdf" "types0.tex" session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = HOL + options [document_variants = "typeclass_hierarchy"] sessions "HOL-Library" theories [document = false] Setup theories Typeclass_Hierarchy document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files "build" "root.tex" "style.sty" diff --git a/src/Doc/System/Phabricator.thy b/src/Doc/System/Phabricator.thy new file mode 100644 --- /dev/null +++ b/src/Doc/System/Phabricator.thy @@ -0,0 +1,314 @@ +(*:maxLineLen=78:*) + +theory Phabricator +imports Base +begin + +chapter \Phabricator server administration\ + +text \ + Phabricator\<^footnote>\\<^url>\https://www.phacility.com/phabricator\\ is an open-source + product to support the development process of complex software projects + (open or closed ones). The official slogan is: + + \begin{quote} + Discuss. Plan. Code. Review. Test. \\ + Every application your project needs, all in one tool. + \end{quote} + + Ongoing changes and discussions about changes are maintained uniformly + within a MySQL database. There are standard connections to major version + control systems: \<^bold>\Subversion\, \<^bold>\Mercurial\, \<^bold>\Git\. So Phabricator offers + a counter-model to trends of monoculture and centralized version control, + especially due to Microsoft's Github and Atlassian's Bitbucket. + + The small company behind Phabricator provides paid plans for support and + hosting of servers, but it is relatively easy to do \<^emph>\independent + self-hosting\ on a standard LAMP server (Linux, Apache, MySQL, PHP). This + merely requires a virtual Ubuntu server on the net, which can be rented + rather cheaply from local hosting providers (there is no need to follow big + cloud corporations). So it is feasible to remain the master of your virtual + home, following the slogan ``own all your data''. In many respects, + Phabricator is similar to the well-known + Nextcloud\<^footnote>\\<^url>\https://nextcloud.com\\ product, concerning both the + technology and sociology. + + \<^medskip> + The following Phabricator instances may serve as examples: + + \<^item> Phabricator development \<^url>\https://secure.phabricator.com\ + \<^item> Wikimedia development \<^url>\https://phabricator.wikimedia.org\ + \<^item> Mercurial development \<^url>\https://phab.mercurial-scm.org\ + \<^item> Isabelle development \<^url>\https://isabelle-dev.sketis.net\ + + \<^medskip> Initial Phabricator server configuration requires many details to be done + right. Isabelle provides some command-line tools to help with it, but + afterwards Isabelle support is optional: it is possible to run and maintain + the server, without requiring a full Isabelle distribution again. +\ + + +section \Quick start\ + +text \ + The starting point is a fresh installation of \<^bold>\Ubuntu 18.04 LTS\: that + particular version is required due to subtle dependencies on system + configuration and add-on packages. + + For production use, a proper \<^emph>\Virtual Server\ or \<^emph>\Root Server\ product + from a hosting provider will be required, including an Internet Domain Name + (a pseudo sub-domain in the style of Apache is sufficient). + + Initial experimentation also works on a local host, e.g.\ via + VirtualBox\<^footnote>\\<^url>\https://www.virtualbox.org\\. The public server behind + \<^verbatim>\lvh.me\ provides arbitrary subdomains as an alias to \<^verbatim>\localhost\, which + will be used for the default installation below. + + All administrative commands need to be run as \<^verbatim>\root\ user (e.g.\ via + \<^verbatim>\sudo\). +\ + + +subsection \Initial setup\ + +text \ + Isabelle can managed multiple named installations Phabricator installations: + this allows to separate administrative responsibilities, e.g.\ different + approaches to user management for different projects. Subsequently we always + use the implicit default name ``\<^verbatim>\vcs\'': it will appear in file and + directory locations, internal database names and URLs. + + The initial setup (with full Linux package upgrade) works as follows: + + @{verbatim [display] \ isabelle phabricator_setup -U\} + + After installing many packages and cloning the Phabricator distribution, the + final output of the tool should be the URL for further manual configuration + (using a local web browser). Here the key points are: + + \<^item> An initial user account that will get administrator rights. There is no + need to create a separate \<^verbatim>\admin\ account. Instead, a regular user that + will take over this responsibility can be used here. Subsequently we + assume that user \<^verbatim>\makarius\ becomes the initial administrator. + + \<^item> An \<^emph>\Auth Provider\ to manage user names and passwords. None is provided + by default, and Phabricator points out this omission prominently in its + overview of \<^emph>\Setup Issues\: following these hints quickly leads to the + place where a regular \<^emph>\Username/Password\ provider can be added. + + Note that Phabricator allows to delegate the responsibility of + authentication to big corporations like Google and Facebook, but these can + be easily avoided. Genuine self-hosting means to manage users directly, + without outsourcing of authentication. + + \<^medskip> + With the Auth Provider available, the administrator can now set a proper + password. This works e.g.\ by initiating a local password reset procedure: + + @{verbatim [display] \ isabelle phabricator bin/auth recover makarius\} + + The printed URL gives access to a password dialog in the web browser. + + Further users will be able to provide a password more directly, because the + Auth Provider is now active. + + \<^medskip> + The pending request in Phabricator Setup Issues to lock the configuration + can be fulfilled as follows: + + @{verbatim [display] \ isabelle phabricator bin/auth lock\} +\ + + +subsection \Mailer configuration\ + +text \ + The next important thing is messaging: Phabricator needs to be able to + communicate with users. There are many variations on \<^emph>\Mailer + Configuration\, but a conventional SMTP server connection with a dedicated + \<^verbatim>\phabricator\ user is sufficient. Note that there is no need to run a mail + server on the self-hosted Linux machine: regular web-hosting packages + usually allow to create new mail accounts easily. (As a last resort it is + possible to use a service like Gmail, but that would again introduce + unnecessary dependency on Google.) + + \<^medskip> + Mailer configuration requires a few command-line invocations as follows: + + @{verbatim [display] \ isabelle phabricator_setup_mail\} + + \<^noindent> Now edit the generated JSON file to provide the mail account details. Then + add and test it with Phabricator like this (to let Phabricator send a + message to the administrator from above): + + @{verbatim [display] \ isabelle phabricator_setup_mail -T makarius\} + + The mail configuration process can be refined and repeated until it really + works: host name, port number, protocol etc.\ all need to be correct. The + \<^verbatim>\key\ field in the JSON file identifies the name of the configuration; it + will be overwritten each time, when taking over the parameters via + \<^verbatim>\isabelle phabricator_setup_mail\. + + \<^medskip> + For information, the resulting mailer configuration can be queried like + this: + + @{verbatim [display] \ isabelle phabricator bin/config get cluster.mailers\} +\ + + +section \Reference of command-line tools\ + +text \ + The subsequent command-line tools usually require root user privileges on + the underlying Linux system (e.g.\ via \<^verbatim>\sudo bash\ to open a subshell, or + directly via \<^verbatim>\sudo isabelle ...\). Note that Isabelle refers to + user-specific configuration in the user home directory via @{setting + ISABELLE_HOME_USER} (\secref{sec:settings}); that may be different or absent + for the root user and thus cause confusion. +\ + + +subsection \\<^verbatim>\isabelle phabricator\\ + +text \ + The @{tool_def phabricator} tool invokes a GNU bash command-line within the + Phabricator home directory: + @{verbatim [display] +\Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...] + + Options are: + -l list available Phabricator installations + -n NAME Phabricator installation name (default: "vcs") + + Invoke a command-line tool within the home directory of the named + Phabricator installation.\} + + Isabelle/Phabricator installations are registered in the global + configuration file \<^path>\/etc/isabelle-phabricator.conf\, with name and + root directory separated by colon (no extra whitespace). The home directory + is the subdirectory \<^verbatim>\phabricator\ within the root. + + \<^medskip> Option \<^verbatim>\-l\ lists the available Phabricator installations with name and + root directory. + + Option \<^verbatim>\-n\ selects the explicitly named Phabricator installation. +\ + + +subsubsection \Examples\ + +text \ + Print the home directory of the Phabricator installation: + @{verbatim [display] \isabelle phabricator pwd\} + + Print some Phabricator configuration information: + @{verbatim [display] \isabelle phabricator bin/config get phabricator.base-uri\} + + The latter conforms to typical command templates seen in the original + Phabricator documentation: + @{verbatim [display] \phabricator/ $ ./bin/config get phabricator.base-uri\} + + Here the user is meant to navigate to the Phabricator home manually, in + contrast to \<^verbatim>\isabelle phabricator\ doing it automatically based on + \<^path>\/etc/isabelle-phabricator.conf\. +\ + + +subsection \\<^verbatim>\isabelle phabricator_setup\\ + +text \ + The @{tool_def phabricator_setup} installs a fresh Phabricator instance on + Ubuntu Linux (notably 18.04 LTS): + @{verbatim [display] \Usage: isabelle phabricator_setup [OPTIONS] + + Options are: + -R DIR repository directory (default: "/var/www/phabricator-NAME/repo") + -U full update of system packages before installation + -n NAME Phabricator installation name (default: "vcs") + -r DIR installation root directory (default: "/var/www/phabricator-NAME") + + Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP). + + The installation name (default: "vcs") is mapped to a regular + Unix user; this is relevant for public SSH access.\} + + Installation requires Linux root user access. All required packages are + installed automatically beforehand, this includes the Apache web server and + the MySQL database engine. + + Global configuration in \<^verbatim>\/etc\ and other directories like \<^verbatim>\/var/www\ + always use name prefixes \<^verbatim>\isabelle-phabricator\ or \<^verbatim>\phabricator\. Local + configuration for a particular installation uses more specific names derived + from \<^verbatim>\phabricator-\\NAME\, e.g. \<^verbatim>\/var/www/phabricator-vcs\ for a default + installation. + + Knowing the conventions, it is possible to purge a Linux installation from + Isabelle/Phabricator with some effort. There is no automated + de-installation: it is often better to re-install a clean virtual machine + image. + + \<^medskip> + Option \<^verbatim>\-U\ ensures a full update of system packages, before installing + further packages required by Phabricator. + + Option \<^verbatim>\-n\ provides an alternative installation name. The default name + \<^verbatim>\vcs\ means ``Version Control System''. The name will appear in the URL for + SSH access, and thus has some relevance to end-users. The initial server URL + also uses that name suffix, but it can be changed later via regular Apache + configuration. + + Option \<^verbatim>\-r\ specifies an alternative installation root directory: it needs + to be accessible for the Apache web server. + + Option \<^verbatim>\-R\ specifies an alternative directory for repositories that are + hosted by Phabricator. Provided that it is accessible for the Apache web + server, the directory can be re-used directly for the builtin \<^verbatim>\hgweb\ view + by Mercurial. See also the documentation + \<^url>\https://www.mercurial-scm.org/wiki/PublishingRepositories#hgweb\ and the + example \<^url>\https://isabelle.sketis.net/repos\ for repositories in + \<^url>\https://isabelle-dev.sketis.net/diffusion\. +\ + + +subsection \\<^verbatim>\isabelle phabricator_setup_mail\\ + +text \ + The @{tool_def phabricator_setup_mail} provides mail configuration for an + existing Phabricator installation (preferably via SMTP): + @{verbatim [display] \Usage: isabelle phabricator_setup_mail [OPTIONS] + + Options are: + -T USER send test mail to Phabricator user + -f FILE config file (default: "mailers.json" within + Phabricator root) + -n NAME Phabricator installation name (default: "vcs") + + Provide mail configuration for existing Phabricator installation.\} + + Proper mail configuration is vital for Phabricator, but the details can be + tricky. A common approach is to re-use an existing SMTP mail service, as is + often included in regular web hosting packages. A single account for + multiple Phabricator installations is sufficient, but the configuration + needs to be set for each installation separately. + + The first invocation of \<^verbatim>\isabelle phabricator_setup_mail\ without options + creates a JSON template file. Its \<^verbatim>\key\ entry should be changed to + something sensible to identify the configuration, e.g.\ the Internet Domain + Name of the mail address being used here. The \<^verbatim>\options\ specify the SMTP + server address and account information. + + Another invocation of \<^verbatim>\isabelle phabricator_setup_mail\ with updated JSON + file will change the underlying Phabricator installation. This can be done + repeatedly, until everything works as expected. + + Option \<^verbatim>\-T\ invokes a standard Phabricator test procedure for the mail + configuration. The argument needs to be a valid Phabricator user: the mail + address is derived from the user profile. + + Option \<^verbatim>\-f\ refers to an existing JSON configuration file, e.g.\ from a + different Phabricator installation: sharing mailers setup with the same mail + address works for outgoing mails; incoming mails are not strictly needed. +\ + +end diff --git a/src/Doc/System/document/root.tex b/src/Doc/System/document/root.tex --- a/src/Doc/System/document/root.tex +++ b/src/Doc/System/document/root.tex @@ -1,49 +1,50 @@ \documentclass[12pt,a4paper]{report} \usepackage{lmodern} \usepackage[T1]{fontenc} \usepackage{supertabular} \usepackage{graphicx} \usepackage{iman,extra,isar} \usepackage[nohyphen,strings]{underscore} \usepackage{isabelle,isabellesym} \usepackage{railsetup} \usepackage{style} \usepackage{pdfsetup} \hyphenation{Isabelle} \hyphenation{Isar} \isadroptag{theory} \isabellestyle{literal} \def\isastylett{\footnotesize\tt} \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual} \author{\emph{Makarius Wenzel}} \makeindex \begin{document} \maketitle \pagenumbering{roman} \tableofcontents \clearfirst \input{Environment.tex} \input{Sessions.tex} \input{Presentation.tex} \input{Server.tex} \input{Scala.tex} +\input{Phabricator.tex} \input{Misc.tex} \begingroup \tocentry{\bibname} \bibliographystyle{abbrv} \small\raggedright\frenchspacing \bibliography{manual} \endgroup \tocentry{\indexname} \printindex \end{document} diff --git a/src/Pure/General/output.scala b/src/Pure/General/output.scala --- a/src/Pure/General/output.scala +++ b/src/Pure/General/output.scala @@ -1,47 +1,47 @@ /* Title: Pure/General/output.scala Author: Makarius Isabelle output channels. */ package isabelle object Output { def clean_yxml(msg: String): String = try { XML.content(Protocol_Message.clean_reports(YXML.parse_body(msg))) } catch { case ERROR(_) => msg } def writeln_text(msg: String): String = clean_yxml(msg) def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _)) def error_message_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _)) - def writeln(msg: String, stdout: Boolean = false) + def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false) { - if (msg != "") { + if (msg.nonEmpty || include_empty) { if (stdout) Console.print(writeln_text(msg) + "\n") else Console.err.print(writeln_text(msg) + "\n") } } - def warning(msg: String, stdout: Boolean = false) + def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false) { - if (msg != "") { + if (msg.nonEmpty || include_empty) { if (stdout) Console.print(warning_text(msg) + "\n") else Console.err.print(warning_text(msg) + "\n") } } - def error_message(msg: String, stdout: Boolean = false) + def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false) { - if (msg != "") { + if (msg.nonEmpty || include_empty) { if (stdout) Console.print(error_message_text(msg) + "\n") else Console.err.print(error_message_text(msg) + "\n") } } } diff --git a/src/Pure/System/isabelle_tool.scala b/src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala +++ b/src/Pure/System/isabelle_tool.scala @@ -1,178 +1,179 @@ /* Title: Pure/System/isabelle_tool.scala Author: Makarius Author: Lars Hupel Isabelle system tools: external executables or internal Scala functions. */ package isabelle import java.net.URLClassLoader import scala.reflect.runtime.universe import scala.tools.reflect.{ToolBox,ToolBoxError} object Isabelle_Tool { /* Scala source tools */ abstract class Body extends Function[List[String], Unit] private def compile(path: Path): Body = { def err(msg: String): Nothing = cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path) val source = File.read(path) val class_loader = new URLClassLoader(Array(), getClass.getClassLoader) val tool_box = universe.runtimeMirror(class_loader).mkToolBox() try { val symbol = tool_box.parse(source) match { case tree: universe.ModuleDef => tool_box.define(tree) case _ => err("Source does not describe a module (Scala object)") } tool_box.compile(universe.Ident(symbol))() match { case body: Body => body case _ => err("Ill-typed source: Isabelle_Tool.Body expected") } } catch { case e: ToolBoxError => if (tool_box.frontEnd.hasErrors) { val infos = tool_box.frontEnd.infos.toList val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg) err(msgs.mkString("\n")) } else err(e.toString) } } /* external tools */ private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS")) private def is_external(dir: Path, file_name: String): Boolean = { val file = (dir + Path.explode(file_name)).file try { file.isFile && file.canRead && (file_name.endsWith(".scala") || file.canExecute) && !file_name.endsWith("~") && !file_name.endsWith(".orig") } catch { case _: SecurityException => false } } private def list_external(): List[(String, String)] = { val Description = """.*\bDESCRIPTION: *(.*)""".r for { dir <- dirs() if dir.is_dir file_name <- File.read_dir(dir) if is_external(dir, file_name) } yield { val source = File.read(dir + Path.explode(file_name)) val name = Library.perhaps_unsuffix(".scala", file_name) val description = split_lines(source).collectFirst({ case Description(s) => s }) getOrElse "" (name, description) } } private def find_external(name: String): Option[List[String] => Unit] = dirs.collectFirst({ case dir if is_external(dir, name + ".scala") => compile(dir + Path.explode(name + ".scala")) case dir if is_external(dir, name) => (args: List[String]) => { val tool = dir + Path.explode(name) val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args)) sys.exit(result.print_stdout.rc) } }) /* internal tools */ private lazy val internal_tools: List[Isabelle_Tool] = Isabelle_System.init_classes[Isabelle_Scala_Tools]("ISABELLE_SCALA_TOOLS") .flatMap(_.tools.toList) private def list_internal(): List[(String, String)] = for (tool <- internal_tools.toList) yield (tool.name, tool.description) private def find_internal(name: String): Option[List[String] => Unit] = internal_tools.collectFirst({ case tool if tool.name == name => args => Command_Line.tool0 { tool.body(args) } }) /* command line entry point */ def main(args: Array[String]) { Command_Line.tool0 { args.toList match { case Nil | List("-?") => val tool_descriptions = (list_external() ::: list_internal()).sortBy(_._1). map({ case (a, "") => a case (a, b) => a + " - " + b }) Getopts(""" Usage: isabelle TOOL [ARGS ...] Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help. Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage case tool_name :: tool_args => find_external(tool_name) orElse find_internal(tool_name) match { case Some(tool) => tool(tool_args) case None => error("Unknown Isabelle tool: " + quote(tool_name)) } } } } } sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit) class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) class Tools extends Isabelle_Scala_Tools( Build.isabelle_tool, Build_Docker.isabelle_tool, Doc.isabelle_tool, Dump.isabelle_tool, Export.isabelle_tool, ML_Process.isabelle_tool, Mkroot.isabelle_tool, Options.isabelle_tool, Phabricator.isabelle_tool1, Phabricator.isabelle_tool2, + Phabricator.isabelle_tool3, Present.isabelle_tool, Profiling_Report.isabelle_tool, Server.isabelle_tool, Update.isabelle_tool, Update_Cartouches.isabelle_tool, Update_Comments.isabelle_tool, Update_Header.isabelle_tool, Update_Then.isabelle_tool, Update_Theorems.isabelle_tool, isabelle.vscode.Grammar.isabelle_tool, isabelle.vscode.Server.isabelle_tool) class Admin_Tools extends Isabelle_Scala_Tools( Build_Cygwin.isabelle_tool, Build_Doc.isabelle_tool, Build_Fonts.isabelle_tool, Build_JDK.isabelle_tool, Build_PolyML.isabelle_tool1, Build_PolyML.isabelle_tool2, Build_Status.isabelle_tool, Check_Sources.isabelle_tool, Components.isabelle_tool, isabelle.vscode.Build_VSCode.isabelle_tool) diff --git a/src/Pure/System/progress.scala b/src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala +++ b/src/Pure/System/progress.scala @@ -1,87 +1,87 @@ /* Title: Pure/System/progress.scala Author: Makarius Progress context for system processes. */ package isabelle import java.io.{File => JFile} object Progress { sealed case class Theory(theory: String, session: String = "", percentage: Option[Int] = None) { def message: String = print_session + print_theory + print_percentage def print_session: String = if (session == "") "" else session + ": " def print_theory: String = "theory " + theory def print_percentage: String = percentage match { case None => "" case Some(p) => " " + p + "%" } } } class Progress { def echo(msg: String) {} def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) } def theory(theory: Progress.Theory) {} def nodes_status(nodes_status: Document_Status.Nodes_Status) {} def echo_warning(msg: String) { echo(Output.warning_text(msg)) } def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) } def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A = Timing.timeit(message, enabled, echo(_))(e) def stopped: Boolean = false def interrupt_handler[A](e: => A): A = e def expose_interrupt() { if (stopped) throw Exn.Interrupt() } override def toString: String = if (stopped) "Progress(stopped)" else "Progress" def bash(script: String, cwd: JFile = null, env: Map[String, String] = Isabelle_System.settings(), redirect: Boolean = false, echo: Boolean = false, strict: Boolean = true): Process_Result = { Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect, progress_stdout = echo_if(echo, _), progress_stderr = echo_if(echo, _), strict = strict) } } object No_Progress extends Progress class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress { override def echo(msg: String): Unit = - Output.writeln(msg, stdout = !stderr) + Output.writeln(msg, stdout = !stderr, include_empty = true) override def theory(theory: Progress.Theory): Unit = if (verbose) echo(theory.message) @volatile private var is_stopped = false override def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e } override def stopped: Boolean = { if (Thread.interrupted) is_stopped = true is_stopped } } class File_Progress(path: Path, verbose: Boolean = false) extends Progress { override def echo(msg: String): Unit = File.append(path, msg + "\n") override def theory(theory: Progress.Theory): Unit = if (verbose) echo(theory.message) override def toString: String = path.toString } diff --git a/src/Pure/Tools/phabricator.scala b/src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala +++ b/src/Pure/Tools/phabricator.scala @@ -1,470 +1,510 @@ /* Title: Pure/Tools/phabricator.scala Author: Makarius Support for Phabricator server, notably for Ubuntu 18.04 LTS. See also: - https://www.phacility.com/phabricator - https://secure.phabricator.com/book/phabricator */ package isabelle import scala.util.matching.Regex object Phabricator { /** defaults **/ /* required packages */ val packages: List[String] = Build_Docker.packages ::: List( // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61 "git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring", // more packages "php-zip", "python-pygments", "ssh") /* global system resources */ val www_user = "www-data" val daemon_user = "phabricator" val ssh_standard = 22 val ssh_alternative1 = 222 val ssh_alternative2 = 2222 /* installation parameters */ val default_name = "vcs" def phabricator_name(name: String = "", ext: String = ""): String = "phabricator" + (if (name.isEmpty) "" else "-" + name) + (if (ext.isEmpty) "" else "." + ext) def isabelle_phabricator_name(name: String = "", ext: String = ""): String = "isabelle-" + phabricator_name(name = name, ext = ext) def default_root(name: String): Path = Path.explode("/var/www") + Path.basic(phabricator_name(name = name)) def default_repo(name: String): Path = default_root(name) + Path.basic("repo") val default_mailers: Path = Path.explode("mailers.json") /** global configuration **/ val global_config = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf")) sealed case class Config(name: String, root: Path) { def home: Path = root + Path.explode(phabricator_name()) def execute(command: String): Process_Result = - Isabelle_System.bash("./bin/" + command, cwd = home.file, redirect = true).check + Isabelle_System.bash("bin/" + command, cwd = home.file, redirect = true).check } def read_config(): List[Config] = { if (global_config.is_file) { for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty) yield { space_explode(':', entry) match { case List(name, root) => Config(name, Path.explode(root)) case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry)) } } } else Nil } def write_config(configs: List[Config]) { File.write(global_config, configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n")) } def get_config(name: String): Config = read_config().find(config => config.name == name) getOrElse error("Bad Isabelle/Phabricator installation " + quote(name)) + /** command-line tools **/ + + /* Isabelle tool wrapper */ + + val isabelle_tool1 = + Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory", args => + { + var list = false + var name = default_name + + val getopts = + Getopts(""" +Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...] + + Options are: + -l list available Phabricator installations + -n NAME Phabricator installation name (default: """ + quote(default_name) + """) + + Invoke a command-line tool within the home directory of the named + Phabricator installation. +""", + "l" -> (_ => list = true), + "n:" -> (arg => name = arg)) + + val more_args = getopts(args) + if (more_args.isEmpty && !list) getopts.usage() + + val progress = new Console_Progress + + if (list) { + for (config <- read_config()) { + progress.echo("phabricator " + quote(config.name) + " root " + config.root) + } + } + + val config = get_config(name) + + val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true) + if (!result.ok) error("Return code: " + result.rc.toString) + }) + + + /** setup **/ def user_setup(name: String, description: String, ssh_setup: Boolean = false) { if (!Linux.user_exists(name)) { Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup) } else if (Linux.user_description(name) != description) { error("User " + quote(name) + " already exists --" + " for Phabricator it should have the description:\n " + quote(description)) } } def phabricator_setup( name: String = default_name, root: String = "", repo: String = "", package_update: Boolean = false, progress: Progress = No_Progress) { /* system environment */ Linux.check_system_root() progress.echo("System packages ...") if (package_update) { Linux.package_update(progress = progress) Linux.check_reboot_required() } Linux.package_install(packages, progress = progress) Linux.check_reboot_required() /* users */ if (name == daemon_user) { error("Clash of installation name with daemon user " + quote(daemon_user)) } user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true) user_setup(name, "Phabricator SSH User") /* basic installation */ progress.echo("\nPhabricator installation ...") val root_path = if (root.nonEmpty) Path.explode(root) else default_root(name) val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(name) val configs = read_config() for (config <- configs if config.name == name) { error("Duplicate Phabricator installation " + quote(name) + " in " + config.root) } if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) { error("Failed to create root directory " + root_path) } progress.bash(cwd = root_path.file, echo = true, script = """ set -e chown """ + Bash.string(www_user) + ":" + Bash.string(www_user) + """ . chmod 755 . git clone https://github.com/phacility/libphutil.git git clone https://github.com/phacility/arcanist.git git clone https://github.com/phacility/phabricator.git """).check val config = Config(name, root_path) write_config(configs ::: List(config)) config.execute("config set pygments.enabled true") /* local repository directory */ if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) { error("Failed to create local repository directory " + repo_path) } Isabelle_System.bash(cwd = repo_path.file, script = """ set -e chown -R """ + Bash.string(daemon_user) + ":" + Bash.string(daemon_user) + """ . chmod 755 . """).check config.execute("config set repository.default-local-path " + File.bash_path(repo_path)) /* MySQL setup */ progress.echo("\nMySQL setup ...") File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")), """[mysqld] max_allowed_packet = 32M innodb_buffer_pool_size = 1600M local_infile = 0 """) Linux.service_restart("mysql") def mysql_conf(R: Regex): Option[String] = split_lines(File.read(Path.explode("/etc/mysql/debian.cnf"))).collectFirst({ case R(a) => a }) for (user <- mysql_conf("""^user\s*=\s*(\S*)\s*$""".r)) { config.execute("config set mysql.user " + Bash.string(user)) } for (pass <- mysql_conf("""^password\s*=\s*(\S*)\s*$""".r)) { config.execute("config set mysql.pass " + Bash.string(pass)) } config.execute("config set storage.default-namespace " + Bash.string(phabricator_name(name = name).replace("-", "_"))) config.execute("config set storage.mysql-engine.max-size 8388608") - progress.bash("./bin/storage upgrade --force", cwd = config.home.file, echo = true).check + progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check /* SSH hosting */ progress.echo("\nSSH hosting setup ...") val ssh_port = ssh_alternative2 config.execute("config set diffusion.ssh-user " + Bash.string(name)) config.execute("config set diffusion.ssh-port " + ssh_port) val sudoers_file = Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name()) File.write(sudoers_file, www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" + name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n") Isabelle_System.bash("chmod 0440 " + File.bash_path(sudoers_file)).check /* PHP setup */ val php_version = Isabelle_System.bash("""php --run 'echo PHP_MAJOR_VERSION . "." . PHP_MINOR_VERSION;'""") .check.out val php_conf = Path.explode("/etc/php") + Path.basic(php_version) + // educated guess Path.explode("apache2/conf.d") + Path.basic(isabelle_phabricator_name(ext = "ini")) File.write(php_conf, "post_max_size = 32M\n" + "opcache.validate_timestamps = 0\n" + "memory_limit = 512M\n") /* Apache setup */ progress.echo("Apache setup ...") val apache_root = Path.explode("/etc/apache2") val apache_sites = apache_root + Path.explode("sites-available") if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites) val server_name = phabricator_name(name = name, ext = "lvh.me") // alias for "localhost" for testing val server_url = "http://" + server_name File.write(apache_sites + Path.basic(isabelle_phabricator_name(name = name, ext = "conf")), """ ServerName """ + server_name + """ ServerAdmin webmaster@localhost DocumentRoot """ + config.home.implode + """/webroot ErrorLog ${APACHE_LOG_DIR}/error.log RewriteEngine on RewriteRule ^(.*)$ /index.php?__path__=$1 [B,L,QSA] # vim: syntax=apache ts=4 sw=4 sts=4 sr noet """) Isabelle_System.bash( """ set -e a2enmod rewrite a2ensite """ + Bash.string(isabelle_phabricator_name(name = name))).check config.execute("config set phabricator.base-uri " + Bash.string(server_url)) Linux.service_restart("apache2") /* PHP daemon */ progress.echo("PHP daemon setup ...") config.execute("config set phd.user " + Bash.string(daemon_user)) Linux.service_install(isabelle_phabricator_name(name = name), """[Unit] Description=PHP daemon for Isabelle/Phabricator """ + quote(name) + """ After=syslog.target network.target apache2.service mysql.service [Service] Type=oneshot User=""" + daemon_user + """ Group=""" + daemon_user + """ Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin ExecStart=""" + config.home.implode + """/bin/phd start ExecStop=""" + config.home.implode + """/bin/phd stop RemainAfterExit=yes [Install] WantedBy=multi-user.target """) progress.echo("\nDONE\nWeb configuration via " + server_url) } /* Isabelle tool wrapper */ - val isabelle_tool1 = + val isabelle_tool2 = Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", args => { var repo = "" var package_update = false var name = default_name var root = "" val getopts = Getopts(""" Usage: isabelle phabricator_setup [OPTIONS] Options are: -R DIR repository directory (default: """ + default_repo("NAME") + """) -U full update of system packages before installation -n NAME Phabricator installation name (default: """ + quote(default_name) + """) -r DIR installation root directory (default: """ + default_root("NAME") + """) - Install Phabricator as Ubuntu LAMP application (Linux, Apache, MySQL, PHP). - - Slogan: "Discuss. Plan. Code. Review. Test. - Every application your project needs, all in one tool." + Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP). The installation name (default: """ + quote(default_name) + """) is mapped to a regular Unix user; this is relevant for public SSH access. """, "R:" -> (arg => repo = arg), "U" -> (_ => package_update = true), "n:" -> (arg => name = arg), "r:" -> (arg => root = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup(name = name, root = root, repo = repo, package_update = package_update, progress = progress) }) /** setup mail **/ val mailers_template: String = """[ { "key": "example.org", "type": "smtp", "options": { "host": "mail.example.org", "port": 465, "user": "phabricator@example.org", "password": "********", "protocol": "ssl", "message-id": true } } ]""" def phabricator_setup_mail( name: String = default_name, config_file: Option[Path] = None, test_user: String = "", progress: Progress = No_Progress) { Linux.check_system_root() val config = get_config(name) val default_config_file = config.root + default_mailers val mail_config = config_file getOrElse default_config_file def setup_mail { progress.echo("Using mail configuration from " + mail_config) config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config)) if (test_user.nonEmpty) { progress.echo("Sending test mail to " + quote(test_user)) progress.bash(cwd = config.home.file, echo = true, - script = """echo "Test from Phabricator ($(date))" | ./bin/mail send-test --subject "Test" --to """ + + script = """echo "Test from Phabricator ($(date))" | bin/mail send-test --subject "Test" --to """ + Bash.string(test_user)).check } } if (config_file.isEmpty) { if (!default_config_file.is_file) { File.write(default_config_file, mailers_template) Isabelle_System.bash("chmod 600 " + File.bash_path(default_config_file)).check } if (File.read(default_config_file) == mailers_template) { progress.echo( """ Please invoke the tool again, after providing details in """ + default_config_file.implode + """ See also section "Mailer: SMTP" in https://secure.phabricator.com/book/phabricator/article/configuring_outbound_email """) } else setup_mail } else setup_mail } /* Isabelle tool wrapper */ - val isabelle_tool2 = + val isabelle_tool3 = Isabelle_Tool("phabricator_setup_mail", "setup mail configuration for existing Phabricator server", args => { var test_user = "" var name = default_name var config_file: Option[Path] = None val getopts = Getopts(""" Usage: isabelle phabricator_setup_mail [OPTIONS] Options are: -T USER send test mail to Phabricator user - -f FILE config file (default: """ + default_mailers + """ within installation root) + -f FILE config file (default: """ + default_mailers + """ within Phabricator root) -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Provide mail configuration for existing Phabricator installation. """, "T:" -> (arg => test_user = arg), "f:" -> (arg => config_file = Some(Path.explode(arg))), "n:" -> (arg => name = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup_mail(name = name, config_file = config_file, test_user = test_user, progress = progress) }) }