diff --git a/etc/options b/etc/options --- a/etc/options +++ b/etc/options @@ -1,365 +1,349 @@ (* :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_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,408 +1,471 @@ /* Title: Pure/Tools/phabricator.scala Author: Makarius -Support for Phabricator server. See also: +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(options: Options, name: String): Path = - Path.explode(options.string("phabricator_www_root")) + - Path.basic(phabricator_name(name = name)) + def default_root(name: String): Path = + Path.explode("/var/www") + Path.basic(phabricator_name(name = name)) - def default_repo(options: Options, name: String): Path = - default_root(options, name) + Path.basic("repo") + def default_repo(name: String): Path = default_root(name) + Path.basic("repo") + + val mailers_path: Path = Path.explode("mailers.json") + + 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 + } + } +]""" /** 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).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, 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( - options: Options, name: String = default_name, 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 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 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("MySQL 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(options.string("phabricator_mysql_config")))). - collectFirst({ case R(a) => a }) + 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") config.execute("storage upgrade --force") /* 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(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(options.string("phabricator_apache_root")) + 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 """) + /* mail configuration */ + + val mail_config = config.home + mailers_path + + progress.echo("Template for mail configuration: " + mail_config) + + File.write(mail_config, mailers_template) + + progress.echo("\nDONE\nWeb configuration via " + server_url) } /* 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 root = "" val getopts = Getopts(""" Usage: isabelle phabricator_setup [OPTIONS] [NAME] Options are: - -R DIR repository directory (default: """ + default_repo(options, "NAME") + """) + -R DIR repository directory (default: """ + default_repo("NAME") + """) -U full update of system packages before installation - -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -r DIR installation root directory (default: """ + default_root(options, "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." 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), "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, root = root, repo = repo, + phabricator_setup(name, root = root, repo = repo, package_update = package_update, progress = progress) }) - /** update **/ + /** setup mail **/ - def phabricator_update(name: String, progress: Progress = No_Progress) + 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.home + mailers_path + + 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 """ + + Bash.string(test_user)).check + } + } + + if (config_file.isEmpty) { + if (!default_config_file.is_file) File.write(default_config_file, mailers_template) + if (File.read(default_config_file) == mailers_template) { + progress.echo( + "Please invoke the tool again, after providing details in\n " + default_config_file) + } + else setup_mail + } + else setup_mail } /* Isabelle tool wrapper */ val isabelle_tool2 = - Isabelle_Tool("phabricator_update", "update Phabricator server installation", args => + 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_update [NAME] +Usage: isabelle phabricator_setup_mail [OPTIONS] - Update Phabricator installation, with lookup of NAME (default + """ + quote(default_name) + """) - in """ + global_config + "\n") + Options are: + -T USER send test mail to Phabricator user + -f FILE config file (default: """ + mailers_path + """ within installation home) + -n NAME Phabricator installation name (default: """ + quote(default_name) + """) + + Provide mail configuration for existing Phabricator installation. See also + https://secure.phabricator.com/book/phabricator/article/configuring_outbound_email + (notably section "Mailer: SMTP"). +""", + "T:" -> (arg => test_user = arg), + "f:" -> (arg => config_file = Some(Path.explode(arg))), + "n:" -> (arg => name = arg)) val more_args = getopts(args) - val name = - more_args match { - case Nil => default_name - case List(name) => name - case _ => getopts.usage() - } + if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress - phabricator_update(name, progress = progress) + phabricator_setup_mail(name = name, config_file = config_file, + test_user = test_user, progress = progress) }) }