diff --git a/src/Pure/Admin/build_e.scala b/src/Pure/Admin/build_e.scala
--- a/src/Pure/Admin/build_e.scala
+++ b/src/Pure/Admin/build_e.scala
@@ -1,178 +1,175 @@
/* Title: Pure/Admin/build_e.scala
Author: Makarius
Build Isabelle E prover component from official downloads.
*/
package isabelle
object Build_E
{
/* build E prover */
val default_version = "2.5"
val default_download_url =
"https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD"
val default_runepar_url =
"https://raw.githubusercontent.com/JUrban/MPTP2/66f03e5b6df8/MaLARea/bin/runepar.pl"
def build_e(
version: String = default_version,
download_url: String = default_download_url,
runepar_url: String = default_runepar_url,
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current)
{
Isabelle_System.with_tmp_dir("e")(tmp_dir =>
{
/* component */
val component_name = "e-" + version
val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
progress.echo("Component " + component_dir)
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
.getOrElse(error("No 64bit platform"))
val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name))
/* runepar.pl */
val runepar_path = platform_dir + Path.basic("runepar.pl")
Isabelle_System.download(runepar_url, runepar_path, progress = progress)
- File.write(runepar_path,
- File.read(runepar_path)
- .replace("#!/usr/bin/perl", "#!/usr/bin/env perl")
- .replace("bin/eprover", "$ENV{E_HOME}/eprover")
- .replace("bin/eproof", "$ENV{E_HOME}/eproof"))
+ File.change(runepar_path,
+ _.replace("#!/usr/bin/perl", "#!/usr/bin/env perl")
+ .replace("bin/eprover", "$ENV{E_HOME}/eprover")
+ .replace("bin/eproof", "$ENV{E_HOME}/eproof"))
File.set_executable(runepar_path, true)
/* download source */
val e_url = download_url + "/V_" + version + "/E.tgz"
val e_path = tmp_dir + Path.explode("E.tgz")
Isabelle_System.download(e_url, e_path, progress = progress)
Isabelle_System.bash("tar xzf " + e_path, cwd = tmp_dir.file).check
Isabelle_System.bash("tar xzf " + e_path + " && mv E src", cwd = component_dir.file).check
/* build */
progress.echo("Building E prover ...")
val build_dir = tmp_dir + Path.basic("E")
val build_options =
{
val result = Isabelle_System.bash("./configure --help", cwd = build_dir.file)
if (result.check.out.containsSlice("--enable-ho")) " --enable-ho" else ""
}
val build_script = "./configure" + build_options + " && make"
Isabelle_System.bash(build_script,
cwd = build_dir.file,
progress_stdout = progress.echo_if(verbose, _),
progress_stderr = progress.echo_if(verbose, _)).check
/* install */
File.copy(build_dir + Path.basic("COPYING"), component_dir + Path.basic("LICENSE"))
val install_files = List("epclextract", "eproof_ram", "eprover", "eprover-ho")
for (name <- install_files ::: install_files.map(_ + ".exe")) {
val path = build_dir + Path.basic("PROVER") + Path.basic(name)
if (path.is_file) File.copy(path, platform_dir)
}
Isabelle_System.bash("if [ -f eprover-ho ]; then mv eprover-ho eprover; fi",
cwd = platform_dir.file).check
val eproof_ram = platform_dir + Path.basic("eproof_ram")
if (eproof_ram.is_file) {
- File.write(eproof_ram,
- File.read(eproof_ram)
- .replace("EXECPATH=.", "EXECPATH=`dirname \"$0\"`"))
+ File.change(eproof_ram, _.replace("EXECPATH=.", "EXECPATH=`dirname \"$0\"`"))
}
/* settings */
val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
File.write(etc_dir + Path.basic("settings"),
"""# -*- shell-script -*- :mode=shellscript:
E_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
E_VERSION=""" + quote(version) + """
""")
/* README */
File.write(component_dir + Path.basic("README"),
"This is E prover " + version + " from\n" + e_url + """
The distribution has been built like this:
cd src && """ + build_script + """
Only a few executables from PROVERS/ have been moved to the platform-specific
Isabelle component directory: x86_64-linux etc.
This includes a copy of Josef Urban's "runepar.pl" script, modified to use
the correct path.
Makarius
""" + Date.Format.date(Date.now()) + "\n")
})
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_e", "build Isabelle E prover component from official download",
args =>
{
var download_url = default_download_url
var target_dir = Path.current
var runepar_url = default_runepar_url
var version = default_version
var verbose = false
val getopts = Getopts("""
Usage: isabelle build_e [OPTIONS]
Options are:
-E URL E prover download URL
(default: """ + default_download_url + """)
-D DIR target directory (default ".")
-R URL URL for runepar.pl by Josef Urban
(default: """ + default_runepar_url + """)
-V VERSION E prover version (default: """ + default_version + """)
-v verbose
Build E prover component from the specified download URLs and version.
""",
"E:" -> (arg => download_url = arg),
"D:" -> (arg => target_dir = Path.explode(arg)),
"R:" -> (arg => runepar_url = arg),
"V:" -> (arg => version = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
build_e(version = version, download_url = download_url, runepar_url = runepar_url,
verbose = verbose, progress = progress, target_dir = target_dir)
})
}
diff --git a/src/Pure/Admin/build_polyml.scala b/src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala
+++ b/src/Pure/Admin/build_polyml.scala
@@ -1,318 +1,314 @@
/* Title: Pure/Admin/build_polyml.scala
Author: Makarius
Build Poly/ML from sources.
*/
package isabelle
import scala.util.matching.Regex
object Build_PolyML
{
/** platform-specific build **/
sealed case class Platform_Info(
options: List[String] = Nil,
setup: String = "",
copy_files: List[String] = Nil,
ldd_pattern: Option[(String, Regex)] = None)
private val platform_info = Map(
"linux" ->
Platform_Info(
options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"),
ldd_pattern = Some(("ldd", """\s*libgmp.*=>\s*(\S+).*""".r))),
"darwin" ->
Platform_Info(
options =
List("--build=x86_64-darwin", "CFLAGS=-arch x86_64 -O3 -I../libffi/include",
"CXXFLAGS=-arch x86_64 -O3 -I../libffi/include", "CCASFLAGS=-arch x86_64",
"LDFLAGS=-segprot POLY rwx rwx"),
setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin",
ldd_pattern = Some(("otool -L", """\s*(\S+lib(?:polyml|gmp).*dylib).*""".r))),
"windows" ->
Platform_Info(
options =
List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
setup =
"""PATH=/usr/bin:/bin:/mingw64/bin
export CONFIG_SITE=/mingw64/etc/config.site""",
copy_files =
List("$MSYS/mingw64/bin/libgcc_s_seh-1.dll",
"$MSYS/mingw64/bin/libgmp-10.dll",
"$MSYS/mingw64/bin/libstdc++-6.dll",
"$MSYS/mingw64/bin/libwinpthread-1.dll")))
def build_polyml(
root: Path,
sha1_root: Option[Path] = None,
progress: Progress = new Progress,
arch_64: Boolean = false,
options: List[String] = Nil,
msys_root: Option[Path] = None)
{
if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
error("Bad Poly/ML root directory: " + root)
val platform = Isabelle_Platform.self
val platform_arch =
if (arch_64) platform.arch_64
else if (platform.is_intel) "x86_64_32"
else platform.arch_32
val polyml_platform = platform_arch + "-" + platform.os_name
val sha1_platform = platform.arch_64 + "-" + platform.os_name
val info =
platform_info.getOrElse(platform.os_name,
error("Bad OS platform: " + quote(platform.os_name)))
val settings =
msys_root match {
case None if platform.is_windows =>
error("Windows requires specification of msys root directory")
case None => Isabelle_System.settings()
case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode)
}
if (platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) {
error("""Missing "chrpath" executable on Linux""")
}
/* bash */
def bash(
cwd: Path, script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
{
val script1 =
msys_root match {
case None => script
case Some(msys) =>
File.bash_path(msys + Path.explode("usr/bin/bash")) + " -c " + Bash.string(script)
}
progress.bash(script1, cwd = cwd.file, redirect = redirect, echo = echo)
}
/* configure and make */
val configure_options =
List("--disable-shared", "--enable-intinf-as-int", "--with-gmp") :::
info.options ::: options ::: (if (arch_64) Nil else List("--enable-compact32bit"))
bash(root,
info.setup + "\n" +
"""
[ -f Makefile ] && make distclean
{
./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """
rm -rf target
make compiler && make compiler && make install
} || { echo "Build failed" >&2; exit 2; }
""", redirect = true, echo = true).check
val ldd_files =
{
info.ldd_pattern match {
case Some((ldd, pattern)) =>
val lines = bash(root, ldd + " target/bin/poly").check.out_lines
for { line <- lines; List(lib) <- pattern.unapplySeq(line) } yield lib
case None => Nil
}
}
/* sha1 library */
val sha1_files =
if (sha1_root.isDefined) {
val dir1 = sha1_root.get
bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check
val dir2 = dir1 + Path.explode(sha1_platform)
File.read_dir(dir2).map(entry => dir2.implode + "/" + entry)
}
else Nil
/* target */
val target = Path.explode(polyml_platform)
Isabelle_System.rm_tree(target)
Isabelle_System.make_directory(target)
for (file <- info.copy_files ::: ldd_files ::: sha1_files)
File.copy(Path.explode(file).expand_env(settings), target)
for {
d <- List("target/bin", "target/lib")
dir = root + Path.explode(d)
entry <- File.read_dir(dir)
} File.move(dir + Path.explode(entry), target)
/* poly: library path */
if (platform.is_linux) {
bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check
}
else if (platform.is_macos) {
for (file <- ldd_files) {
bash(target,
"""install_name_tool -change """ + Bash.string(file) + " " +
Bash.string("@executable_path/" + Path.explode(file).file_name) + " poly").check
}
}
/* polyc: directory prefix */
- {
- val polyc_path = target + Path.explode("polyc")
-
- val Header = "#! */bin/sh".r
- val polyc_patched =
- split_lines(File.read(polyc_path)) match {
- case Header() :: lines =>
- val lines1 =
- lines.map(line =>
- if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\""
- else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\""
- else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\""
- else line)
- cat_lines("#!/usr/bin/env bash" ::lines1)
- case lines =>
- error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3)))
- }
- File.write(polyc_path, polyc_patched)
- }
+ val Header = "#! */bin/sh".r
+ File.change(target + Path.explode("polyc"), txt =>
+ split_lines(txt) match {
+ case Header() :: lines =>
+ val lines1 =
+ lines.map(line =>
+ if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\""
+ else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\""
+ else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\""
+ else line)
+ cat_lines("#!/usr/bin/env bash" ::lines1)
+ case lines =>
+ error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3)))
+ }
+ )
}
/** skeleton for component **/
private def extract_sources(source_archive: Path, component_dir: Path) =
{
if (source_archive.get_ext == "zip") {
Isabelle_System.bash(
"unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check
}
else {
Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check
}
val src_dir = component_dir + Path.explode("src")
File.read_dir(component_dir) match {
case List(s) => File.move(component_dir + Path.basic(s), src_dir)
case _ => error("Source archive contains multiple directories")
}
val lines = split_lines(File.read(src_dir + Path.explode("RootX86.ML")))
val ml_files =
for {
line <- lines
rest <- Library.try_unprefix("use", line)
} yield "ML_file" + rest
File.write(src_dir + Path.explode("ROOT.ML"),
"""(* Poly/ML Compiler root file.
When this file is open in the Prover IDE, the ML files of the Poly/ML
compiler can be explored interactively. This is a separate copy: it does
not affect the running ML session. *)
""" + ml_files.mkString("\n", "\n", "\n"))
}
def build_polyml_component(
source_archive: Path,
component_dir: Path,
sha1_root: Option[Path] = None)
{
Isabelle_System.new_directory(component_dir)
extract_sources(source_archive, component_dir)
File.copy(Path.explode("~~/Admin/polyml/README"), component_dir)
val etc_dir = Isabelle_System.make_directory(component_dir + Path.explode("etc"))
File.copy(Path.explode("~~/Admin/polyml/settings"), etc_dir)
sha1_root match {
case Some(dir) =>
Mercurial.repository(dir).archive(File.standard_path(component_dir + Path.explode("sha1")))
case None =>
}
}
/** Isabelle tool wrappers **/
val isabelle_tool1 =
Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
{
var msys_root: Option[Path] = None
var arch_64 = Isabelle_Platform.self.is_arm
var sha1_root: Option[Path] = None
val getopts = Getopts("""
Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
Options are:
-M DIR msys root directory (for Windows)
-m ARCH processor architecture (32 or 64, default: """ +
(if (arch_64) "64" else "32") + """)
-s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1
Build Poly/ML in the ROOT directory of its sources, with additional
CONFIGURE_OPTIONS (e.g. --without-gmp).
""",
"M:" -> (arg => msys_root = Some(Path.explode(arg))),
"m:" ->
{
case "32" => arch_64 = false
case "64" => arch_64 = true
case bad => error("Bad processor architecture: " + quote(bad))
},
"s:" -> (arg => sha1_root = Some(Path.explode(arg))))
val more_args = getopts(args)
val (root, options) =
more_args match {
case root :: options => (Path.explode(root), options)
case Nil => getopts.usage()
}
build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
arch_64 = arch_64, options = options, msys_root = msys_root)
})
val isabelle_tool2 =
Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", args =>
{
var sha1_root: Option[Path] = None
val getopts = Getopts("""
Usage: isabelle build_polyml_component [OPTIONS] SOURCE_ARCHIVE COMPONENT_DIR
Options are:
-s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1
Make skeleton for Poly/ML component, based on official source archive
(zip or tar.gz).
""",
"s:" -> (arg => sha1_root = Some(Path.explode(arg))))
val more_args = getopts(args)
val (source_archive, component_dir) =
more_args match {
case List(archive, dir) => (Path.explode(archive), Path.explode(dir))
case _ => getopts.usage()
}
build_polyml_component(source_archive, component_dir, sha1_root = sha1_root)
})
}
diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala
+++ b/src/Pure/Admin/build_release.scala
@@ -1,846 +1,835 @@
/* Title: Pure/Admin/build_release.scala
Author: Makarius
Build full Isabelle distribution from repository.
*/
package isabelle
object Build_Release
{
/** release info **/
sealed case class Bundle_Info(
platform: Platform.Family.Value,
platform_description: String,
name: String)
{
def path: Path = Path.explode(name)
}
class Release private[Build_Release](
progress: Progress,
val date: Date,
val dist_name: String,
val dist_dir: Path,
val dist_version: String,
val ident: String)
{
val isabelle_dir: Path = dist_dir + Path.explode(dist_name)
val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
def other_isabelle(dir: Path): Other_Isabelle =
Other_Isabelle(dir + Path.explode(dist_name),
isabelle_identifier = dist_name + "-build",
progress = progress)
def bundle_info(platform: Platform.Family.Value): Bundle_Info =
platform match {
case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz")
case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
}
}
/** generated content **/
/* patch release */
- private def change_file(dir: Path, name: String, f: String => String)
- {
- val file = dir + Path.explode(name)
- File.write(file, f(File.read(file)))
- }
-
- private val getsettings_file: String = "lib/scripts/getsettings"
+ private val getsettings_path = Path.explode("lib/scripts/getsettings")
private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r
def patch_release(release: Release, is_official: Boolean)
{
val dir = release.isabelle_dir
for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala"))
{
- change_file(dir, name,
+ File.change(dir + Path.explode(name),
s =>
s.replaceAllLiterally("val is_identified = false", "val is_identified = true")
.replaceAllLiterally("val is_official = false", "val is_official = " + is_official))
}
- change_file(dir, getsettings_file,
- s =>
- s.replaceAllLiterally("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
- .replaceAllLiterally("ISABELLE_IDENTIFIER=\"\"",
- "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
+ File.change(dir + getsettings_path,
+ _.replaceAllLiterally("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
+ .replaceAllLiterally("ISABELLE_IDENTIFIER=\"\"",
+ "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
- change_file(dir, "lib/html/library_index_header.template",
- s => s.replaceAllLiterally("{ISABELLE}", release.dist_name))
+ File.change(dir + Path.explode("lib/html/library_index_header.template"),
+ _.replaceAllLiterally("{ISABELLE}", release.dist_name))
for {
name <-
List(
"src/Pure/System/distribution.ML",
"src/Pure/System/distribution.scala",
"lib/Tools/version") }
{
- change_file(dir, name,
+ File.change(dir + Path.explode(name),
s => s.replaceAllLiterally("repository version", release.dist_version))
}
- change_file(dir, "README",
+ File.change(dir + Path.explode("README"),
s => s.replaceAllLiterally("some repository version of Isabelle", release.dist_version))
}
/* ANNOUNCE */
def make_announce(release: Release)
{
File.write(release.isabelle_dir + Path.explode("ANNOUNCE"),
"""
IMPORTANT NOTE
==============
This is a snapshot of Isabelle/""" + release.ident + """ from the repository.
""")
}
/* NEWS */
def make_news(other_isabelle: Other_Isabelle, dist_version: String)
{
val target = other_isabelle.isabelle_home + Path.explode("doc")
val target_fonts = Isabelle_System.make_directory(target + Path.explode("fonts"))
other_isabelle.copy_fonts(target_fonts)
HTML.write_document(target, "NEWS.html",
List(HTML.title("NEWS (" + dist_version + ")")),
List(
HTML.chapter("NEWS"),
HTML.source(
Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS"))))))
}
/* bundled components */
class Bundled(platform: Option[Platform.Family.Value] = None)
{
def detect(s: String): Boolean =
s.startsWith("#bundled") && !s.startsWith("#bundled ")
def apply(name: String): String =
"#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name
private val Pattern1 = ("""^#bundled:(.*)$""").r
private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r
def unapply(s: String): Option[String] =
s match {
case Pattern1(name) => Some(name)
case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name)
case _ => None
}
}
def record_bundled_components(dir: Path)
{
val catalogs =
List("main", "bundled").map((_, new Bundled())) :::
default_platform_families.flatMap(platform =>
List(platform.toString, "bundled-" + platform.toString).
map((_, new Bundled(platform = Some(platform)))))
File.append(Components.components(dir),
terminate_lines("#bundled components" ::
(for {
(catalog, bundled) <- catalogs.iterator
path = Components.admin(dir) + Path.basic(catalog)
if path.is_file
line <- split_lines(File.read(path))
if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
} yield bundled(line)).toList))
}
def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) =
{
val Bundled = new Bundled(platform = Some(platform))
val components =
for {
Bundled(name) <- Components.read_components(dir)
if !name.startsWith("jedit_build")
} yield name
val jdk_component =
components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
(components, jdk_component)
}
def activate_components(dir: Path, platform: Platform.Family.Value, more_names: List[String])
{
def contrib_name(name: String): String =
Components.contrib(name = name).implode
val Bundled = new Bundled(platform = Some(platform))
Components.write_components(dir,
Components.read_components(dir).flatMap(line =>
line match {
case Bundled(name) =>
if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name))
else None
case _ => if (Bundled.detect(line)) None else Some(line)
}) ::: more_names.map(contrib_name))
}
def make_contrib(dir: Path)
{
Isabelle_System.make_directory(Components.contrib(dir))
File.write(Components.contrib(dir, "README"),
"""This directory contains add-on components that contribute to the main
Isabelle distribution. Separate licensing conditions apply, see each
directory individually.
""")
}
/** build release **/
private def execute(dir: Path, script: String): Unit =
Isabelle_System.bash(script, cwd = dir.file).check
private def execute_tar(dir: Path, args: String): Unit =
Isabelle_System.gnutar(args, dir = dir).check
/* build heaps on remote server */
private def remote_build_heaps(
options: Options,
platform: Platform.Family.Value,
build_sessions: List[String],
local_dir: Path)
{
val server_option = "build_host_" + platform.toString
options.string(server_option) match {
case SSH.Target(user, host) =>
using(SSH.open_session(options, host = host, user = user))(ssh =>
{
Isabelle_System.with_tmp_file("tmp", "tar")(local_tmp_tar =>
{
execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
ssh.with_tmp_dir(remote_dir =>
{
val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
ssh.write_file(remote_tmp_tar, local_tmp_tar)
val remote_commands =
List(
"cd " + File.bash_path(remote_dir),
"tar -xf tmp.tar",
"./bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
"tar -cf tmp.tar heaps")
ssh.execute(remote_commands.mkString(" && ")).check
ssh.read_file(remote_tmp_tar, local_tmp_tar)
})
execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
})
})
case s => error("Bad " + server_option + ": " + quote(s))
}
}
/* main */
private val default_platform_families: List[Platform.Family.Value] =
List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
def build_release(base_dir: Path,
options: Options,
components_base: Path = Components.default_components_base,
progress: Progress = new Progress,
rev: String = "",
afp_rev: String = "",
official_release: Boolean = false,
proper_release_name: Option[String] = None,
platform_families: List[Platform.Family.Value] = default_platform_families,
more_components: List[Path] = Nil,
website: Option[Path] = None,
build_sessions: List[String] = Nil,
build_library: Boolean = false,
parallel_jobs: Int = 1): Release =
{
val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME"))
val release =
{
val date = Date.now()
val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date))
val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute
val version = proper_string(rev) orElse proper_release_name getOrElse "tip"
val ident =
try { hg.id(version) }
catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
val dist_version =
proper_release_name match {
case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date)
case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
}
new Release(progress, date, dist_name, dist_dir, dist_version, ident)
}
/* make distribution */
if (release.isabelle_archive.is_file) {
progress.echo_warning("Release archive already exists: " + release.isabelle_archive)
val archive_ident =
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
- val getsettings = Path.explode(release.dist_name + "/" + getsettings_file)
+ val getsettings = Path.explode(release.dist_name) + getsettings_path
execute_tar(tmp_dir, "-xzf " +
File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings))
split_lines(File.read(tmp_dir + getsettings))
.collectFirst({ case ISABELLE_ID(ident) => ident })
.getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive))
})
if (release.ident != archive_ident) {
error("Mismatch of release identification " + release.ident +
" vs. archive " + archive_ident)
}
}
else {
progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...")
Isabelle_System.make_directory(release.dist_dir)
if (release.isabelle_dir.is_dir)
error("Directory " + release.isabelle_dir + " already exists")
progress.echo_warning("Retrieving Mercurial repository version " + release.ident)
hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files")
for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
(release.isabelle_dir + Path.explode(name)).file.delete
}
progress.echo_warning("Preparing distribution " + quote(release.dist_name))
patch_release(release, proper_release_name.isDefined && official_release)
if (proper_release_name.isEmpty) make_announce(release)
make_contrib(release.isabelle_dir)
execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
record_bundled_components(release.isabelle_dir)
/* build tools and documentation */
val other_isabelle = release.other_isabelle(release.dist_dir)
other_isabelle.init_settings(
other_isabelle.init_components(components_base = components_base, catalogs = List("main")))
other_isabelle.resolve_components(echo = true)
try {
val export_classpath =
"export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) }
try {
other_isabelle.bash(
"./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) }
make_news(other_isabelle, release.dist_version)
for (name <- List("Admin", "browser_info", "heaps")) {
Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
}
other_isabelle.cleanup()
progress.echo_warning("Creating distribution archive " + release.isabelle_archive)
def execute_dist_name(script: String): Unit =
Isabelle_System.bash(script, cwd = release.dist_dir.file,
env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check
execute_dist_name("""
set -e
chmod -R a+r "$DIST_NAME"
chmod -R u+w "$DIST_NAME"
chmod -R g=o "$DIST_NAME"
find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
""")
execute_tar(release.dist_dir, "-czf " +
File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
execute_dist_name("""
set -e
mv "$DIST_NAME" "${DIST_NAME}-old"
mkdir "$DIST_NAME"
mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \
"${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME"
mkdir "$DIST_NAME/doc"
mv "${DIST_NAME}-old/doc/"*.pdf \
"${DIST_NAME}-old/doc/"*.html \
"${DIST_NAME}-old/doc/"*.css \
"${DIST_NAME}-old/doc/fonts" \
"${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc"
rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle
rm -rf "${DIST_NAME}-old"
""")
}
/* make application bundles */
val bundle_infos = platform_families.map(release.bundle_info)
for (bundle_info <- bundle_infos) {
val isabelle_name = release.dist_name
val platform = bundle_info.platform
progress.echo("\nApplication bundle for " + platform)
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
// release archive
execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
val other_isabelle = release.other_isabelle(tmp_dir)
val isabelle_target = other_isabelle.isabelle_home
// bundled components
progress.echo("Bundled components:")
val contrib_dir = Components.contrib(isabelle_target)
val (bundled_components, jdk_component) =
get_bundled_components(isabelle_target, platform)
Components.resolve(components_base, bundled_components,
target_dir = Some(contrib_dir),
copy_dir = Some(release.dist_dir + Path.explode("contrib")),
progress = progress)
val more_components_names =
more_components.map(Components.unpack(contrib_dir, _, progress = progress))
Components.purge(contrib_dir, platform)
activate_components(isabelle_target, platform, more_components_names)
// Java parameters
val java_options_title = "# Java runtime options"
val java_options: List[String] =
(for {
variable <-
List(
"ISABELLE_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_OPTIONS")
opt <- Word.explode(other_isabelle.getenv(variable))
} yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name)
val classpath: List[Path] =
{
val base = isabelle_target.absolute
Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
{
val abs_path = path.absolute
File.relative_path(base, abs_path) match {
case Some(rel_path) => rel_path
case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
}
}) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
}
val jedit_options = Path.explode("src/Tools/jEdit/etc/options")
val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
// build heaps
if (build_sessions.nonEmpty) {
progress.echo("Building heaps ...")
remote_build_heaps(options, platform, build_sessions, isabelle_target)
}
// application bundling
platform match {
case Platform.Family.linux =>
- File.write(isabelle_target + jedit_options,
- File.read(isabelle_target + jedit_options)
- .replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24"))
+ File.change(isabelle_target + jedit_options,
+ _.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24"))
- File.write(isabelle_target + jedit_props,
- File.read(isabelle_target + jedit_props)
- .replaceAll("console.fontsize=.*", "console.fontsize=18")
- .replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18")
- .replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18")
- .replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18")
- .replaceAll("view.fontsize=.*", "view.fontsize=24")
- .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16"))
+ File.change(isabelle_target + jedit_props,
+ _.replaceAll("console.fontsize=.*", "console.fontsize=18")
+ .replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18")
+ .replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18")
+ .replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18")
+ .replaceAll("view.fontsize=.*", "view.fontsize=24")
+ .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16"))
File.write(isabelle_target + Path.explode("Isabelle.options"),
terminate_lines(java_options_title :: java_options))
val isabelle_app = isabelle_target + Path.explode("lib/scripts/Isabelle_app")
File.write(isabelle_app,
File.read(Path.explode("~~/Admin/Linux/Isabelle_app"))
.replaceAllLiterally("{CLASSPATH}",
classpath.map("$ISABELLE_HOME/" + _).mkString(":"))
.replaceAllLiterally("/jdk/", "/" + jdk_component + "/"))
File.set_executable(isabelle_app, true)
val linux_app = isabelle_target + Path.explode("contrib/linux_app")
File.move(linux_app + Path.explode("Isabelle"),
isabelle_target + Path.explode(isabelle_name))
Isabelle_System.rm_tree(linux_app)
val archive_name = isabelle_name + "_linux.tar.gz"
progress.echo("Packaging " + archive_name + " ...")
execute_tar(tmp_dir,
"-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
Bash.string(isabelle_name))
case Platform.Family.macos =>
- File.write(isabelle_target + jedit_props,
- File.read(isabelle_target + jedit_props)
- .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
- .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
- .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
+ File.change(isabelle_target + jedit_props,
+ _.replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
+ .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
+ .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
// MacOS application bundle
File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
val isabelle_app = Path.explode(isabelle_name + ".app")
val app_dir = tmp_dir + isabelle_app
File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir)
val app_contents = app_dir + Path.explode("Contents")
val app_resources = app_contents + Path.explode("Resources")
File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
File.write(app_contents + Path.explode("Info.plist"),
File.read(Path.explode("~~/Admin/MacOS/Info.plist"))
.replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
.replaceAllLiterally("{JAVA_OPTIONS}",
terminate_lines(java_options.map(opt => "" + opt + ""))))
for (cp <- classpath) {
File.link(
Path.explode("../Resources/" + isabelle_name + "/") + cp,
app_contents + Path.explode("Java"),
force = true)
}
File.link(
Path.explode("../Resources/" + isabelle_name + "/contrib/" +
jdk_component + "/x86_64-darwin"),
app_contents + Path.explode("PlugIns/bundled.jdk"),
force = true)
File.link(
Path.explode("../../Info.plist"),
app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"),
force = true)
File.link(
Path.explode("Contents/Resources/" + isabelle_name),
app_dir + Path.explode("Isabelle"),
force = true)
// application archive
val archive_name = isabelle_name + "_macos.tar.gz"
progress.echo("Packaging " + archive_name + " ...")
execute_tar(tmp_dir,
"-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
File.bash_path(isabelle_app))
case Platform.Family.windows =>
- File.write(isabelle_target + jedit_props,
- File.read(isabelle_target + jedit_props)
- .replaceAll("lookAndFeel=.*",
+ File.change(isabelle_target + jedit_props,
+ _.replaceAll("lookAndFeel=.*",
"lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
- .replaceAll("foldPainter=.*", "foldPainter=Square"))
+ .replaceAll("foldPainter=.*", "foldPainter=Square"))
// application launcher
File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
val app_template = Path.explode("~~/Admin/Windows/launch4j")
File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
(java_options_title :: java_options).map(_ + "\r\n").mkString)
val isabelle_xml = Path.explode("isabelle.xml")
val isabelle_exe = Path.explode(isabelle_name + ".exe")
File.write(tmp_dir + isabelle_xml,
File.read(app_template + isabelle_xml)
.replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
.replaceAllLiterally("{OUTFILE}",
File.platform_path(isabelle_target + isabelle_exe))
.replaceAllLiterally("{ICON}",
File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
.replaceAllLiterally("{SPLASH}",
File.platform_path(app_template + Path.explode("isabelle.bmp")))
.replaceAllLiterally("{CLASSPATH}",
cat_lines(classpath.map(cp =>
" %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "")))
.replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\"))
execute(tmp_dir,
"\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
File.copy(app_template + Path.explode("manifest.xml"),
isabelle_target + isabelle_exe.ext("manifest"))
// Cygwin setup
val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
val cygwin_mirror =
File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
val cygwin_bat = Path.explode("Cygwin-Setup.bat")
File.write(isabelle_target + cygwin_bat,
File.read(cygwin_template + cygwin_bat)
.replaceAllLiterally("{MIRROR}", cygwin_mirror))
File.set_executable(isabelle_target + cygwin_bat, true)
for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
val path = Path.explode(name)
File.copy(cygwin_template + path,
isabelle_target + Path.explode("contrib/cygwin") + path)
}
execute(isabelle_target,
"""find . -type f -not -name "*.exe" -not -name "*.dll" """ +
(if (Platform.is_macos) "-perm +100" else "-executable") +
" -print0 > contrib/cygwin/isabelle/executables")
execute(isabelle_target,
"""find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
"""> contrib/cygwin/isabelle/symlinks""")
execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
// executable archive (self-extracting 7z)
val archive_name = isabelle_name + ".7z"
val exe_archive = tmp_dir + Path.explode(archive_name)
exe_archive.file.delete
progress.echo("Packaging " + archive_name + " ...")
execute(tmp_dir,
"7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
val sfx_txt =
File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")).
replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
Bytes.write(release.dist_dir + isabelle_exe,
Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
File.set_executable(release.dist_dir + isabelle_exe, true)
}
})
progress.echo("DONE")
}
/* minimal website */
for (dir <- website) {
val website_platform_bundles =
for {
bundle_info <- bundle_infos
if (release.dist_dir + bundle_info.path).is_file
} yield (bundle_info.name, bundle_info)
val isabelle_link =
HTML.link(Isabelle_Cronjob.isabelle_repos_source + "/rev/" + release.ident,
HTML.text("Isabelle/" + release.ident))
val afp_link =
HTML.link(AFP.repos_source + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev))
HTML.write_document(dir, "index.html",
List(HTML.title(release.dist_name)),
List(
HTML.section(release.dist_name),
HTML.subsection("Platforms"),
HTML.itemize(
website_platform_bundles.map({ case (bundle, bundle_info) =>
List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) })),
HTML.subsection("Repositories"),
HTML.itemize(
List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
for ((bundle, _) <- website_platform_bundles)
File.copy(release.dist_dir + Path.explode(bundle), dir)
}
/* HTML library */
if (build_library) {
if (release.isabelle_library_archive.is_file) {
progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive)
}
else {
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
val bundle =
release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz")
execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
val other_isabelle = release.other_isabelle(tmp_dir)
Isabelle_System.make_directory(other_isabelle.etc)
File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
" -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
" -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
other_isabelle.isabelle_home_user.file.delete
execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name))
execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name))
execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) +
" " + Bash.string(release.dist_name + "/browser_info"))
})
}
}
release
}
/** command line entry point **/
def main(args: Array[String])
{
Command_Line.tool {
var afp_rev = ""
var components_base: Path = Components.default_components_base
var official_release = false
var proper_release_name: Option[String] = None
var website: Option[Path] = None
var build_sessions: List[String] = Nil
var more_components: List[Path] = Nil
var parallel_jobs = 1
var build_library = false
var options = Options.init()
var platform_families = default_platform_families
var rev = ""
val getopts = Getopts("""
Usage: Admin/build_release [OPTIONS] BASE_DIR
Options are:
-A REV corresponding AFP changeset id
-C DIR base directory for Isabelle components (default: """ +
Components.default_components_base + """)
-O official release (not release-candidate)
-R RELEASE proper release with name
-W WEBSITE produce minimal website in given directory
-b SESSIONS build platform-specific session images (separated by commas)
-c ARCHIVE clean bundling with additional component .tar.gz archive
-j INT maximum number of parallel jobs (default 1)
-l build library
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p NAMES platform families (default: """ + default_platform_families.mkString(",") + """)
-r REV Mercurial changeset id (default: RELEASE or tip)
Build Isabelle release in base directory, using the local repository clone.
""",
"A:" -> (arg => afp_rev = arg),
"C:" -> (arg => components_base = Path.explode(arg)),
"O" -> (_ => official_release = true),
"R:" -> (arg => proper_release_name = Some(arg)),
"W:" -> (arg => website = Some(Path.explode(arg))),
"b:" -> (arg => build_sessions = space_explode(',', arg)),
"c:" -> (arg =>
{
val path = Path.explode(arg)
Components.Archive.get_name(path.file_name)
more_components = more_components ::: List(path)
}),
"j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
"l" -> (_ => build_library = true),
"o:" -> (arg => options = options + arg),
"p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)),
"r:" -> (arg => rev = arg))
val more_args = getopts(args)
val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() }
val progress = new Console_Progress()
if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
error("Building for windows requires 7z")
build_release(Path.explode(base_dir), options, components_base = components_base,
progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release,
proper_release_name = proper_release_name, website = website,
platform_families =
if (platform_families.isEmpty) default_platform_families
else platform_families,
more_components = more_components, build_sessions = build_sessions,
build_library = build_library, parallel_jobs = parallel_jobs)
}
}
}
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,360 +1,366 @@
/* 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, StandardCopyOption, Path => JPath,
Files, SimpleFileVisitor, FileVisitOption, FileVisitResult, FileSystemException}
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
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
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 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) { 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)
}
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: CharSequence, make_stream: OutputStream => OutputStream)
{
val stream = make_stream(new FileOutputStream(file))
using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text))
}
def write(file: JFile, text: CharSequence): Unit = write_file(file, text, s => s)
def write(path: Path, text: CharSequence): Unit = write(path.file, text)
def write_gzip(file: JFile, text: CharSequence): Unit =
write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s)))
def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text)
def write_xz(file: JFile, text: CharSequence, options: XZ.Options): Unit =
File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options))
def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, XZ.options())
def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit =
write_xz(path.file, text, options)
def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options())
def write_backup(path: Path, text: CharSequence)
{
if (path.is_file) move(path, path.backup)
write(path, text)
}
def write_backup2(path: Path, text: CharSequence)
{
if (path.is_file) move(path, path.backup2)
write(path, text)
}
+ /* change */
+
+ def change(file: JFile, f: String => String): Unit = write(file, f(read(file)))
+ def change(path: Path, f: String => String): Unit = write(path, f(read(path)))
+
+
/* append */
def append(file: JFile, text: CharSequence): Unit =
Files.write(file.toPath, UTF8.bytes(text.toString),
StandardOpenOption.APPEND, StandardOpenOption.CREATE)
def append(path: Path, text: CharSequence): Unit = append(path.file, text)
/* eq */
def eq(file1: JFile, file2: JFile): Boolean =
try { java.nio.file.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)
/* copy */
def copy(src: JFile, dst: JFile)
{
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
if (!eq(src, target))
Files.copy(src.toPath, target.toPath,
StandardCopyOption.COPY_ATTRIBUTES,
StandardCopyOption.REPLACE_EXISTING)
}
def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
/* move */
def move(src: JFile, dst: JFile)
{
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
if (!eq(src, target))
Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
}
def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file)
/* symbolic link */
def link(src: Path, dst: Path, force: Boolean = false)
{
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(standard_path(src), target)
case _: FileSystemException if Platform.is_windows =>
Cygwin.link(standard_path(src), target)
}
}
/* 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)
{
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)
}
}