diff --git a/src/Pure/Admin/build_history.scala b/src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala +++ b/src/Pure/Admin/build_history.scala @@ -1,618 +1,618 @@ /* Title: Pure/Admin/build_history.scala Author: Makarius Build other history versions. */ package isabelle object Build_History { /* log files */ val engine = "build_history" val log_prefix = engine + "_" /* augment settings */ def augment_settings( other_isabelle: Other_Isabelle, threads: Int, arch_64: Boolean, heap: Int, max_heap: Option[Int], more_settings: List[String]): String = { val (ml_platform, ml_settings) = { val windows_32 = "x86-windows" val windows_64 = "x86_64-windows" val windows_64_32 = "x86_64_32-windows" val platform_32 = other_isabelle.getenv("ISABELLE_PLATFORM32") val platform_64 = other_isabelle.getenv("ISABELLE_PLATFORM64") val platform_64_32 = platform_64.replace("x86_64-", "x86_64_32-") val polyml_home = try { Path.explode(other_isabelle.getenv("ML_HOME")).dir } catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) } def ml_home(platform: String): Path = polyml_home + Path.explode(platform) def err(platform: String): Nothing = error("Platform " + platform + " unavailable on this machine") def check_dir(platform: String): Boolean = platform != "" && ml_home(platform).is_dir val ml_platform = if (Platform.is_windows && arch_64) { if (check_dir(windows_64)) windows_64 else err(windows_64) } else if (Platform.is_windows && !arch_64) { if (check_dir(windows_64_32)) windows_64_32 else if (check_dir(windows_32)) windows_32 else platform_32 // x86-cygwin } else if (arch_64) { if (check_dir(platform_64)) platform_64 else err(platform_64) } else if (check_dir(platform_64_32)) platform_64_32 else platform_32 val ml_options = "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") + " --gcthreads " + threads + (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "") (ml_platform, List( "ML_HOME=" + File.bash_path(ml_home(ml_platform)), "ML_PLATFORM=" + quote(ml_platform), "ML_OPTIONS=" + quote(ml_options))) } val thread_settings = List( "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"", "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"") val settings = List(ml_settings, thread_settings) ::: (if (more_settings.isEmpty) Nil else List(more_settings)) File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_)))) ml_platform } /** build_history **/ private val default_user_home = Path.USER_HOME private val default_rev = "tip" private val default_multicore = (1, 1) private val default_heap = 1500 private val default_isabelle_identifier = "build_history" def build_history( options: Options, root: Path, user_home: Path = default_user_home, progress: Progress = new Progress, rev: String = default_rev, afp_rev: Option[String] = None, afp_partition: Int = 0, isabelle_identifier: String = default_isabelle_identifier, ml_statistics_step: Int = 1, component_repository: String = Components.default_component_repository, components_base: Path = Components.default_components_base, fresh: Boolean = false, hostname: String = "", multicore_base: Boolean = false, multicore_list: List[(Int, Int)] = List(default_multicore), arch_64: Boolean = false, heap: Int = default_heap, max_heap: Option[Int] = None, init_settings: List[String] = Nil, more_settings: List[String] = Nil, more_preferences: List[String] = Nil, verbose: Boolean = false, build_tags: List[String] = Nil, build_args: List[String] = Nil): List[(Process_Result, Path)] = { /* sanity checks */ if (File.eq(Path.ISABELLE_HOME, root)) error("Repository coincides with ISABELLE_HOME=" + Path.ISABELLE_HOME.expand) for ((threads, _) <- multicore_list if threads < 1) error("Bad threads value < 1: " + threads) for ((_, processes) <- multicore_list if processes < 1) error("Bad processes value < 1: " + processes) if (heap < 100) error("Bad heap value < 100: " + heap) if (max_heap.isDefined && max_heap.get < heap) error("Bad max_heap value < heap: " + max_heap.get) System.getenv("ISABELLE_SETTINGS_PRESENT") match { case null | "" => case _ => error("Cannot run build_history within existing Isabelle settings environment") } /* checkout Isabelle + AFP repository */ def checkout(dir: Path, version: String): String = { val hg = Mercurial.repository(dir) hg.update(rev = version, clean = true) progress.echo_if(verbose, hg.log(version, options = "-l1")) hg.id(rev = version) } val isabelle_version = checkout(root, rev) val afp_repos = root + Path.explode("AFP") val afp_version = afp_rev.map(checkout(afp_repos, _)) val (afp_build_args, afp_sessions) = if (afp_rev.isEmpty) (Nil, Nil) else { val (opt, sessions) = try { val afp = AFP.init(options, afp_repos) ("-d", afp.partition(afp_partition)) } catch { case ERROR(_) => ("-D", Nil) } (List(opt, "~~/AFP/thys"), sessions) } /* main */ val other_isabelle = Other_Isabelle(root, isabelle_identifier = isabelle_identifier, user_home = user_home, progress = progress) val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname() val build_history_date = Date.now() val build_group_id = build_host + ":" + build_history_date.time.ms var first_build = true for ((threads, processes) <- multicore_list) yield { /* init settings */ val component_settings = other_isabelle.init_components( component_repository = component_repository, components_base = components_base, catalogs = List("main", "optional")) other_isabelle.init_settings(component_settings ::: init_settings) other_isabelle.resolve_components(echo = verbose) val ml_platform = augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings) File.write(other_isabelle.etc_preferences, cat_lines(more_preferences)) val isabelle_output = other_isabelle.isabelle_home_user + Path.explode("heaps") + Path.explode(other_isabelle.getenv("ML_IDENTIFIER")) val isabelle_output_log = isabelle_output + Path.explode("log") val isabelle_base_log = isabelle_output + Path.explode("../base_log") if (first_build) { other_isabelle.resolve_components(echo = verbose) if (fresh) Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes")) other_isabelle.bash( "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " + "bin/isabelle jedit -b", redirect = true, echo = verbose).check for { tool <- List("ghc_setup", "ocaml_setup") if other_isabelle.getenv("ISABELLE_" + Word.uppercase(tool)) == "true" && (other_isabelle.isabelle_home + Path.explode("lib/Tools/" + tool)).is_file } other_isabelle(tool, echo = verbose) Isabelle_System.rm_tree(isabelle_base_log) } Isabelle_System.rm_tree(isabelle_output) Isabelle_System.make_directory(isabelle_output) val log_path = other_isabelle.isabelle_home_user + Build_Log.log_subdir(build_history_date) + Build_Log.log_filename(Build_History.engine, build_history_date, List(build_host, ml_platform, "M" + threads) ::: build_tags) Isabelle_System.make_directory(log_path.dir) val build_out = other_isabelle.isabelle_home_user + Path.explode("log/build.out") val build_out_progress = new File_Progress(build_out) build_out.file.delete /* build */ if (multicore_base && !first_build && isabelle_base_log.is_dir) Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log) val build_start = Date.now() val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args val build_isabelle = Other_Isabelle(root, isabelle_identifier = isabelle_identifier, user_home = user_home, progress = build_out_progress) val build_result = build_isabelle("build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true, strict = false) val build_end = Date.now() val build_info: Build_Log.Build_Info = Build_Log.Log_File(log_path.file_name, build_result.out_lines). parse_build_info(ml_statistics = true) /* output log */ val store = Sessions.store(options + "build_database_server=false") val meta_info = Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) ::: Properties.lines_nonempty(Build_Log.Prop.build_args.name, build_args1) ::: List( Build_Log.Prop.build_group_id.name -> build_group_id, Build_Log.Prop.build_id.name -> (build_host + ":" + build_start.time.ms), Build_Log.Prop.build_engine.name -> Build_History.engine, Build_Log.Prop.build_host.name -> build_host, Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start), Build_Log.Prop.build_end.name -> Build_Log.print_date(build_end), Build_Log.Prop.isabelle_version.name -> isabelle_version) ::: afp_version.map(Build_Log.Prop.afp_version.name -> _).toList build_out_progress.echo("Reading session build info ...") val session_build_info = build_info.finished_sessions.flatMap(session_name => { val database = isabelle_output + store.database(session_name) if (database.is_file) { using(SQLite.open_database(database))(db => { val theory_timings = try { store.read_theory_timings(db, session_name).map(ps => Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps)) } catch { case ERROR(_) => Nil } val session_sources = store.read_build(db, session_name).map(_.sources) match { case Some(sources) if sources.length == SHA1.digest_length => List("Sources " + session_name + " " + sources) case _ => Nil } theory_timings ::: session_sources }) } else Nil }) build_out_progress.echo("Reading ML statistics ...") val ml_statistics = build_info.finished_sessions.flatMap(session_name => { val database = isabelle_output + store.database(session_name) val log_gz = isabelle_output + store.log_gz(session_name) val properties = if (database.is_file) { using(SQLite.open_database(database))(db => store.read_ml_statistics(db, session_name)) } else if (log_gz.is_file) { Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics } else Nil val trimmed_properties = if (ml_statistics_step <= 0) Nil else if (ml_statistics_step == 1) properties else { (for { (ps, i) <- properties.iterator.zipWithIndex if i % ml_statistics_step == 0 } yield ps).toList } trimmed_properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps) }) build_out_progress.echo("Reading error messages ...") val session_errors = build_info.failed_sessions.flatMap(session_name => { val database = isabelle_output + store.database(session_name) val errors = if (database.is_file) { try { using(SQLite.open_database(database))(db => store.read_errors(db, session_name)) } // column "errors" could be missing catch { case _: java.sql.SQLException => Nil } } else Nil errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg)) }) build_out_progress.echo("Reading heap sizes ...") val heap_sizes = build_info.finished_sessions.flatMap(session_name => { val heap = isabelle_output + Path.explode(session_name) if (heap.is_file) Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)") else None }) build_out_progress.echo("Writing log file " + log_path.xz + " ...") File.write_xz(log_path.xz, terminate_lines( Protocol.Meta_Info_Marker(meta_info) :: build_result.out_lines ::: session_build_info ::: ml_statistics.map(Protocol.ML_Statistics_Marker.apply) ::: session_errors.map(Protocol.Error_Message_Marker.apply) ::: heap_sizes), XZ.options(6)) /* next build */ if (multicore_base && first_build && isabelle_output_log.is_dir) Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log) Isabelle_System.rm_tree(isabelle_output) first_build = false (build_result, log_path.xz) } } /* command line entry point */ private object Multicore { private val Pat1 = """^(\d+)$""".r private val Pat2 = """^(\d+)x(\d+)$""".r def parse(s: String): (Int, Int) = s match { case Pat1(Value.Int(x)) => (x, 1) case Pat2(Value.Int(x), Value.Int(y)) => (x, y) case _ => error("Bad multicore configuration: " + quote(s)) } } def main(args: Array[String]): Unit = { Command_Line.tool { var afp_rev: Option[String] = None var multicore_base = false var components_base: Path = Components.default_components_base var heap: Option[Int] = None var max_heap: Option[Int] = None var multicore_list = List(default_multicore) var isabelle_identifier = default_isabelle_identifier var afp_partition = 0 var component_repository = Components.default_component_repository var more_settings: List[String] = Nil var more_preferences: List[String] = Nil var fresh = false var hostname = "" var init_settings: List[String] = Nil var arch_64 = false var output_file = "" var rev = default_rev var ml_statistics_step = 1 var build_tags = List.empty[String] var user_home = default_user_home var verbose = false var exit_code = false val getopts = Getopts(""" Usage: Admin/build_history [OPTIONS] REPOSITORY [ARGS ...] Options are: -A REV include $ISABELLE_HOME/AFP repository at given revision -B first multicore build serves as base for scheduling information -C DIR base directory for Isabelle components (default: """ + Components.default_components_base + """) -H SIZE minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64) -M MULTICORE multicore configurations (see below) -N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """) -P NUMBER AFP partition number (0, 1, 2, default: 0=unrestricted) -R URL remote repository for Isabelle components (default: """ + Components.default_component_repository + """) -U SIZE maximal ML heap in MB (default: unbounded) -e TEXT additional text for generated etc/settings -f fresh build of Isabelle/Scala components (recommended) -h NAME override local hostname -i TEXT initial text for generated etc/settings -m ARCH processor architecture (32=x86, 64=x86_64, default: x86) -o FILE output file for log names (default: stdout) -p TEXT additional text for generated etc/preferences -r REV update to revision (default: """ + default_rev + """) -s NUMBER step size for ML statistics (0=none, 1=all, n=step, default: 1) -t TAG free-form build tag (multiple occurrences possible) -u DIR alternative USER_HOME directory -v verbose -x return overall exit code from build processes Build Isabelle sessions from the history of another REPOSITORY clone, passing ARGS directly to its isabelle build tool. Each MULTICORE configuration consists of one or two numbers (default 1): THREADS or THREADSxPROCESSES, e.g. -M 1,2,4 or -M 1x4,2x2,4. """, "A:" -> (arg => afp_rev = Some(arg)), "B" -> (_ => multicore_base = true), "C:" -> (arg => components_base = Path.explode(arg)), "H:" -> (arg => heap = Some(Value.Int.parse(arg))), "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)), "N:" -> (arg => isabelle_identifier = arg), "P:" -> (arg => afp_partition = Value.Int.parse(arg)), "R:" -> (arg => component_repository = arg), "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))), "e:" -> (arg => more_settings = more_settings ::: List(arg)), "f" -> (_ => fresh = true), "h:" -> (arg => hostname = arg), "i:" -> (arg => init_settings = init_settings ::: List(arg)), "m:" -> { case "32" | "x86" => arch_64 = false case "64" | "x86_64" => arch_64 = true case bad => error("Bad processor architecture: " + quote(bad)) }, "o:" -> (arg => output_file = arg), "p:" -> (arg => more_preferences = more_preferences ::: List(arg)), "r:" -> (arg => rev = arg), "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)), "t:" -> (arg => build_tags = build_tags ::: List(arg)), "u:" -> (arg => user_home = Path.explode(arg)), "v" -> (_ => verbose = true), "x" -> (_ => exit_code = true)) val more_args = getopts(args) val (root, build_args) = more_args match { case root :: build_args => (Path.explode(root), build_args) case _ => getopts.usage() } val progress = new Console_Progress(stderr = true) val results = build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev, afp_rev = afp_rev, afp_partition = afp_partition, isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step, component_repository = component_repository, components_base = components_base, fresh = fresh, hostname = hostname, multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64, heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap), max_heap = max_heap, init_settings = init_settings, more_settings = more_settings, more_preferences = more_preferences, verbose = verbose, build_tags = build_tags, build_args = build_args) if (output_file == "") { for ((_, log_path) <- results) Output.writeln(log_path.implode, stdout = true) } else { File.write(Path.explode(output_file), cat_lines(for ((_, log_path) <- results) yield log_path.implode)) } val rc = results.foldLeft(0) { case (rc, (res, _)) => rc max res.rc } if (rc != 0 && exit_code) sys.exit(rc) } } /** remote build_history -- via command-line **/ def remote_build_history( ssh: SSH.Session, isabelle_repos_self: Path, isabelle_repos_other: Path, - isabelle_repository: Mercurial.Address = Isabelle_System.isabelle_repository, - afp_repository: Mercurial.Address = Isabelle_System.afp_repository, + isabelle_repository: Mercurial.Server = Isabelle_System.isabelle_repository, + afp_repository: Mercurial.Server = Isabelle_System.afp_repository, isabelle_identifier: String = "remote_build_history", self_update: Boolean = false, progress: Progress = new Progress, rev: String = "", afp_rev: Option[String] = None, options: String = "", args: String = ""): List[(String, Bytes)] = { /* Isabelle self repository */ val self_hg = - Mercurial.setup_repository(isabelle_repository, isabelle_repos_self, ssh = ssh) + Mercurial.setup_repository(isabelle_repository.root, isabelle_repos_self, ssh = ssh) def execute(cmd: String, args: String, echo: Boolean = false, strict: Boolean = true): Unit = ssh.execute( Isabelle_System.export_isabelle_identifier(isabelle_identifier) + ssh.bash_path(isabelle_repos_self + Path.explode(cmd)) + " " + args, progress_stdout = progress.echo_if(echo, _), progress_stderr = progress.echo_if(echo, _), strict = strict).check if (self_update) { val hg = Mercurial.repository(Path.ISABELLE_HOME) hg.push(self_hg.root_url, force = true) self_hg.update(rev = hg.parent(), clean = true) execute("bin/isabelle", "components -I") execute("bin/isabelle", "components -a", echo = true) execute("Admin/build", "jars_fresh") } val rev_id = self_hg.id(rev) /* Isabelle other + AFP repository */ if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) { ssh.rm_tree(isabelle_repos_other) } Mercurial.clone_repository( ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev_id, ssh = ssh) val afp_options = if (afp_rev.isEmpty) "" else { val afp_repos = isabelle_repos_other + Path.explode("AFP") - Mercurial.setup_repository(afp_repository, afp_repos, ssh = ssh) + Mercurial.setup_repository(afp_repository.root, afp_repos, ssh = ssh) " -A " + Bash.string(afp_rev.get) } /* Admin/build_history */ ssh.with_tmp_dir(tmp_dir => { val output_file = tmp_dir + Path.explode("output") val rev_options = if (rev == "") "" else " -r " + Bash.string(rev_id) try { execute("Admin/build_history", "-o " + ssh.bash_path(output_file) + rev_options + afp_options + " " + options + " " + ssh.bash_path(isabelle_repos_other) + " " + args, echo = true, strict = false) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for build_bistory " + rev_options + afp_options) } for (line <- split_lines(ssh.read(output_file))) yield { val log = Path.explode(line) val bytes = ssh.read_bytes(log) ssh.rm(log) (log.file_name, bytes) } }) } } diff --git a/src/Pure/Admin/isabelle_cronjob.scala b/src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala +++ b/src/Pure/Admin/isabelle_cronjob.scala @@ -1,634 +1,634 @@ /* Title: Pure/Admin/isabelle_cronjob.scala Author: Makarius Main entry point for administrative cronjob at TUM. */ package isabelle import java.nio.file.Files import scala.annotation.tailrec object Isabelle_Cronjob { /* global resources: owned by main cronjob */ val backup = "lxbroy10:cronjob" val main_dir: Path = Path.explode("~/cronjob") val main_state_file: Path = main_dir + Path.explode("run/main.state") val current_log: Path = main_dir + Path.explode("run/main.log") // owned by log service val cumulative_log: Path = main_dir + Path.explode("log/main.log") // owned by log service val isabelle_repos: Path = main_dir + Path.explode("isabelle") val afp_repos: Path = main_dir + Path.explode("AFP") val mailman_archives_dir = Path.explode("~/cronjob/Mailman") val build_log_dirs = List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log")) /** logger tasks **/ sealed case class Logger_Task(name: String = "", body: Logger => Unit) /* init and exit */ def get_rev(): String = Mercurial.repository(isabelle_repos).id() def get_afp_rev(): String = Mercurial.repository(afp_repos).id() val init: Logger_Task = Logger_Task("init", logger => { Isabelle_Devel.make_index() - Mercurial.setup_repository(Isabelle_System.isabelle_repository, isabelle_repos) - Mercurial.setup_repository(Isabelle_System.afp_repository, afp_repos) + Mercurial.setup_repository(Isabelle_System.isabelle_repository.root, isabelle_repos) + Mercurial.setup_repository(Isabelle_System.afp_repository.root, afp_repos) File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date), Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev()))) Isabelle_System.bash( """rsync -a --include="*/" --include="plain_identify*" --exclude="*" """ + Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check if (!Isabelle_Devel.cronjob_log.is_file) Files.createSymbolicLink(Isabelle_Devel.cronjob_log.file.toPath, current_log.file.toPath) }) val exit: Logger_Task = Logger_Task("exit", logger => { Isabelle_System.bash( "rsync -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.") .check }) /* Mailman archives */ val mailman_archives: Logger_Task = Logger_Task("mailman_archives", logger => { Mailman.isabelle_users.download(mailman_archives_dir) Mailman.isabelle_dev.download(mailman_archives_dir) }) /* build release */ val build_release: Logger_Task = Logger_Task("build_release", logger => { Isabelle_Devel.release_snapshot(logger.options, rev = get_rev(), afp_rev = get_afp_rev()) }) /* remote build_history */ sealed case class Item( known: Boolean, isabelle_version: String, afp_version: Option[String], pull_date: Date) { def unknown: Boolean = !known def versions: (String, Option[String]) = (isabelle_version, afp_version) def known_versions(rev: String, afp_rev: Option[String]): Boolean = known && rev != "" && isabelle_version == rev && (afp_rev.isEmpty || afp_rev.get != "" && afp_version == afp_rev) } def recent_items(db: SQL.Database, days: Int, rev: String, afp_rev: Option[String], sql: SQL.Source): List[Item] = { val afp = afp_rev.isDefined val select = Build_Log.Data.select_recent_versions( days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql) db.using_statement(select)(stmt => stmt.execute_query().iterator(res => { val known = res.bool(Build_Log.Data.known) val isabelle_version = res.string(Build_Log.Prop.isabelle_version) val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None val pull_date = res.date(Build_Log.Data.pull_date(afp)) Item(known, isabelle_version, afp_version, pull_date) }).toList) } def unknown_runs(items: List[Item]): List[List[Item]] = { val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known)) if (run.nonEmpty) run :: unknown_runs(rest) else Nil } sealed case class Remote_Build( description: String, host: String, actual_host: String = "", user: String = "", port: Int = 0, proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, self_update: Boolean = false, historic: Boolean = false, history: Int = 0, history_base: String = "build_history_base", java_heap: String = "", options: String = "", args: String = "", afp: Boolean = false, bulky: Boolean = false, more_hosts: List[String] = Nil, detect: SQL.Source = "", active: Boolean = true) { def ssh_session(context: SSH.Context): SSH.Session = context.open_session(host = host, user = user, port = port, actual_host = actual_host, proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port, permissive = proxy_host.nonEmpty) def sql: SQL.Source = Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine) + " AND " + SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) + (if (detect == "") "" else " AND " + SQL.enclose(detect)) def profile: Build_Status.Profile = Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql) def pick( options: Options, rev: String = "", filter: Item => Boolean = _ => true): Option[(String, Option[String])] = { val afp_rev = if (afp) Some(get_afp_rev()) else None val store = Build_Log.store(options) using(store.open_database())(db => { def pick_days(days: Int, gap: Int): Option[(String, Option[String])] = { val items = recent_items(db, days, rev, afp_rev, sql).filter(filter) def runs = unknown_runs(items).filter(run => run.length >= gap) if (historic || items.exists(_.known_versions(rev, afp_rev))) { val longest_run = runs.foldLeft(List.empty[Item]) { case (item1, item2) => if (item1.length >= item2.length) item1 else item2 } if (longest_run.isEmpty) None else Some(longest_run(longest_run.length / 2).versions) } else if (rev != "") Some((rev, afp_rev)) else runs.flatten.headOption.map(_.versions) } pick_days(options.int("build_log_history") max history, 2) orElse pick_days(200, 5) orElse pick_days(2000, 1) }) } def build_history_options: String = " -h " + Bash.string(host) + " " + (java_heap match { case "" => "" case h => "-e 'ISABELLE_TOOL_JAVA_OPTIONS=\"$ISABELLE_TOOL_JAVA_OPTIONS -Xmx" + h + "\"' " }) + options } val remote_builds_old: List[Remote_Build] = List( Remote_Build("Linux A", "lxbroy9", java_heap = "2g", options = "-m32 -B -M1x2,2", args = "-N -g timing"), Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90, java_heap = "2g", options = "-m32 -B -M1x2,2 -t Benchmarks" + " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind -e ISABELLE_SMLNJ=sml" + " -e ISABELLE_SWIPL=swipl", args = "-N -a -d '~~/src/Benchmarks'", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("Benchmarks")), Remote_Build("macOS 10.14 Mojave (Old)", "lapnipkow3", options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true -p pide_session=false", self_update = true, args = "-a -d '~~/src/Benchmarks'"), Remote_Build("AFP old bulky", "lrzcloud1", self_update = true, proxy_host = "lxbroy10", proxy_user = "i21isatest", options = "-m64 -M6 -U30000 -s10 -t AFP", args = "-g large -g slow", afp = true, bulky = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")), Remote_Build("AFP old", "lxbroy7", args = "-N -X large -X slow", afp = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")), Remote_Build("Poly/ML 5.7 Linux", "lxbroy8", history_base = "37074e22e8be", options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'", args = "-N -g timing", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7") + " AND " + Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")), Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8", history_base = "a9d5b59c3e12", options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'", args = "-N -g timing", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), Remote_Build("Poly/ML 5.7 macOS", "macbroy2", history_base = "37074e22e8be", options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'", args = "-a", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7")), Remote_Build("Poly/ML 5.7.1 macOS", "macbroy2", history_base = "a9d5b59c3e12", options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'", args = "-a", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), Remote_Build("macOS", "macbroy2", options = "-m32 -M8" + " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_OPAM_ROOT=\"$ISABELLE_HOME/opam\"" + " -e ISABELLE_SMLNJ=/home/isabelle/smlnj/110.85/bin/sml" + " -p pide_session=false", args = "-a", detect = Build_Log.Prop.build_tags.undefined, history_base = "2c0f24e927dd"), Remote_Build("macOS, quick_and_dirty", "macbroy2", options = "-m32 -M8 -t quick_and_dirty -p pide_session=false", args = "-a -o quick_and_dirty", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty"), history_base = "2c0f24e927dd"), Remote_Build("macOS, skip_proofs", "macbroy2", options = "-m32 -M8 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"), history_base = "2c0f24e927dd"), Remote_Build("Poly/ML test", "lxbroy8", options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'", args = "-N -g timing", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-test")), Remote_Build("macOS 10.12 Sierra", "macbroy30", options = "-m32 -M2 -p pide_session=false", args = "-a", detect = Build_Log.Prop.build_start.toString + " > date '2017-03-03'"), Remote_Build("macOS 10.10 Yosemite", "macbroy31", options = "-m32 -M2 -p pide_session=false", args = "-a"), Remote_Build("macOS 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a", detect = Build_Log.Prop.build_start.toString + " < date '2017-03-03'")) ::: { for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) } yield { Remote_Build("AFP old", host = hosts.head, more_hosts = hosts.tail, options = "-m32 -M1x2 -t AFP -P" + n + " -e ISABELLE_GHC=ghc" + " -e ISABELLE_MLTON=mlton" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" + " -e ISABELLE_SMLNJ=sml", args = "-N -X large -X slow", afp = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")) } } val remote_builds1: List[List[Remote_Build]] = { List( List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90, options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), List(Remote_Build("macOS 10.13 High Sierra", "lapbroy68", options = "-m32 -B -M1,2,4 -e ISABELLE_GHC_SETUP=true -p pide_session=false", self_update = true, args = "-a -d '~~/src/Benchmarks'")), List( Remote_Build("macOS 11.1 Big Sur", "mini1", options = "-m32 -B -M1x2,2,4 -p pide_session=false" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_MLTON=/usr/local/bin/mlton" + " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" + " -e ISABELLE_SWIPL=/usr/local/bin/swipl", self_update = true, args = "-a -d '~~/src/Benchmarks'")), List( Remote_Build("macOS 10.14 Mojave", "mini2", options = "-m32 -B -M1x2,2,4 -p pide_session=false" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_MLTON=/usr/local/bin/mlton" + " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" + " -e ISABELLE_SWIPL=/usr/local/bin/swipl", self_update = true, args = "-a -d '~~/src/Benchmarks'"), Remote_Build("macOS, quick_and_dirty", "mini2", options = "-m32 -M4 -t quick_and_dirty -p pide_session=false", self_update = true, args = "-a -o quick_and_dirty", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty")), Remote_Build("macOS, skip_proofs", "mini2", options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"))), List(Remote_Build("macOS 10.15 Catalina", "laramac01", user = "makarius", proxy_host = "laraserver", proxy_user = "makarius", self_update = true, options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false", args = "-a -d '~~/src/Benchmarks'")), List( Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true, options = "-m32 -M4" + " -C /cygdrive/d/isatest/contrib" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml", args = "-a", detect = Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86-windows") + " OR " + Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64_32-windows")), Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true, options = "-m64 -M4" + " -C /cygdrive/d/isatest/contrib" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml", args = "-a", detect = Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86_64-windows")))) } val remote_builds2: List[List[Remote_Build]] = List( List( Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41", self_update = true, proxy_host = "lxbroy10", proxy_user = "i21isatest", java_heap = "8g", options = "-m32 -M1x6 -t AFP" + " -e ISABELLE_GHC=ghc" + " -e ISABELLE_MLTON=mlton" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" + " -e ISABELLE_SMLNJ=sml", args = "-a -X large -X slow", afp = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")), Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41", self_update = true, proxy_host = "lxbroy10", proxy_user = "i21isatest", java_heap = "8g", options = "-m64 -M8 -U30000 -s10 -t AFP", args = "-g large -g slow", afp = true, bulky = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")))) def remote_build_history(rev: String, afp_rev: Option[String], i: Int, r: Remote_Build) : Logger_Task = { val task_name = "build_history-" + r.host Logger_Task(task_name, logger => { using(r.ssh_session(logger.ssh_context))(ssh => { val results = Build_History.remote_build_history(ssh, isabelle_repos, isabelle_repos.ext(r.host), isabelle_identifier = "cronjob_build_history", self_update = r.self_update, rev = rev, afp_rev = afp_rev, options = " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) + " -R " + Bash.string(Components.default_component_repository) + " -C '$USER_HOME/.isabelle/contrib' -f " + r.build_history_options, args = "-o timeout=10800 " + r.args) for ((log_name, bytes) <- results) { logger.log(Date.now(), log_name) Bytes.write(logger.log_dir + Path.explode(log_name), bytes) } }) }) } val build_status_profiles: List[Build_Status.Profile] = (remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile) /** task logging **/ object Log_Service { def apply(options: Options, progress: Progress = new Progress): Log_Service = new Log_Service(SSH.init_context(options), progress) } class Log_Service private(val ssh_context: SSH.Context, progress: Progress) { current_log.file.delete private val thread: Consumer_Thread[String] = Consumer_Thread.fork("cronjob: logger", daemon = true)( consume = (text: String) => { // critical File.append(current_log, text + "\n") File.append(cumulative_log, text + "\n") progress.echo(text) true }) def shutdown(): Unit = { thread.shutdown() } val hostname: String = Isabelle_System.hostname() def log(date: Date, task_name: String, msg: String): Unit = if (task_name != "") thread.send( "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg) def start_logger(start_date: Date, task_name: String): Logger = new Logger(this, start_date, task_name) def run_task(start_date: Date, task: Logger_Task): Unit = { val logger = start_logger(start_date, task.name) val res = Exn.capture { task.body(logger) } val end_date = Date.now() val err = res match { case Exn.Res(_) => None case Exn.Exn(exn) => Output.writeln("Exception trace for " + quote(task.name) + ":") exn.printStackTrace() val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception" Some(first_line) } logger.log_end(end_date, err) } def fork_task(start_date: Date, task: Logger_Task): Task = new Task(task.name, run_task(start_date, task)) } class Logger private[Isabelle_Cronjob]( val log_service: Log_Service, val start_date: Date, val task_name: String) { def ssh_context: SSH.Context = log_service.ssh_context def options: Options = ssh_context.options def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg) def log_end(end_date: Date, err: Option[String]): Unit = { val elapsed_time = end_date.time - start_date.time val msg = (if (err.isEmpty) "finished" else "ERROR " + err.get) + (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)") log(end_date, msg) } val log_dir = Isabelle_System.make_directory(main_dir + Build_Log.log_subdir(start_date)) log(start_date, "started") } class Task private[Isabelle_Cronjob](name: String, body: => Unit) { private val future: Future[Unit] = Future.thread("cronjob: " + name) { body } def is_finished: Boolean = future.is_finished } /** cronjob **/ def cronjob(progress: Progress, exclude_task: Set[String]): Unit = { /* soft lock */ val still_running = try { Some(File.read(main_state_file)) } catch { case ERROR(_) => None } still_running match { case None | Some("") => case Some(running) => error("Isabelle cronjob appears to be still running: " + running) } /* log service */ val log_service = Log_Service(Options.init(), progress = progress) def run(start_date: Date, task: Logger_Task): Unit = log_service.run_task(start_date, task) def run_now(task: Logger_Task): Unit = run(Date.now(), task) /* structured tasks */ def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ => for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "") run_now(task)) def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ => { @tailrec def join(running: List[Task]): Unit = { running.partition(_.is_finished) match { case (Nil, Nil) => case (Nil, _ :: _) => Time.seconds(0.5).sleep; join(running) case (_ :: _, remaining) => join(remaining) } } val start_date = Date.now() val running = for (task <- tasks if !exclude_task(task.name)) yield log_service.fork_task(start_date, task) join(running) }) /* repository structure */ val hg = Mercurial.repository(isabelle_repos) val hg_graph = hg.graph() def history_base_filter(r: Remote_Build): Item => Boolean = { val base_rev = hg.id(r.history_base) val nodes = hg_graph.all_succs(List(base_rev)).toSet (item: Item) => nodes(item.isabelle_version) } /* main */ val main_start_date = Date.now() File.write(main_state_file, main_start_date.toString + " " + log_service.hostname) run(main_start_date, Logger_Task("isabelle_cronjob", logger => run_now( SEQ(List( init, PAR(List(mailman_archives, build_release)), PAR( List(remote_builds1, remote_builds2).map(remote_builds => SEQ(List( PAR(remote_builds.map(_.filter(_.active)).map(seq => SEQ( for { (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex) (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r)) } yield remote_build_history(rev, afp_rev, i, r)))), Logger_Task("jenkins_logs", _ => Jenkins.download_logs(logger.options, Jenkins.build_log_jobs, main_dir)), Logger_Task("build_log_database", logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)), Logger_Task("build_status", logger => Isabelle_Devel.build_status(logger.options)))))), exit))))) log_service.shutdown() main_state_file.file.delete } /** command line entry point **/ def main(args: Array[String]): Unit = { Command_Line.tool { var force = false var verbose = false var exclude_task = Set.empty[String] val getopts = Getopts(""" Usage: Admin/cronjob/main [OPTIONS] Options are: -f apply force to do anything -v verbose -x NAME exclude tasks with this name """, "f" -> (_ => force = true), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_task += arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = if (verbose) new Console_Progress() else new Progress if (force) cronjob(progress, exclude_task) else error("Need to apply force to do anything") } } } diff --git a/src/Pure/General/mercurial.scala b/src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala +++ b/src/Pure/General/mercurial.scala @@ -1,410 +1,438 @@ /* Title: Pure/General/mercurial.scala Author: Makarius Support for Mercurial repositories, with local or remote repository clone and working directory (via ssh connection). */ package isabelle import scala.annotation.tailrec import scala.collection.mutable object Mercurial { type Graph = isabelle.Graph[String, Unit] - /* HTTP server addresses */ + /* HTTP server */ - object Address + object Server { - def apply(root: String): Address = new Address(root) + def apply(root: String): Server = new Server(root) + + def start(root: Path): Server = + { + val hg = repository(root) + + val server_process = Future.promise[Bash.Process] + val server_root = Future.promise[String] + Isabelle_Thread.fork("hg") { + val process = + Exn.capture { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) } + server_process.fulfill_result(process) + Exn.release(process).result(progress_stdout = + line => if (!server_root.is_finished) { + server_root.fulfill(Library.try_unsuffix("/", line).getOrElse(line)) + }) + } + server_process.join + + new Server(server_root.join) { + override def close(): Unit = server_process.join.terminate() + } + } } - final class Address private(val root: String) + class Server private(val root: String) extends AutoCloseable { override def toString: String = root + def close(): Unit = () + def changeset(rev: String = "tip", raw: Boolean = false): String = root + (if (raw) "/raw-rev/" else "/rev/") + rev def file(path: Path, rev: String = "tip", raw: Boolean = false): String = root + (if (raw) "/raw-file/" else "/file/") + rev + "/" + path.expand.implode def archive(rev: String = "tip"): String = root + "/archive/" + rev + ".tar.gz" def read_changeset(rev: String = "tip"): String = Url.read(changeset(rev = rev, raw = true)) def read_file(path: Path, rev: String = "tip"): String = Url.read(file(path, rev = rev, raw = true)) def download_archive(rev: String = "tip", progress: Progress = new Progress): HTTP.Content = Isabelle_System.download(archive(rev = rev), progress = progress) def download_dir(dir: Path, rev: String = "tip", progress: Progress = new Progress): Unit = { Isabelle_System.new_directory(dir) Isabelle_System.with_tmp_file("rev", ext = ".tar.gz")(archive_path => { val content = download_archive(rev = rev, progress = progress) Bytes.write(archive_path, content.bytes) progress.echo("Unpacking " + rev + ".tar.gz") Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path) + " --strip-components=1", dir = dir, original_owner = true).check }) } } /* command-line syntax */ def optional(s: String, prefix: String = ""): String = if (s == "") "" else " " + prefix + " " + Bash.string(s) def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else "" def opt_rev(s: String): String = optional(s, "--rev") def opt_template(s: String): String = optional(s, "--template") /* repository archives */ private val Archive_Node = """^node: (\S{12}).*$""".r private val Archive_Tag = """^tag: (\S+).*$""".r sealed case class Archive_Info(lines: List[String]) { def id: Option[String] = lines.collectFirst({ case Archive_Node(a) => a }) def tags: List[String] = for (Archive_Tag(tag) <- lines if tag != "tip") yield tag } def archive_info(root: Path): Option[Archive_Info] = { val path = root + Path.explode(".hg_archival.txt") if (path.is_file) Some(Archive_Info(Library.trim_split_lines(File.read(path)))) else None } def archive_id(root: Path): Option[String] = archive_info(root).flatMap(_.id) def archive_tags(root: Path): Option[String] = archive_info(root).map(info => info.tags.mkString(" ")) /* repository access */ def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean = ssh.is_dir(root + Path.explode(".hg")) && new Repository(root, ssh).command("root").ok def repository(root: Path, ssh: SSH.System = SSH.Local): Repository = { val hg = new Repository(root, ssh) hg.command("root").check hg } def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] = { @tailrec def find(root: Path): Option[Repository] = if (is_repository(root, ssh)) Some(repository(root, ssh = ssh)) else if (root.is_root) None else find(root + Path.parent) find(ssh.expand_path(start)) } private def make_repository(root: Path, cmd: String, args: String, ssh: SSH.System = SSH.Local) : Repository = { val hg = new Repository(root, ssh) ssh.make_directory(hg.root.dir) hg.command(cmd, args, repository = false).check hg } def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository = make_repository(root, "init", ssh.bash_path(root), ssh = ssh) def clone_repository(source: String, root: Path, rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository = make_repository(root, "clone", options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh) - def setup_repository(address: Address, root: Path, ssh: SSH.System = SSH.Local): Repository = + def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository = { - val source = address.root if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg } else clone_repository(source, root, options = "--noupdate", ssh = ssh) } class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local) { hg => val root: Path = ssh.expand_path(root_path) def root_url: String = ssh.hg_url + root.implode override def toString: String = ssh.hg_url + root.implode - def command(name: String, args: String = "", options: String = "", - repository: Boolean = true): Process_Result = + def command_line(name: String, args: String = "", options: String = "", + repository: Boolean = true): String = { - val cmdline = - "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") + - (if (repository) " --repository " + ssh.bash_path(root) else "") + - " --noninteractive " + name + " " + options + " " + args - ssh.execute(cmdline) + "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") + + (if (repository) " --repository " + ssh.bash_path(root) else "") + + " --noninteractive " + name + " " + options + " " + args + } + + def command( + name: String, args: String = "", options: String = "", + repository: Boolean = true): Process_Result = + { + ssh.execute(command_line(name, args = args, options = options, repository = repository)) } def add(files: List[Path]): Unit = hg.command("add", files.map(ssh.bash_path).mkString(" ")) def archive(target: String, rev: String = "", options: String = ""): Unit = hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check def heads(template: String = "{node|short}\n", options: String = ""): List[String] = hg.command("heads", opt_template(template), options).check.out_lines def identify(rev: String = "tip", options: String = ""): String = hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse "" def id(rev: String = "tip"): String = identify(rev, options = "-i") def tags(rev: String = "tip"): String = { val result = identify(rev, options = "-t") Library.space_explode(' ', result).filterNot(_ == "tip").mkString(" ") } def paths(args: String = "", options: String = ""): List[String] = hg.command("paths", args = args, options = options).check.out_lines def manifest(rev: String = "", options: String = ""): List[String] = hg.command("manifest", opt_rev(rev), options).check.out_lines def log(rev: String = "", template: String = "", options: String = ""): String = hg.command("log", opt_rev(rev) + opt_template(template), options).check.out def parent(): String = log(rev = "p1()", template = "{node|short}") def push( remote: String = "", rev: String = "", force: Boolean = false, options: String = ""): Unit = { hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options). check_rc(rc => rc == 0 | rc == 1) } def pull(remote: String = "", rev: String = "", options: String = ""): Unit = hg.command("pull", opt_rev(rev) + optional(remote), options).check def update( rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = ""): Unit = { hg.command("update", opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check } def known_files(): List[String] = hg.command("status", options = "--modified --added --clean --no-status").check.out_lines def graph(): Graph = { val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r val log_result = log(template = """node: {node|short} {p1node|short} {p2node|short}\n""") split_lines(log_result).foldLeft(Graph.string[Unit]) { case (graph, Node(x, y, z)) => val deps = List(y, z).filterNot(s => s.forall(_ == '0')) val graph1 = (x :: deps).foldLeft(graph)(_.default_node(_, ())) deps.foldLeft(graph1)({ case (g, dep) => g.add_edge(dep, x) }) case (graph, _) => graph } } } /* check files */ def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) = { val outside = new mutable.ListBuffer[Path] val unknown = new mutable.ListBuffer[Path] @tailrec def check(paths: List[Path]): Unit = { paths match { case path :: rest => find_repository(path, ssh) match { case None => outside += path; check(rest) case Some(hg) => val known = hg.known_files().iterator.map(name => (hg.root + Path.explode(name)).canonical_file).toSet if (!known(path.canonical_file)) unknown += path check(rest.filterNot(p => known(p.canonical_file))) } case Nil => } } check(files) (outside.toList, unknown.toList) } /* setup remote vs. local repository */ private def edit_hgrc(local_hg: Repository, path_name: String, source: String): Unit = { val hgrc = local_hg.root + Path.explode(".hg/hgrc") def header(line: String): Boolean = line.startsWith("[paths]") val Entry = """^(\S+)\s*=\s*(.*)$""".r val new_entry = path_name + " = " + source def commit(lines: List[String]): Boolean = { File.write(hgrc, cat_lines(lines)) true } val edited = hgrc.is_file && { val lines = split_lines(File.read(hgrc)) lines.count(header) == 1 && { if (local_hg.paths(options = "-q").contains(path_name)) { val old_source = local_hg.paths(args = path_name).head val old_entry = path_name + ".old = " + old_source val lines1 = lines.map { case Entry(a, b) if a == path_name && b == old_source => new_entry + "\n" + old_entry case line => line } lines != lines1 && commit(lines1) } else { val prefix = lines.takeWhile(line => !header(line)) val n = prefix.length commit(prefix ::: List(lines(n), new_entry) ::: lines.drop(n + 1)) } } } if (!edited) File.append(hgrc, "\n[paths]\n" + new_entry + "\n") } val default_path_name = "default" def hg_setup( remote: String, local_path: Path, remote_name: String = "", path_name: String = default_path_name, remote_exists: Boolean = false, progress: Progress = new Progress): Unit = { /* local repository */ Isabelle_System.make_directory(local_path) val repos_name = proper_string(remote_name) getOrElse local_path.absolute.base.implode val local_hg = if (is_repository(local_path)) repository(local_path) else init_repository(local_path) progress.echo("Local repository " + local_hg.root.absolute) /* remote repository */ val remote_url = remote match { case _ if remote.startsWith("ssh://") => val ssh_url = remote + "/" + repos_name if (!remote_exists) { try { local_hg.command("init", ssh_url, repository = false).check } catch { case ERROR(msg) => progress.echo_warning(msg) } } ssh_url case SSH.Target(user, host) => val phabricator = Phabricator.API(user, host) var repos = phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse { if (remote_exists) { error("Remote repository " + quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist") } else phabricator.create_repository(repos_name, short_name = repos_name) } while (repos.importing) { progress.echo("Awaiting remote repository ...") Time.seconds(0.5).sleep repos = phabricator.the_repository(repos.phid) } repos.ssh_url case _ => error("Malformed remote specification " + quote(remote)) } progress.echo("Remote repository " + quote(remote_url)) /* synchronize local and remote state */ progress.echo("Synchronizing ...") edit_hgrc(local_hg, path_name, remote_url) local_hg.pull(options = "-u") local_hg.push(remote = remote_url) } val isabelle_tool = Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository", Scala_Project.here, args => { var remote_name = "" var path_name = default_path_name var remote_exists = false val getopts = Getopts(""" Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR Options are: -n NAME remote repository name (default: base name of LOCAL_DIR) -p PATH Mercurial path name (default: """ + quote(default_path_name) + """) -r assume that remote repository already exists Setup a remote vs. local Mercurial repository: REMOTE either refers to a Phabricator server "user@host" or SSH file server "ssh://user@host/path". """, "n:" -> (arg => remote_name = arg), "p:" -> (arg => path_name = arg), "r" -> (_ => remote_exists = true)) val more_args = getopts(args) val (remote, local_path) = more_args match { case List(arg1, arg2) => (arg1, Path.explode(arg2)) case _ => getopts.usage() } val progress = new Console_Progress hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name, remote_exists = remote_exists, progress = progress) }) } diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,633 +1,633 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Fundamental Isabelle system environment: quasi-static module with optional init operation. */ package isabelle import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult, StandardCopyOption, FileSystemException} import java.nio.file.attribute.BasicFileAttributes import scala.jdk.CollectionConverters._ object Isabelle_System { /** bootstrap information **/ def jdk_home(): String = { val java_home = System.getProperty("java.home", "") val home = new JFile(java_home) val parent = home.getParent if (home.getName == "jre" && parent != null && (new JFile(new JFile(parent, "bin"), "javac")).exists) parent else java_home } def bootstrap_directory( preference: String, envar: String, property: String, description: String): String = { val value = proper_string(preference) orElse // explicit argument proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process error("Unknown " + description + " directory") if ((new JFile(value)).isDirectory) value else error("Bad " + description + " directory " + quote(value)) } /** implicit settings environment **/ abstract class Service @volatile private var _settings: Option[Map[String, String]] = None @volatile private var _services: Option[List[Class[Service]]] = None def settings(): Map[String, String] = { if (_settings.isEmpty) init() // unsynchronized check _settings.get } def services(): List[Class[Service]] = { if (_services.isEmpty) init() // unsynchronized check _services.get } def make_services[C](c: Class[C]): List[C] = for { c1 <- services() if Library.is_subclass(c1, c) } yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C] def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized { if (_settings.isEmpty || _services.isEmpty) { val isabelle_root1 = bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root") val cygwin_root1 = if (Platform.is_windows) bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") else "" if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1) def set_cygwin_root(): Unit = { if (Platform.is_windows) _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1)) } set_cygwin_root() def default(env: Map[String, String], entry: (String, String)): Map[String, String] = if (env.isDefinedAt(entry._1) || entry._2 == "") env else env + entry val env = { val temp_windows = { val temp = if (Platform.is_windows) System.getenv("TEMP") else null if (temp != null && temp.contains('\\')) temp else "" } val user_home = System.getProperty("user.home", "") val isabelle_app = System.getProperty("isabelle.app", "") default( default( default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), "TEMP_WINDOWS" -> temp_windows), "HOME" -> user_home), "ISABELLE_APP" -> "true") } val settings = { val dump = JFile.createTempFile("settings", null) dump.deleteOnExit try { val cmd1 = if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l", File.standard_path(isabelle_root1 + "\\bin\\isabelle")) else List(isabelle_root1 + "/bin/isabelle") val cmd = cmd1 ::: List("getenv", "-d", dump.toString) val (output, rc) = process_output(process(cmd, env = env, redirect = true)) if (rc != 0) error(output) val entries = (for (entry <- space_explode('\u0000', File.read(dump)) if entry != "") yield { val i = entry.indexOf('=') if (i <= 0) entry -> "" else entry.substring(0, i) -> entry.substring(i + 1) }).toMap entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" } finally { dump.delete } } _settings = Some(settings) set_cygwin_root() val variable = "ISABELLE_SCALA_SERVICES" val services = for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable)))) yield { def err(msg: String): Nothing = error("Bad entry " + quote(name) + " in " + variable + "\n" + msg) try { Class.forName(name).asInstanceOf[Class[Service]] } catch { case _: ClassNotFoundException => err("Class not found") case exn: Throwable => err(Exn.message(exn)) } } _services = Some(services) } } /* getenv -- dynamic process environment */ private def getenv_error(name: String): Nothing = error("Undefined Isabelle environment variable: " + quote(name)) def getenv(name: String, env: Map[String, String] = settings()): String = env.getOrElse(name, "") def getenv_strict(name: String, env: Map[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) def cygwin_root(): String = getenv_strict("CYGWIN_ROOT") /* getetc -- static distribution parameters */ def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] = { val path = root + Path.basic("etc") + Path.basic(name) if (path.is_file) { Library.trim_split_lines(File.read(path)) match { case Nil => None case List(s) => Some(s) case _ => error("Single line expected in " + path.absolute) } } else None } /* Isabelle distribution identification */ def isabelle_id(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse { if (Mercurial.is_repository(root)) Mercurial.repository(root).parent() else error("Failed to identify Isabelle distribution " + root) } object Isabelle_Id extends Scala.Fun_String("isabelle_id") { val here = Scala_Project.here def apply(arg: String): String = isabelle_id() } def isabelle_tags(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse { if (Mercurial.is_repository(root)) { val hg = Mercurial.repository(root) hg.tags(rev = hg.parent()) } else "" } def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER")) def isabelle_heading(): String = isabelle_identifier() match { case None => "" case Some(version) => " (" + version + ")" } def isabelle_name(): String = getenv_strict("ISABELLE_NAME") def identification(): String = "Isabelle/" + isabelle_id() + isabelle_heading() /** file-system operations **/ /* scala functions */ private def apply_paths(args: List[String], fun: List[Path] => Unit): List[String] = { fun(args.map(Path.explode)); Nil } private def apply_paths1(args: List[String], fun: Path => Unit): List[String] = apply_paths(args, { case List(path) => fun(path) }) private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] = apply_paths(args, { case List(path1, path2) => fun(path1, path2) }) private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] = apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) }) /* permissions */ def chmod(arg: String, path: Path): Unit = bash("chmod " + arg + " " + File.bash_path(path)).check def chown(arg: String, path: Path): Unit = bash("chown " + arg + " " + File.bash_path(path)).check /* directories */ def make_directory(path: Path): Path = { if (!path.is_dir) { try { Files.createDirectories(path.file.toPath) } catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) } } path } def new_directory(path: Path): Path = if (path.is_dir) error("Directory already exists: " + path.absolute) else make_directory(path) def copy_dir(dir1: Path, dir2: Path): Unit = { val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)) if (!res.ok) { cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err) } } object Make_Directory extends Scala.Fun_Strings("make_directory") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, make_directory) } object Copy_Dir extends Scala.Fun_Strings("copy_dir") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir) } /* copy files */ def copy_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) { try { Files.copy(src.toPath, target.toPath, StandardCopyOption.COPY_ATTRIBUTES, StandardCopyOption.REPLACE_EXISTING) } catch { case ERROR(msg) => cat_error("Failed top copy file " + File.path(src).absolute + " to " + File.path(dst).absolute, msg) } } } def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file) def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = { val src1 = src.expand val src1_dir = src1.dir if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory") copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir)) } object Copy_File extends Scala.Fun_Strings("copy_file") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_file) } object Copy_File_Base extends Scala.Fun_Strings("copy_file_base") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base) } /* move files */ def move_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) } def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file) /* symbolic link */ def symlink(src: Path, dst: Path, force: Boolean = false): Unit = { val src_file = src.file val dst_file = dst.file val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file if (force) target.delete try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => Cygwin.link(File.standard_path(src), target) case _: FileSystemException if Platform.is_windows => Cygwin.link(File.standard_path(src), target) } } /* tmp files */ def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment File.platform_file(path) } def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile file.deleteOnExit file } def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { val file = tmp_file(name, ext) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: JFile): Unit = { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def rm_tree(root: Path): Unit = rm_tree(root.file) object Rm_Tree extends Scala.Fun_Strings("rm_tree") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree) } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit dir } def with_tmp_dir[A](name: String)(body: Path => A): A = { val dir = tmp_dir(name) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit): Unit = { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) move_file(dir, old_dir) move_file(new_dir, dir) rm_tree(old_dir) } /** external processes **/ /* raw process */ def process(command_line: List[String], cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false): Process = { val proc = new ProcessBuilder // fragile on Windows: // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160 proc.command(command_line.asJava) if (cwd != null) proc.directory(cwd) if (env != null) { proc.environment.clear() for ((x, y) <- env) proc.environment.put(x, y) } proc.redirectErrorStream(redirect) proc.start } def process_output(proc: Process): (String, Int) = { proc.getOutputStream.close() val output = File.read_stream(proc.getInputStream) val rc = try { proc.waitFor } finally { proc.getInputStream.close() proc.getErrorStream.close() proc.destroy() Exn.Interrupt.dispose() } (output, rc) } def process_signal(group_pid: String, signal: String = "0"): Boolean = { val bash = if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe") else List("/usr/bin/env", "bash") val (_, rc) = process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid))) rc == 0 } /* GNU bash */ def bash(script: String, cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Bash.Watchdog] = None, strict: Boolean = true, cleanup: () => Unit = () => ()): Process_Result = { Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(progress_stdout = progress_stdout, progress_stderr = progress_stderr, watchdog = watchdog, strict = strict) } private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } def gnutar( args: String, dir: Path = Path.current, original_owner: Boolean = false, redirect: Boolean = false): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } def require_command(cmds: String*): Unit = { for (cmd <- cmds) { if (!bash(Bash.string(cmd) + " --version").ok) error("Missing system command: " + quote(cmd)) } } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def open_external_file(name: String): Boolean = { val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString val external = ext.nonEmpty && Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext) if (external) { if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name)) else open(name) } external } def export_isabelle_identifier(isabelle_identifier: String): String = if (isabelle_identifier == "") "" else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* components */ def components(): List[Path] = Path.split(getenv_strict("ISABELLE_COMPONENTS")) /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => getenv_strict("ISABELLE_LOGIC") } } /* download file */ def download(url_name: String, progress: Progress = new Progress): HTTP.Content = { val url = Url(url_name) progress.echo("Getting " + quote(url_name)) try { HTTP.Client.get(url) } catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) } } def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit = Bytes.write(file, download(url_name, progress = progress).bytes) object Download extends Scala.Fun("download", thread = true) { val here = Scala_Project.here override def invoke(args: List[Bytes]): List[Bytes] = args match { case List(url) => List(download(url.text).bytes) } } /* repositories */ - val isabelle_repository: Mercurial.Address = - Mercurial.Address("https://isabelle.sketis.net/repos/isabelle") + val isabelle_repository: Mercurial.Server = + Mercurial.Server("https://isabelle.sketis.net/repos/isabelle") - val afp_repository: Mercurial.Address = - Mercurial.Address("https://isabelle.sketis.net/repos/afp-devel") + val afp_repository: Mercurial.Server = + Mercurial.Server("https://isabelle.sketis.net/repos/afp-devel") def official_releases(): List[String] = Library.trim_split_lines( isabelle_repository.read_file(Path.explode("Admin/Release/official"))) }