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,438 +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 */ 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) + " --strip-components=1", - dir = dir, original_owner = true).check + Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path), + dir = dir, original_owner = true, strip = 1).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(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 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,635 @@ /* 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, + strip: Int = 0, 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 (original_owner) "" else "--owner=root --group=staff ") + + (if (strip <= 0) "" else "--strip-components=" + strip + " ") 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.Server = Mercurial.Server("https://isabelle.sketis.net/repos/isabelle") 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"))) }