diff --git a/src/Pure/General/file.scala b/src/Pure/General/file.scala --- a/src/Pure/General/file.scala +++ b/src/Pure/General/file.scala @@ -1,338 +1,295 @@ /* Title: Pure/General/file.scala Author: Makarius File-system operations. */ package isabelle import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader, File => JFile, IOException} import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor, FileVisitOption, FileVisitResult} import java.nio.file.attribute.BasicFileAttributes import java.net.{URL, MalformedURLException} import java.util.zip.{GZIPInputStream, GZIPOutputStream} -import java.util.regex.Pattern import java.util.EnumSet import org.tukaani.xz.{XZInputStream, XZOutputStream} import scala.collection.mutable -import scala.util.matching.Regex object File { /* standard path (Cygwin or Posix) */ def standard_path(path: Path): String = path.expand.implode def standard_path(platform_path: String): String = - if (Platform.is_windows) { - val Platform_Root = new Regex("(?i)" + - Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""") - val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") - - platform_path.replace('/', '\\') match { - case Platform_Root(rest) => "/" + rest.replace('\\', '/') - case Drive(letter, rest) => - "/cygdrive/" + Word.lowercase(letter) + - (if (rest == "") "" else "/" + rest.replace('\\', '/')) - case path => path.replace('\\', '/') - } - } - else platform_path + Isabelle_Env.standard_path(Isabelle_System.cygwin_root(), platform_path) def standard_path(file: JFile): String = standard_path(file.getPath) def standard_url(name: String): String = try { val url = new URL(name) if (url.getProtocol == "file" && Url.is_wellformed_file(name)) standard_path(Url.parse_file(name)) else name } catch { case _: MalformedURLException => standard_path(name) } /* platform path (Windows or Posix) */ - private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)") - private val Named_Root = new Regex("//+([^/]*)(.*)") - def platform_path(standard_path: String): String = - if (Platform.is_windows) { - val result_path = new StringBuilder - val rest = - standard_path match { - case Cygdrive(drive, rest) => - result_path ++= (Word.uppercase(drive) + ":" + JFile.separator) - rest - case Named_Root(root, rest) => - result_path ++= JFile.separator - result_path ++= JFile.separator - result_path ++= root - rest - case path if path.startsWith("/") => - result_path ++= Isabelle_System.cygwin_root() - path - case path => path - } - for (p <- space_explode('/', rest) if p != "") { - val len = result_path.length - if (len > 0 && result_path(len - 1) != JFile.separatorChar) - result_path += JFile.separatorChar - result_path ++= p - } - result_path.toString - } - else standard_path + Isabelle_Env.platform_path(Isabelle_System.cygwin_root(), standard_path) def platform_path(path: Path): String = platform_path(standard_path(path)) def platform_file(path: Path): JFile = new JFile(platform_path(path)) /* platform files */ def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile def absolute_name(file: JFile): String = absolute(file).getPath def canonical(file: JFile): JFile = file.getCanonicalFile def canonical_name(file: JFile): String = canonical(file).getPath def path(file: JFile): Path = Path.explode(standard_path(file)) def pwd(): Path = path(Path.current.absolute_file) /* relative paths */ def relative_path(base: Path, other: Path): Option[Path] = { val base_path = base.file.toPath val other_path = other.file.toPath if (other_path.startsWith(base_path)) Some(path(base_path.relativize(other_path).toFile)) else None } /* bash path */ def bash_path(path: Path): String = Bash.string(standard_path(path)) def bash_path(file: JFile): String = Bash.string(standard_path(file)) def bash_platform_path(path: Path): String = Bash.string(platform_path(path)) /* directory entries */ def check_dir(path: Path): Path = if (path.is_dir) path else error("No such directory: " + path) def check_file(path: Path): Path = if (path.is_file) path else error("No such file: " + path) /* directory content */ def read_dir(dir: Path): List[String] = { if (!dir.is_dir) error("No such directory: " + dir.toString) val files = dir.file.listFiles if (files == null) Nil else files.toList.map(_.getName).sorted } def get_dir(dir: Path): String = read_dir(dir).filter(name => (dir + Path.basic(name)).is_dir) match { case List(entry) => entry case dirs => error("Exactly one directory entry expected: " + commas_quote(dirs.sorted)) } def find_files( start: JFile, pred: JFile => Boolean = _ => true, include_dirs: Boolean = false, follow_links: Boolean = false): List[JFile] = { val result = new mutable.ListBuffer[JFile] def check(file: JFile): Unit = if (pred(file)) result += file if (start.isFile) check(start) else if (start.isDirectory) { val options = if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS) else EnumSet.noneOf(classOf[FileVisitOption]) Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE, new SimpleFileVisitor[JPath] { override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult = { if (include_dirs) check(path.toFile) FileVisitResult.CONTINUE } override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult = { val file = path.toFile if (include_dirs || !file.isDirectory) check(file) FileVisitResult.CONTINUE } } ) } result.toList } /* read */ def read(file: JFile): String = Bytes.read(file).text def read(path: Path): String = read(path.file) def read_stream(reader: BufferedReader): String = { val output = new StringBuilder(100) var c = -1 while ({ c = reader.read; c != -1 }) output += c.toChar reader.close() output.toString } def read_stream(stream: InputStream): String = read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset))) def read_gzip(file: JFile): String = read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file)))) def read_gzip(path: Path): String = read_gzip(path.file) def read_xz(file: JFile): String = read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file)))) def read_xz(path: Path): String = read_xz(path.file) /* read lines */ def read_line(reader: BufferedReader): Option[String] = { val line = try { reader.readLine} catch { case _: IOException => null } Option(line).map(Library.trim_line) } def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = { val result = new mutable.ListBuffer[String] var line: Option[String] = None while ({ line = read_line(reader); line.isDefined }) { progress(line.get) result += line.get } reader.close() result.toList } /* write */ def writer(file: JFile): BufferedWriter = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset)) def write_file( file: JFile, text: String, make_stream: OutputStream => OutputStream): Unit = { val stream = make_stream(new FileOutputStream(file)) using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text)) } def write(file: JFile, text: String): Unit = write_file(file, text, s => s) def write(path: Path, text: String): Unit = write(path.file, text) def write_gzip(file: JFile, text: String): Unit = write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s))) def write_gzip(path: Path, text: String): Unit = write_gzip(path.file, text) def write_xz(file: JFile, text: String, options: XZ.Options): Unit = File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options)) def write_xz(file: JFile, text: String): Unit = write_xz(file, text, XZ.options()) def write_xz(path: Path, text: String, options: XZ.Options): Unit = write_xz(path.file, text, options) def write_xz(path: Path, text: String): Unit = write_xz(path, text, XZ.options()) def write_backup(path: Path, text: String): Unit = { if (path.is_file) Isabelle_System.move_file(path, path.backup) write(path, text) } def write_backup2(path: Path, text: String): Unit = { if (path.is_file) Isabelle_System.move_file(path, path.backup2) write(path, text) } /* change */ def change(file: JFile, f: String => String): Unit = { val x = read(file) val y = f(x) if (x != y) write(file, y) } def change_lines(file: JFile, f: List[String] => List[String]): Unit = change(file, text => cat_lines(f(split_lines(text)))) def change(path: Path, f: String => String): Unit = change(path.file, f) def change_lines(path: Path, f: List[String] => List[String]): Unit = change_lines(path.file, f) /* append */ def append(file: JFile, text: String): Unit = Files.write(file.toPath, UTF8.bytes(text), StandardOpenOption.APPEND, StandardOpenOption.CREATE) def append(path: Path, text: String): Unit = append(path.file, text) /* eq */ def eq(file1: JFile, file2: JFile): Boolean = try { Files.isSameFile(file1.toPath, file2.toPath) } catch { case ERROR(_) => false } def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file) /* eq_content */ def eq_content(file1: JFile, file2: JFile): Boolean = if (eq(file1, file2)) true else if (file1.length != file2.length) false else Bytes.read(file1) == Bytes.read(file2) def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file) /* permissions */ def is_executable(path: Path): Boolean = { if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok else path.file.canExecute } def set_executable(path: Path, flag: Boolean): Unit = { if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path) else if (Platform.is_windows) Isabelle_System.chmod("a-x", path) else path.file.setExecutable(flag, false) } } diff --git a/src/Pure/System/isabelle_env.scala b/src/Pure/System/isabelle_env.scala --- a/src/Pure/System/isabelle_env.scala +++ b/src/Pure/System/isabelle_env.scala @@ -1,237 +1,288 @@ /* Title: Pure/System/isabelle_env.scala Author: Makarius Fundamental Isabelle system environment: quasi-static module with optional init operation. */ package isabelle +import java.util.regex.Pattern import java.util.{HashMap, LinkedList, List => JList, Map => JMap} import java.io.{File => JFile} import java.nio.file.Files +import scala.util.matching.Regex + object Isabelle_Env { /** 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)) } /** Support for Cygwin as POSIX emulation on Windows **/ + /* system path representations */ + + def standard_path(cygwin_root: String, platform_path: String): String = + if (Platform.is_windows) { + val Platform_Root = new Regex("(?i)" + Pattern.quote(cygwin_root) + """(?:\\+|\z)(.*)""") + val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") + + platform_path.replace('/', '\\') match { + case Platform_Root(rest) => "/" + rest.replace('\\', '/') + case Drive(letter, rest) => + "/cygdrive/" + Word.lowercase(letter) + + (if (rest == "") "" else "/" + rest.replace('\\', '/')) + case path => path.replace('\\', '/') + } + } + else platform_path + + def platform_path(cygwin_root: String, standard_path: String): String = + if (Platform.is_windows) { + val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)") + val Named_Root = new Regex("//+([^/]*)(.*)") + + val result_path = new StringBuilder + val rest = + standard_path match { + case Cygdrive(drive, rest) => + result_path ++= (Word.uppercase(drive) + ":" + JFile.separator) + rest + case Named_Root(root, rest) => + result_path ++= JFile.separator + result_path ++= JFile.separator + result_path ++= root + rest + case path if path.startsWith("/") => + result_path ++= cygwin_root + path + case path => path + } + for (p <- space_explode('/', rest) if p != "") { + val len = result_path.length + if (len > 0 && result_path(len - 1) != JFile.separatorChar) + result_path += JFile.separatorChar + result_path ++= p + } + result_path.toString + } + else standard_path + + /* symlink emulation */ def cygwin_link(content: String, target: JFile): Unit = { val target_path = target.toPath Files.writeString(target_path, "!" + content + "\u0000") Files.setAttribute(target_path, "dos:system", true) } /* init (e.g. after extraction via 7zip) */ def cygwin_init(isabelle_root: String, cygwin_root: String): Unit = { if (Platform.is_windows) { def cygwin_exec(cmd: JList[String]): Unit = { val cwd = new JFile(isabelle_root) val env = new HashMap(System.getenv()) env.put("CYGWIN", "nodosfilewarning") val res = exec_process(cmd, cwd = cwd, env = env, redirect = true) if (!res.ok) error(res.out) } val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized") val uninitialized = uninitialized_file.isFile && uninitialized_file.delete if (uninitialized) { val symlinks_path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath val symlinks = Files.readAllLines(symlinks_path, UTF8.charset).toArray(new Array[String](0)) // recover symlinks var i = 0 val m = symlinks.length val n = if (m > 0 && symlinks(m - 1).isEmpty) m - 1 else m while (i < n) { if (i + 1 < n) { val target = symlinks(i) val content = symlinks(i + 1) cygwin_link(content, new JFile(isabelle_root, target)) i += 2 } else error("Unbalanced symlinks list") } cygwin_exec(JList.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")) cygwin_exec(JList.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")) } } } /** raw process **/ /* raw process */ def process_builder(cmd: JList[String], cwd: JFile = null, env: JMap[String, String] = settings(), redirect: Boolean = false): ProcessBuilder = { val builder = new ProcessBuilder // fragile on Windows: // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160 builder.command(cmd) if (cwd != null) builder.directory(cwd) if (env != null) { builder.environment.clear() builder.environment().putAll(env) } builder.redirectErrorStream(redirect) } class Exec_Result(val rc: Int, val out: String, val err: String) { def ok: Boolean = rc == 0 } def exec_process(command_line: JList[String], cwd: JFile = null, env: JMap[String, String] = settings(), redirect: Boolean = false): Exec_Result = { val out_file = Files.createTempFile(null, null) val err_file = Files.createTempFile(null, null) try { val proc = { val builder = process_builder(command_line, cwd = cwd, env = env, redirect = redirect) builder.redirectOutput(out_file.toFile) builder.redirectError(err_file.toFile) builder.start() } proc.getOutputStream.close() try { proc.waitFor() } finally { proc.getInputStream.close() proc.getErrorStream.close() proc.destroy() Thread.interrupted() } val rc = proc.exitValue() val out = Files.readString(out_file) val err = Files.readString(err_file) new Exec_Result(rc, out, err) } finally { Files.deleteIfExists(out_file) Files.deleteIfExists(err_file) } } /** implicit settings environment **/ @volatile private var _settings: JMap[String, String] = null def settings(): JMap[String, String] = { if (_settings == null) init("", "") // unsynchronized check _settings } def init(isabelle_root: String, cygwin_root: String): Unit = synchronized { if (_settings == null) { val isabelle_root1 = bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root") val cygwin_root1 = if (Platform.is_windows) { val root = bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") cygwin_init(isabelle_root1, root) - _settings = JMap.of("CYGWIN_ROOT", root) root } else "" val env = new HashMap(System.getenv()) def env_default(a: String, b: String): Unit = if (b != "") env.putIfAbsent(a, b) env_default("CYGWIN_ROOT", cygwin_root1) env_default("TEMP_WINDOWS", { val temp = if (Platform.is_windows) System.getenv("TEMP") else null if (temp != null && temp.contains('\\')) temp else "" }) - env_default("ISABELLE_JDK_HOME", File.standard_path(jdk_home())) + env_default("ISABELLE_JDK_HOME", standard_path(cygwin_root1, jdk_home())) env_default("HOME", System.getProperty("user.home", "")) env_default("ISABELLE_APP", System.getProperty("isabelle.app", "")) val settings = new HashMap[String, String] val settings_file = Files.createTempFile(null, null) try { val cmd = new LinkedList[String] if (Platform.is_windows) { cmd.add(cygwin_root1 + "\\bin\\bash") cmd.add("-l") - cmd.add(File.standard_path(isabelle_root1 + "\\bin\\isabelle")) + cmd.add(standard_path(cygwin_root1, isabelle_root1 + "\\bin\\isabelle")) } else { cmd.add(isabelle_root1 + "/bin/isabelle") } cmd.add("getenv") cmd.add("-d") cmd.add(settings_file.toString) val res = exec_process(cmd, env = env, redirect = true) if (!res.ok) error(res.out) for (s <- space_explode('\u0000', Files.readString(settings_file))) { val i = s.indexOf('=') if (i > 0) settings.put(s.substring(0, i), s.substring(i + 1)) else if (i < 0 && s.nonEmpty) settings.put(s, "") } } finally { Files.delete(settings_file) } if (Platform.is_windows) settings.put("CYGWIN_ROOT", cygwin_root1) settings.put("PATH", settings.get("PATH_JVM")) settings.remove("PATH_JVM") _settings = JMap.copyOf(settings) } } } 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,480 +1,480 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Miscellaneous Isabelle system operations. */ package isabelle import java.util.{Map => JMap} import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult, StandardCopyOption, FileSystemException} import java.nio.file.attribute.BasicFileAttributes object Isabelle_System { /* settings */ def settings(): JMap[String, String] = Isabelle_Env.settings() def getenv(name: String, env: JMap[String, String] = settings()): String = Option(env.get(name)).getOrElse("") def getenv_strict(name: String, env: JMap[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") + def cygwin_root(): String = getenv("CYGWIN_ROOT") /* services */ abstract class Service @volatile private var _services: Option[List[Class[Service]]] = None 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] /* init settings + services */ def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = { Isabelle_Env.init(isabelle_root, cygwin_root) synchronized { if (_services.isEmpty) { val variable = "ISABELLE_SCALA_SERVICES" val services = for (name <- space_explode(':', getenv_strict(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) } } } /* 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 to 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 def cygwin_link(): Unit = Isabelle_Env.cygwin_link(File.standard_path(src), target) try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => cygwin_link() case _: FileSystemException if Platform.is_windows => cygwin_link() } } /* 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 **/ /* GNU bash */ def bash(script: String, cwd: JFile = null, env: JMap[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 (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(cmd: String, test: String = "--version"): Unit = { if (!bash(Bash.string(cmd) + " " + test).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 /* 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"))) }