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,592 +1,593 @@ /* 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 cygwin_32 = "x86-cygwin" 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(cygwin_32)) cygwin_32 else if (check_dir(windows_32)) windows_32 else err(windows_32) } 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 } /** local build --- from sync_repos directory **/ private val default_user_home = Path.USER_HOME private val default_multicore = (1, 1) private val default_heap = 1500 private val default_isabelle_identifier = "build_history" def local_build( options: Options, root: Path, user_home: Path = default_user_home, progress: Progress = new Progress, afp: Boolean = false, 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 Admin/build_other within existing Isabelle settings environment") } /* Isabelle + AFP directory (produced via sync_repos) */ def directory(dir: Path): Mercurial.Hg_Sync.Directory = { val directory = Mercurial.Hg_Sync.directory(dir) if (verbose) progress.echo(directory.log) directory } val isabelle_directory = directory(root) val afp_directory = if (afp) Some(directory(root + Path.explode("AFP"))) else None val (afp_build_args, afp_sessions) = if (afp_directory.isEmpty) (Nil, Nil) else { val (opt, sessions) = { if (afp_partition == 0) ("-d", Nil) else { try { val afp_info = AFP.init(options, base_dir = afp_directory.get.root) ("-d", afp_info.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_directory.id) ::: afp_directory.map(dir => Build_Log.Prop.afp_version.name -> dir.id).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 = false 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 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_other [OPTIONS] ISABELLE_HOME [ARGS ...] Options are: -A include $ISABELLE_HOME/AFP directory -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) -n no build: sync only -o FILE output file for log names (default: stdout) -p TEXT additional text for generated etc/preferences -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" -> (_ => afp = true), "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)), "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 = local_build(Options.init(), root, user_home = user_home, progress = progress, afp = afp, 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(Process_Result.RC.ok) { case (rc, (res, _)) => rc max res.rc } if (rc != Process_Result.RC.ok && exit_code) sys.exit(rc) } } /** remote build -- via rsync and ssh **/ def remote_build( ssh: SSH.Session, isabelle_self: Path, isabelle_other: Path, isabelle_identifier: String = "remote_build_history", progress: Progress = new Progress, rev: String = "", afp_repos: Option[Path] = None, afp_rev: String = "", options: String = "", args: String = "", no_build: Boolean = false ): List[(String, Bytes)] = { /* synchronize Isabelle + AFP repositories */ def sync_repos(target: Path, accurate: Boolean = false, rev: String = "", afp_rev: String = "", afp: Boolean = false ): Unit = { - Sync_Repos.sync_repos(ssh.rsync_path(target), port = ssh.port, progress = progress, + val context = Rsync.Context(progress, port = ssh.port) + Sync_Repos.sync_repos(context, ssh.rsync_path(target), thorough = accurate, preserve_jars = !accurate, rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None) } def execute(command: String, args: String, echo: Boolean = false, strict: Boolean = true ): Unit = ssh.execute( Isabelle_System.export_isabelle_identifier(isabelle_identifier) + ssh.bash_path(isabelle_self + Path.explode(command)) + " " + args, progress_stdout = progress.echo_if(echo, _), progress_stderr = progress.echo_if(echo, _), strict = strict).check sync_repos(isabelle_self) execute("bin/isabelle", "components -I") execute("bin/isabelle", "components -a", echo = true) execute("bin/isabelle", "jedit -bf") sync_repos(isabelle_other, accurate = true, rev = proper_string(rev) getOrElse "tip", afp_rev = proper_string(afp_rev) getOrElse "tip", afp = true) /* build */ if (no_build) Nil else { ssh.with_tmp_dir { tmp_dir => val output_file = tmp_dir + Path.explode("output") val build_options = (if (afp_repos.isEmpty) "" else " -A") + " " + options try { execute("Admin/build_other", "-o " + ssh.bash_path(output_file) + build_options + " " + ssh.bash_path(isabelle_other) + " " + args, echo = true, strict = false) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for Admin/build_other " + build_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/sync_repos.scala b/src/Pure/Admin/sync_repos.scala --- a/src/Pure/Admin/sync_repos.scala +++ b/src/Pure/Admin/sync_repos.scala @@ -1,102 +1,101 @@ /* Title: Pure/Admin/sync_repos.scala Author: Makarius Synchronize Isabelle + AFP repositories. */ package isabelle object Sync_Repos { - def sync_repos(target: String, - progress: Progress = new Progress, - port: Int = SSH.default_port, + def sync_repos(context: Rsync.Context, target: String, verbose: Boolean = false, thorough: Boolean = false, preserve_jars: Boolean = false, dry_run: Boolean = false, rev: String = "", afp_root: Option[Path] = None, afp_rev: String = "" ): Unit = { val hg = Mercurial.self_repository() val afp_hg = afp_root.map(Mercurial.repository(_)) val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil def sync(hg: Mercurial.Repository, dest: String, r: String, contents: List[File.Content] = Nil, filter: List[String] = Nil ): Unit = { - hg.sync(dest, rev = r, progress = progress, port = port, verbose = verbose, - thorough = thorough, dry_run = dry_run, contents = contents, filter = filter ::: more_filter) + hg.sync(context, dest, rev = r, verbose = verbose, thorough = thorough, dry_run = dry_run, + contents = contents, filter = filter ::: more_filter) } - progress.echo_if(verbose, "\n* Isabelle repository:") + context.progress.echo_if(verbose, "\n* Isabelle repository:") sync(hg, target, rev, contents = List(File.Content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))), filter = List("protect /AFP")) for (hg <- afp_hg) { - progress.echo_if(verbose, "\n* AFP repository:") + context.progress.echo_if(verbose, "\n* AFP repository:") sync(hg, Rsync.append(target, "AFP"), afp_rev) } } val isabelle_tool = Isabelle_Tool("sync_repos", "synchronize Isabelle + AFP repositories", Scala_Project.here, { args => var afp_root: Option[Path] = None var preserve_jars = false var thorough = false var afp_rev = "" var dry_run = false var rev = "" var port = SSH.default_port var verbose = false val getopts = Getopts(""" Usage: isabelle sync_repos [OPTIONS] TARGET Options are: -A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """) -J preserve *.jar files -T thorough treatment of file content and directory times -a REV explicit AFP revision (default: state of working directory) -n no changes: dry-run -r REV explicit revision (default: state of working directory) -p PORT explicit SSH port (default: """ + SSH.default_port + """) -v verbose Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync". Example: quick testing isabelle sync_repos -A: -J testmachine:test/isabelle_afp Example: accurate testing isabelle sync_repos -A: -T testmachine:test/isabelle_afp """, "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))), "J" -> (_ => preserve_jars = true), "T" -> (_ => thorough = true), "a:" -> (arg => afp_rev = arg), "n" -> (_ => dry_run = true), "r:" -> (arg => rev = arg), "p:" -> (arg => port = Value.Int.parse(arg)), "v" -> (_ => verbose = true)) val more_args = getopts(args) val target = more_args match { case List(target) => target case _ => getopts.usage() } val progress = new Console_Progress - sync_repos(target, progress = progress, port = port, verbose = verbose, thorough = thorough, + val context = Rsync.Context(progress, port = port) + sync_repos(context, target, verbose = verbose, thorough = thorough, preserve_jars = preserve_jars, dry_run = dry_run, rev = rev, afp_root = afp_root, afp_rev = afp_rev) } ) } 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,613 +1,613 @@ /* 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 **/ object Server { 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() } } } 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), dir = dir, original_owner = true, strip = 1).check } } } /** repository commands **/ /* 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(" ")) /* hg_sync meta data */ object Hg_Sync { val NAME = ".hg_sync" val _NAME: String = " " + NAME val PATH: Path = Path.explode(NAME) val PATH_ID: Path = PATH + Path.explode("id") val PATH_LOG: Path = PATH + Path.explode("log") val PATH_DIFF: Path = PATH + Path.explode("diff") val PATH_STAT: Path = PATH + Path.explode("stat") def is_directory(root: Path, ssh: SSH.System = SSH.Local): Boolean = ssh.is_dir(root + PATH) def directory(root: Path, ssh: SSH.System = SSH.Local): Directory = { if (is_directory(root, ssh = ssh)) new Directory(root, ssh) else error("No .hg_sync directory found in " + ssh.rsync_path(root)) } class Directory private [Hg_Sync](val root: Path, val ssh: SSH.System) { override def toString: String = ssh.rsync_path(root) def read(path: Path): String = ssh.read(root + path) lazy val id: String = read(PATH_ID) lazy val log: String = read(PATH_LOG) lazy val diff: String = read(PATH_DIFF) lazy val stat: String = read(PATH_STAT) def changed: Boolean = id.endsWith("+") } } /* 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 id_repository(root: Path, ssh: SSH.System = SSH.Local, rev: String = "tip"): Option[String] = if (is_repository(root, ssh = ssh)) Some(repository(root, ssh = ssh).id(rev = rev)) else None def repository(root: Path, ssh: SSH.System = SSH.Local): Repository = { val hg = new Repository(root, ssh) hg.command("root").check hg } def self_repository(): Repository = repository(Path.ISABELLE_HOME) 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)) } def the_repository(start: Path, ssh: SSH.System = SSH.Local): Repository = find_repository(start, ssh = ssh) getOrElse error("No repository found in " + start.absolute) 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(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository = { 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_line( name: String, args: String = "", options: String = "", repository: Boolean = true ): String = { "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 diff(rev: String = "", options: String = ""): String = hg.command("diff", opt_rev(rev), 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 status(options: String = ""): List[String] = hg.command("status", options = options).check.out_lines def known_files(): List[String] = status(options = "--modified --added --clean --no-status") - def sync(target: String, - progress: Progress = new Progress, - port: Int = SSH.default_port, + def sync(context: Rsync.Context, target: String, verbose: Boolean = false, thorough: Boolean = false, dry_run: Boolean = false, filter: List[String] = Nil, contents: List[File.Content] = Nil, rev: String = "" ): Unit = { require(ssh == SSH.Local, "local repository required") Isabelle_System.with_tmp_dir("sync") { tmp_dir => - Rsync.rsync_init(target, port = port) + Rsync.rsync_init(context, target) val list = - Rsync.rsync(port = port, list = true, + Rsync.rsync(context, list = true, args = List("--", Rsync.terminate(target)) ).check.out_lines.filterNot(_.endsWith(" .")) if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) { error("No .hg_sync meta data in " + quote(target)) } val id_content = id(rev = rev) val is_changed = id_content.endsWith("+") val log_content = if (is_changed) "" else log(rev = rev, options = "-l1") val diff_content = if (is_changed) diff(rev = rev, options = "--git") else "" val stat_content = if (is_changed) diff(rev = rev, options = "--stat") else "" - Rsync.rsync_init(target, port = port, + Rsync.rsync_init(context, target, contents = File.Content(Hg_Sync.PATH_ID, id_content) :: File.Content(Hg_Sync.PATH_LOG, log_content) :: File.Content(Hg_Sync.PATH_DIFF, diff_content) :: File.Content(Hg_Sync.PATH_STAT, stat_content) :: contents) val (exclude, source) = if (rev.isEmpty) { val exclude = ".hg" :: status(options = "--unknown --ignored --no-status") val source = File.standard_path(root) (exclude, source) } else { val exclude = List(".hg_archival.txt") val source = File.standard_path(tmp_dir + Path.explode("archive")) archive(source, rev = rev) (exclude, source) } val exclude_path = tmp_dir + Path.explode("exclude") File.write(exclude_path, cat_lines(exclude.map("/" + _))) val protect = (Hg_Sync.PATH :: contents.map(_.path)) .map(path => "protect /" + File.standard_path(path)) - Rsync.rsync( - progress = progress, port = port, verbose = verbose, thorough = thorough, + Rsync.rsync(context, + verbose = verbose, + thorough = thorough, dry_run = dry_run, clean = true, prune_empty_dirs = true, filter = protect ::: filter, args = List("--exclude-from=" + exclude_path.implode, "--", Rsync.terminate(source), target) ).check } } 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) } /** hg_setup **/ 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_tool1 = 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) }) /** hg_sync **/ val isabelle_tool2 = Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory", Scala_Project.here, { args => var filter: List[String] = Nil var root: Option[Path] = None var thorough = false var dry_run = false var rev = "" var port = SSH.default_port var verbose = false val getopts = Getopts(""" Usage: isabelle hg_sync [OPTIONS] TARGET Options are: -F RULE add rsync filter RULE (e.g. "protect /foo" to avoid deletion) -R ROOT explicit repository root directory (default: implicit from current directory) -T thorough treatment of file content and directory times -n no changes: dry-run -r REV explicit revision (default: state of working directory) -p PORT explicit SSH port (default: """ + SSH.default_port + """) -v verbose Synchronize Mercurial repository with TARGET directory, which can be local or remote (using notation of rsync). """, "F:" -> (arg => filter = filter ::: List(arg)), "R:" -> (arg => root = Some(Path.explode(arg))), "T" -> (_ => thorough = true), "n" -> (_ => dry_run = true), "r:" -> (arg => rev = arg), "p:" -> (arg => port = Value.Int.parse(arg)), "v" -> (_ => verbose = true)) val more_args = getopts(args) val target = more_args match { case List(target) => target case _ => getopts.usage() } val progress = new Console_Progress val hg = root match { case Some(dir) => repository(dir) case None => the_repository(Path.current) } - hg.sync(target, progress = progress, port = port, verbose = verbose, thorough = thorough, + val context = Rsync.Context(progress, port = port) + hg.sync(context, target, verbose = verbose, thorough = thorough, dry_run = dry_run, filter = filter, rev = rev) } ) } diff --git a/src/Pure/General/rsync.scala b/src/Pure/General/rsync.scala --- a/src/Pure/General/rsync.scala +++ b/src/Pure/General/rsync.scala @@ -1,55 +1,58 @@ /* Title: Pure/General/rsync.scala Author: Makarius Support for rsync: see also https://rsync.samba.org */ package isabelle object Rsync { + sealed case class Context(progress: Progress, port: Int = SSH.default_port) { + def command: String = + "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) + } + def rsync( - progress: Progress = new Progress, - port: Int = SSH.default_port, + context: Context, verbose: Boolean = false, thorough: Boolean = false, prune_empty_dirs: Boolean = false, dry_run: Boolean = false, clean: Boolean = false, list: Boolean = false, filter: List[String] = Nil, args: List[String] = Nil ): Process_Result = { val script = - "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) + + context.command + (if (verbose) " --verbose" else "") + (if (thorough) " --ignore-times" else " --omit-dir-times") + (if (prune_empty_dirs) " --prune-empty-dirs" else "") + (if (dry_run) " --dry-run" else "") + (if (clean) " --delete-excluded" else "") + (if (list) " --list-only --no-human-readable" else "") + filter.map(s => " --filter=" + Bash.string(s)).mkString + (if (args.nonEmpty) " " + Bash.strings(args) else "") - progress.bash(script, echo = true) + context.progress.bash(script, echo = true) } - def rsync_init(target: String, - port: Int = SSH.default_port, + def rsync_init(context: Context, target: String, contents: List[File.Content] = Nil ): Unit = Isabelle_System.with_tmp_dir("sync") { tmp_dir => val init_dir = Isabelle_System.make_directory(tmp_dir + Path.explode("init")) contents.foreach(_.write(init_dir)) - rsync(port = port, thorough = true, + rsync(context, thorough = true, args = List(File.bash_path(init_dir) + "/.", target)).check } def terminate(target: String): String = if (target.endsWith(":") || target.endsWith("/")) target + "." else if (target.endsWith(":.") || target.endsWith("/.")) target else target + "/." def append(target: String, rest: String): String = if (target.endsWith(":") || target.endsWith("/")) target + rest else target + "/" + rest }