diff --git a/Admin/Phabricator/README b/Admin/Phabricator/README --- a/Admin/Phabricator/README +++ b/Admin/Phabricator/README @@ -1,99 +1,99 @@ Phabricator server ================== - https://www.phacility.com/phabricator Slogan: "Discuss. Plan. Code. Review. Test. Every application your project needs, all in one tool." - Ubuntu 18.04 LTS Linux Server standard installation with Apache and MySQL https://help.ubuntu.com/lts/serverguide https://help.ubuntu.com/lts/serverguide/httpd.html https://help.ubuntu.com/lts/serverguide/mysql.html - Apache HTTPS via "Let's Encrypt": https://letsencrypt.org/getting-started https://certbot.eff.org/lets-encrypt/ubuntubionic-apache.html - Installation: https://secure.phabricator.com/book/phabricator/article/installation_guide https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh ./bin/storage upgrade --force admin user: makarius - Configuration/Setup Issues: ignore "Alternate File Domain Not Configured" Add Auth Provider: Username/Password ./bin/auth lock ./bin/phd start - Configuration / Authentication: https://secure.phabricator.com/book/phabricator/article/configuring_accounts_and_registration . only local User/Password, *not* Google, Github etc. . auth.require-email-verification true . policy.allow-public true - Configuration/Mail: https://secure.phabricator.com/book/phabricator/article/configuring_outbound_email e.g. external SMTP via suitable mailers.json: $ ./bin/config set --stdin cluster.mailers < mailers.json - Configuration/SSH: https://secure.phabricator.com/book/phabricator/article/diffusion_hosting /etc/ssh/sshd_config: Port 222 /etc/passwd: - phab-daemon:x:118:126::/home/phab-daemon:/bin/bash + phabricator:x:118:126::/home/phabricator:/bin/bash vcs:x:119:125::/home/vcs:/bin/bash /etc/group: - phab-daemon:x:126: + phabricator:x:126: vcs:x:125: $ cp ssh/ssh-hook /usr/local/bin/. $ cp ssh/sshd_config.phabricator /etc/ssh/. $ cp ssh/sshd-phabricator.service /lib/systemd/system/. $ cp ssh/sudoers.d/phabricator /etc/sudoers.d/. - $ ./bin/config set phd.user phab-daemon + $ ./bin/config set phd.user phabricator $ ./bin/config set diffusion.ssh-user vcs $ ./bin/config set diffusion.ssh-port 22 + $ systemctl enable sshd-phabricator $ systemctl start sshd-phabricator - $ systemctl enable sshd-phabricator Test on local machine: $ echo "{}" | ssh vcs@phabricator.sketis.net conduit conduit.ping - Repository Local Path: mkdir -p /var/www/phabricator/repo - chown phab-daemon:phab-daemon /var/www/phabricator/repo + chown phabricator:phabricator /var/www/phabricator/repo - PHP Daemon: $ cp phd/phd-phabricator.service /lib/systemd/system/. + $ systemctl enable phd-phabricator $ systemctl start phd-phabricator - $ systemctl enable phd-phabricator - Update: https://secure.phabricator.com/book/phabricator/article/upgrading sudo ./update ./bin/diviner generate - Backup: https://secure.phabricator.com/book/phabricator/article/configuring_backups $ apt install automysqlbackup edit /etc/default/automysqlbackup: BACKUPDIR diff --git a/Admin/Phabricator/phd/phd-phabricator.service b/Admin/Phabricator/phd/phd-phabricator.service --- a/Admin/Phabricator/phd/phd-phabricator.service +++ b/Admin/Phabricator/phd/phd-phabricator.service @@ -1,15 +1,15 @@ [Unit] Description=PHP daemon (Phabricator) After=syslog.target network.target apache2.service mysql.service [Service] Type=oneshot -User=phab-daemon -Group=phab-daemon +User=phabricator +Group=phabricator Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin ExecStart=/var/www/phabricator/phabricator/bin/phd start ExecStop=/var/www/phabricator/phabricator/bin/phd stop RemainAfterExit=yes [Install] WantedBy=multi-user.target diff --git a/Admin/Phabricator/ssh/sudoers.d/phabricator b/Admin/Phabricator/ssh/sudoers.d/phabricator --- a/Admin/Phabricator/ssh/sudoers.d/phabricator +++ b/Admin/Phabricator/ssh/sudoers.d/phabricator @@ -1,2 +1,2 @@ -www-data ALL=(phab-daemon) SETENV: NOPASSWD: /usr/bin/git, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id -vcs ALL=(phab-daemon) 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 +www-data ALL=(phabricator) SETENV: NOPASSWD: /usr/bin/git, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id +vcs ALL=(phabricator) 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 diff --git a/etc/options b/etc/options --- a/etc/options +++ b/etc/options @@ -1,367 +1,365 @@ (* :mode=isabelle-options: *) section "Document Preparation" option browser_info : bool = false -- "generate theory browser information" option document : string = "" -- "build document in given format: pdf, dvi, false" option document_output : string = "" -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)" option document_variants : string = "document" -- "alternative document variants (separated by colons)" option document_tags : string = "" -- "default command tags (separated by commas)" option thy_output_display : bool = false -- "indicate output as multi-line display-style material" option thy_output_break : bool = false -- "control line breaks in non-display material" option thy_output_cartouche : bool = false -- "indicate if the output should be delimited as cartouche" option thy_output_quotes : bool = false -- "indicate if the output should be delimited via double quotes" option thy_output_margin : int = 76 -- "right margin / page width for printing of display material" option thy_output_indent : int = 0 -- "indentation for pretty printing of display material" option thy_output_source : bool = false -- "print original source text rather than internal representation" option thy_output_source_cartouche : bool = false -- "print original source text rather than internal representation, preserve cartouches" option thy_output_modes : string = "" -- "additional print modes for document output (separated by commas)" section "Prover Output" option show_types : bool = false -- "show type constraints when printing terms" option show_sorts : bool = false -- "show sort constraints when printing types" option show_brackets : bool = false -- "show extra brackets when printing terms/types" option show_question_marks : bool = true -- "show leading question mark of schematic variables" option show_consts : bool = false -- "show constants with types when printing proof state" option show_main_goal : bool = false -- "show main goal when printing proof state" option goals_limit : int = 10 -- "maximum number of subgoals to be printed" option names_long : bool = false -- "show fully qualified names" option names_short : bool = false -- "show base names only" option names_unique : bool = true -- "show partially qualified names, as required for unique name resolution" option eta_contract : bool = true -- "print terms in eta-contracted form" option print_mode : string = "" -- "additional print modes for prover output (separated by commas)" section "Parallel Processing" public option threads : int = 0 -- "maximum number of worker threads for prover process (0 = hardware max.)" option threads_trace : int = 0 -- "level of tracing information for multithreading" option threads_stack_limit : real = 0.25 -- "maximum stack size for worker threads (in giga words, 0 = unlimited)" public option parallel_limit : int = 0 -- "approximative limit for parallel tasks (0 = unlimited)" public option parallel_print : bool = true -- "parallel and asynchronous printing of results" public option parallel_proofs : int = 1 -- "level of parallel proof checking: 0, 1, 2" option parallel_subproofs_threshold : real = 0.01 -- "lower bound of timing estimate for forked nested proofs (seconds)" option command_timing_threshold : real = 0.1 -- "default threshold for persistent command timing (seconds)" section "Detail of Proof Checking" option record_proofs : int = -1 -- "set level of proofterm recording: 0, 1, 2, negative means unchanged" option quick_and_dirty : bool = false -- "if true then some tools will OMIT some proofs" option skip_proofs : bool = false -- "skip over proofs (implicit 'sorry')" option strict_facts : bool = false -- "force lazy facts when defined in context" section "Global Session Parameters" option condition : string = "" -- "required environment variables for subsequent theories (separated by commas)" option timeout : real = 0 -- "timeout for session build job (seconds > 0)" option timeout_scale : real = 1.0 -- "scale factor for session timeout" option process_output_limit : int = 100 -- "build process output limit (in million characters, 0 = unlimited)" option process_output_tail : int = 40 -- "build process output tail shown to user (in lines, 0 = unlimited)" option profiling : string = "" -- "ML profiling (possible values: time, allocations)" option system_heaps : bool = false -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" section "ML System" option ML_print_depth : int = 20 -- "ML print depth for toplevel pretty-printing" public option ML_exception_trace : bool = false -- "ML exception trace for toplevel command execution" public option ML_exception_debugger : bool = false -- "ML debugger exception trace for toplevel command execution" public option ML_debugger : bool = false -- "ML debugger instrumentation for newly compiled code" public option ML_statistics : bool = true -- "ML run-time system statistics" public option ML_system_64 : bool = false -- "ML system for 64bit platform is used if possible (change requires restart)" public option ML_process_policy : string = "" -- "ML process command prefix (process policy)" section "Editor Session" public option editor_load_delay : real = 0.5 -- "delay for file load operations (new buffers etc.)" public option editor_input_delay : real = 0.3 -- "delay for user input (text edits, cursor movement etc.)" public option editor_generated_input_delay : real = 1.0 -- "delay for machine-generated input that may outperform user edits" public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" public option editor_consolidate_delay : real = 2.0 -- "delay to consolidate status of command evaluation (execution forks)" public option editor_prune_delay : real = 15 -- "delay to prune history (delete old versions)" option editor_prune_size : int = 0 -- "retained size of pruned history (delete old versions)" public option editor_update_delay : real = 0.5 -- "delay for physical GUI updates" public option editor_reparse_limit : int = 10000 -- "maximum amount of reparsed text outside perspective" public option editor_tracing_messages : int = 1000 -- "initial number of tracing messages for each command transaction (0: unbounded)" public option editor_chart_delay : real = 3.0 -- "delay for chart repainting" public option editor_continuous_checking : bool = true -- "continuous checking of proof document (visible and required parts)" public option editor_output_state : bool = false -- "implicit output of proof state" option editor_execution_delay : real = 0.02 -- "delay for start of execution process after document update (seconds)" option editor_syslog_limit : int = 100 -- "maximum amount of buffered syslog messages" public option editor_presentation : bool = false -- "dynamic presentation while editing" section "Headless Session" option headless_consolidate_delay : real = 15 -- "delay to consolidate status of command evaluation (execution forks)" option headless_prune_delay : real = 60 -- "delay to prune history (delete old versions)" option headless_check_delay : real = 0.5 -- "delay for theory status check during PIDE processing (seconds)" option headless_check_limit : int = 0 -- "maximum number of theory status checks (0 = unlimited)" option headless_nodes_status_delay : real = -1 -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)" option headless_watchdog_timeout : real = 600 -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)" option headless_commit_cleanup_delay : real = 60 -- "delay for cleanup of already imported theories (seconds, 0 = disabled)" option headless_load_limit : real = 5.0 -- "limit in MB for loaded theory files (0 = unlimited)" section "Miscellaneous Tools" public option find_theorems_limit : int = 40 -- "limit of displayed results" public option find_theorems_tactic_limit : int = 5 -- "limit of tactic search for 'solves' criterion" section "Completion" public option completion_limit : int = 40 -- "limit for completion within the formal context" public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store" -- "glob patterns to ignore in file-system path completion (separated by colons)" section "Spell Checker" public option spell_checker : bool = true -- "enable spell-checker for prose words within document text, comments etc." public option spell_checker_dictionary : string = "en" -- "spell-checker dictionary name" public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment" -- "included markup elements for spell-checker (separated by commas)" public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text" -- "excluded markup elements for spell-checker (separated by commas)" section "Secure Shell" option ssh_config_dir : string = "$HOME/.ssh" -- "SSH configuration directory" option ssh_config_file : string = "$HOME/.ssh/config" -- "main SSH configuration file" option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa" -- "possible SSH identity files (separated by colons)" option ssh_compression : bool = true -- "enable SSH compression" option ssh_connect_timeout : real = 60 -- "SSH connection timeout (seconds)" option ssh_alive_interval : real = 30 -- "time interval to keep SSH server connection alive (seconds)" option ssh_alive_count_max : int = 3 -- "maximum number of messages to keep SSH server connection alive" section "Theory Export" option export_document : bool = false -- "export document sources to Isabelle/Scala" option export_theory : bool = false -- "export theory content to Isabelle/Scala" option export_standard_proofs : bool = false -- "export standardized proof terms to Isabelle/Scala (not scalable)" option export_proofs : bool = false -- "export proof terms to Isabelle/Scala" option prune_proofs : bool = false -- "prune proof terms after export (do not store in Isabelle/ML)" section "Theory update" option update_inner_syntax_cartouches : bool = false -- "update inner syntax (types, terms, etc.) to use cartouches" option update_mixfix_cartouches : bool = false -- "update mixfix templates to use cartouches instead of double quotes" option update_control_cartouches : bool = false -- "update antiquotations to use control symbol with cartouche argument" option update_path_cartouches : bool = false -- "update file-system paths to use cartouches" section "Build Database" option build_database_server : bool = false option build_database_user : string = "" option build_database_password : string = "" option build_database_name : string = "" option build_database_host : string = "" option build_database_port : int = 0 option build_database_ssh_host : string = "" option build_database_ssh_user : string = "" option build_database_ssh_port : int = 0 section "Build Log Database" option build_log_database_user : string = "" option build_log_database_password : string = "" option build_log_database_name : string = "" option build_log_database_host : string = "" option build_log_database_port : int = 0 option build_log_ssh_host : string = "" option build_log_ssh_user : string = "" option build_log_ssh_port : int = 0 option build_log_history : int = 30 -- "length of relevant history (in days)" option build_log_transaction_size : int = 1 -- "number of log files for each db update" section "Phabricator server" -option phabricator_user : string = "phabricator" - option phabricator_www_user : string = "www-data" option phabricator_www_root : string = "/var/www" option phabricator_mysql_config : string = "/etc/mysql/debian.cnf" option phabricator_apache_root : string = "/etc/apache2" option phabricator_smtp_host : string = "" option phabricator_smtp_port : int = 465 option phabricator_smtp_user : string = "" option phabricator_smtp_passwd : string = "" option phabricator_smtp_protocol : string = "ssl" option phabricator_smtp_message_id : bool = true section "Isabelle/Scala/ML system channel" option system_channel_address : string = "" option system_channel_password : string = "" 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,277 +1,356 @@ /* Title: Pure/Tools/phabricator.scala Author: Makarius Support for Phabricator server. 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 daemon_user = "phabricator" + + val ssh_standard = 22 + val ssh_alternative1 = 222 + val ssh_alternative2 = 2222 + + + /* installation parameters */ + val default_name = "vcs" def default_prefix(name: String): String = "phabricator-" + name def default_root(options: Options, name: String): Path = Path.explode(options.string("phabricator_www_root")) + Path.basic(default_prefix(name)) def default_repo(options: Options, name: String): Path = default_root(options, name) + Path.basic("repo") - 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") - /** global configuration **/ val global_config = Path.explode("/etc/isabelle-phabricator.conf") sealed case class Config(name: String, root: Path) { def home: Path = root + Path.explode("phabricator") def execute(command: String): Process_Result = Isabelle_System.bash("./bin/" + command, cwd = home.file).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)) /** setup **/ + def user_setup(name: String, description: String, ssh_setup: Boolean = false) + { + if (!Linux.user_exists(name)) { + Linux.user_add(name, description = description, 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( options: Options, name: String = default_name, prefix: String = "", root: String = "", repo: String = "", package_update: Boolean = false, progress: Progress = No_Progress) { /* system environment */ Linux.check_system_root() 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") + + val www_user = options.string("phabricator_www_user") + + /* basic installation */ val prefix_name = proper_string(prefix) getOrElse default_prefix(name) val root_path = if (root.nonEmpty) Path.explode(root) else default_root(options, name) val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(options, 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(options.string("phabricator_www_user")) + """ . + chown """ + 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)) /* MySQL setup */ progress.echo("MySQL setup...") def mysql_conf(R: Regex): Option[String] = split_lines(File.read(Path.explode(options.string("phabricator_mysql_config")))). 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(prefix_name.replace("-", "_"))) config.execute("storage upgrade --force") + /* PHP daemon */ + + progress.echo("PHP daemon setup...") + + config.execute("config set phd.user " + Bash.string(daemon_user)) + + Linux.service_install("phd-" + prefix_name, +"""[Unit] +Description=PHP daemon (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=""" + root_path.expand.implode + """/phabricator/bin/phd start +ExecStop=""" + root_path.expand.implode + """/phabricator/bin/phd stop +RemainAfterExit=yes + +[Install] +WantedBy=multi-user.target +""") + + + /* SSH hosting */ + + progress.echo("SSH 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(prefix_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 + + /* Apache setup */ progress.echo("Apache setup...") val apache_root = Path.explode(options.string("phabricator_apache_root")) val apache_sites = apache_root + Path.explode("sites-available") if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites) File.write(apache_sites + Path.basic(prefix_name + ".conf"), """ #ServerName: "lvh.me" is an alias for "localhost" for testing ServerName """ + prefix_name + """.lvh.me 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(prefix_name) + """ systemctl restart apache2 """).check progress.echo("\nDONE\nWeb configuration via http://" + prefix_name + ".lvh.me") } /* Isabelle tool wrapper */ val isabelle_tool1 = Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", args => { var repo = "" var package_update = false var options = Options.init() var prefix = "" var root = "" val getopts = Getopts(""" Usage: isabelle phabricator_setup [OPTIONS] [NAME] Options are: -R DIR repository directory (default: """ + default_repo(options, "NAME") + """) -U full update of system packages before installation -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p PREFIX prefix for derived names (default: """ + default_prefix("NAME") + """) -r DIR installation root directory (default: """ + default_root(options, "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." The installation NAME (default: """ + quote(default_name) + """) is mapped to a regular Unix user and used for public SSH access. """, "R:" -> (arg => repo = arg), "U" -> (_ => package_update = true), "o:" -> (arg => options = options + arg), "p:" -> (arg => prefix = arg), "r:" -> (arg => root = arg)) val more_args = getopts(args) val name = more_args match { case Nil => default_name case List(name) => name case _ => getopts.usage() } val progress = new Console_Progress phabricator_setup(options, name, prefix = prefix, root = root, repo = repo, package_update = package_update, progress = progress) }) /** update **/ def phabricator_update(name: String, progress: Progress = No_Progress) { Linux.check_system_root() ??? } /* Isabelle tool wrapper */ val isabelle_tool2 = Isabelle_Tool("phabricator_update", "update Phabricator server installation", args => { val getopts = Getopts(""" Usage: isabelle phabricator_update [NAME] Update Phabricator installation, with lookup of NAME (default + """ + quote(default_name) + """) in """ + global_config + "\n") val more_args = getopts(args) val name = more_args match { case Nil => default_name case List(name) => name case _ => getopts.usage() } val progress = new Console_Progress phabricator_update(name, progress = progress) }) }