diff --git a/src/Pure/Admin/build_csdp.scala b/src/Pure/Admin/build_csdp.scala --- a/src/Pure/Admin/build_csdp.scala +++ b/src/Pure/Admin/build_csdp.scala @@ -1,199 +1,198 @@ /* Title: Pure/Admin/build_csdp.scala Author: Makarius Build Isabelle CSDP component from official download. */ package isabelle object Build_CSDP { // Note: version 6.2.0 does not quite work for the "sos" proof method val default_download_url = "https://github.com/coin-or/Csdp/archive/releases/6.1.1.tar.gz" /* flags */ sealed case class Flags(platform: String, CFLAGS: String = "", LIBS: String = "") { val changed: List[(String, String)] = List("CFLAGS" -> CFLAGS, "LIBS" -> LIBS).filter(p => p._2.nonEmpty) def print: Option[String] = if (changed.isEmpty) None else Some(" * " + platform + ":\n" + changed.map(p => " " + Properties.Eq(p)) .mkString("\n")) def change(path: Path): Unit = { def change_line(line: String, p: (String, String)): String = line.replaceAll(p._1 + "=.*", Properties.Eq(p)) File.change_lines(path) { _.map(line => changed.foldLeft(line)(change_line)) } } } val build_flags: List[Flags] = List( Flags("arm64-linux", CFLAGS = "-O3 -ansi -Wall -DNOSHORTS -DBIT64 -DUSESIGTERM -DUSEGETTIME -I../include", LIBS = "-static -L../lib -lsdp -llapack -lblas -lgfortran -lm"), Flags("x86_64-linux", CFLAGS = "-O3 -ansi -Wall -DNOSHORTS -DBIT64 -DUSESIGTERM -DUSEGETTIME -I../include", LIBS = "-static -L../lib -lsdp -llapack -lblas -lgfortran -lquadmath -lm"), Flags("x86_64-darwin", CFLAGS = "-O3 -Wall -DNOSHORTS -DBIT64 -DUSESIGTERM -DUSEGETTIME -I../include", LIBS = "-L../lib -lsdp -llapack -lblas -lm"), Flags("x86_64-windows")) /* build CSDP */ def build_csdp( download_url: String = default_download_url, verbose: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current, mingw: MinGW = MinGW.none ): Unit = { mingw.check Isabelle_System.with_tmp_dir("build") { tmp_dir => /* component */ val Archive_Name = """^.*?([^/]+)$""".r val Version = """^[^0-9]*([0-9].*)\.tar.gz$""".r val archive_name = download_url match { case Archive_Name(name) => name case _ => error("Failed to determine source archive name from " + quote(download_url)) } val version = archive_name match { case Version(version) => version case _ => error("Failed to determine component version from " + quote(archive_name)) } val component_name = "csdp-" + version val component_dir = Components.Directory.create(target_dir + Path.basic(component_name), progress = progress) /* platform */ val platform_name = proper_string(Isabelle_System.getenv("ISABELLE_WINDOWS_PLATFORM64")) orElse proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse error("No 64bit platform") val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name)) /* download source */ val archive_path = tmp_dir + Path.basic(archive_name) Isabelle_System.download_file(download_url, archive_path, progress = progress) Isabelle_System.extract(archive_path, tmp_dir) val source_dir = File.get_dir(tmp_dir, title = download_url) - Isabelle_System.extract(archive_path, component_dir.path) - Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src) + Isabelle_System.extract(archive_path, component_dir.src, strip = true) /* build */ progress.echo("Building CSDP for " + platform_name + " ...") build_flags.find(flags => flags.platform == platform_name) match { case None => error("No build flags for platform " + quote(platform_name)) case Some(flags) => File.find_files(source_dir.file, pred = file => file.getName == "Makefile"). foreach(file => flags.change(File.path(file))) } progress.bash(mingw.bash_script("make"), cwd = source_dir.file, echo = verbose).check /* install */ Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path) Isabelle_System.copy_file(source_dir + Path.explode("solver/csdp").platform_exe, platform_dir) if (Platform.is_windows) { Executable.libraries_closure(platform_dir + Path.explode("csdp.exe"), mingw = mingw, filter = Set("libblas", "liblapack", "libgfortran", "libgcc_s_seh", "libquadmath", "libwinpthread")) } /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: ISABELLE_CSDP="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/csdp" """) /* README */ File.write(component_dir.README, """This is CSDP """ + version + """ from """ + download_url + """ Makefile flags have been changed for various platforms as follows: """ + build_flags.flatMap(_.print).mkString("\n\n") + """ The distribution has been built like this: cd src && make Only the bare "solver/csdp" program is used for Isabelle. Makarius """ + Date.Format.date(Date.now()) + "\n") } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_csdp", "build prover component from official download", Scala_Project.here, { args => var target_dir = Path.current var mingw = MinGW.none var download_url = default_download_url var verbose = false val getopts = Getopts(""" Usage: isabelle build_csdp [OPTIONS] Options are: -D DIR target directory (default ".") -M DIR msys/mingw root specification for Windows -U URL download URL (default: """" + default_download_url + """") -v verbose Build prover component from official download. """, "D:" -> (arg => target_dir = Path.explode(arg)), "M:" -> (arg => mingw = MinGW(Path.explode(arg))), "U:" -> (arg => download_url = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_csdp(download_url = download_url, verbose = verbose, progress = progress, target_dir = target_dir, mingw = mingw) }) } 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,141 +1,140 @@ /* 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.6" val default_download_url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD" def build_e( version: String = default_version, download_url: String = default_download_url, verbose: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current ): Unit = { Isabelle_System.with_tmp_dir("build") { tmp_dir => /* component */ val component_name = "e-" + version val component_dir = Components.Directory.create(target_dir + Path.basic(component_name), progress = progress) 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 + Path.basic(platform_name)) /* download source */ val archive_url = download_url + "/V_" + version + "/E.tgz" val archive_path = tmp_dir + Path.explode("E.tgz") Isabelle_System.download_file(archive_url, archive_path, progress = progress) Isabelle_System.extract(archive_path, tmp_dir) val source_dir = File.get_dir(tmp_dir, title = archive_url) - Isabelle_System.extract(archive_path, component_dir.path) - Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src) + Isabelle_System.extract(archive_path, component_dir.src, strip = true) /* build */ progress.echo("Building E prover for " + platform_name + " ...") val build_options = { val result = Isabelle_System.bash("./configure --help", cwd = source_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 = source_dir.file, progress_stdout = progress.echo_if(verbose, _), progress_stderr = progress.echo_if(verbose, _)).check /* install */ Isabelle_System.copy_file(source_dir + Path.basic("COPYING"), component_dir.LICENSE) val install_files = List("epclextract", "eprover", "eprover-ho") for (name <- install_files ::: install_files.map(_ + ".exe")) { val path = source_dir + Path.basic("PROVER") + Path.basic(name) if (path.is_file) Isabelle_System.copy_file(path, platform_dir) } Isabelle_System.bash("if [ -f eprover-ho ]; then mv eprover-ho eprover; fi", cwd = platform_dir.file).check /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: E_HOME="$COMPONENT/$ISABELLE_PLATFORM64" E_VERSION=""" + quote(version) + """ """) /* README */ File.write(component_dir.README, "This is E prover " + version + " from\n" + archive_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. Makarius """ + Date.Format.date(Date.now()) + "\n") } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_e", "build prover component from source distribution", Scala_Project.here, { args => var target_dir = Path.current var version = default_version var download_url = default_download_url var verbose = false val getopts = Getopts(""" Usage: isabelle build_e [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_download_url + """") -V VERSION version (default: """ + default_version + """) -v verbose Build prover component from the specified source distribution. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => download_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, verbose = verbose, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/build_jdk.scala b/src/Pure/Admin/build_jdk.scala --- a/src/Pure/Admin/build_jdk.scala +++ b/src/Pure/Admin/build_jdk.scala @@ -1,169 +1,167 @@ /* Title: Pure/Admin/build_jdk.scala Author: Makarius Build Isabelle jdk component using downloads from Azul. */ package isabelle import java.nio.file.Files import java.nio.file.attribute.PosixFilePermission object Build_JDK { /* platform information */ sealed case class JDK_Platform(name: String, url_template: String) { override def toString: String = name def url(base_url: String, jdk_version: String, zulu_version: String): String = base_url + "/" + url_template.replace("{V}", jdk_version).replace("{Z}", zulu_version) } val platforms: List[JDK_Platform] = List( JDK_Platform("arm64-darwin", "zulu{Z}-jdk{V}-macosx_aarch64.tar.gz"), JDK_Platform("arm64-linux", "zulu{Z}-jdk{V}-linux_aarch64.tar.gz"), JDK_Platform("x86_64-darwin", "zulu{Z}-jdk{V}-macosx_x64.tar.gz"), JDK_Platform("x86_64-linux", "zulu{Z}-jdk{V}-linux_x64.tar.gz"), JDK_Platform("x86_64-windows", "zulu{Z}-jdk{V}-win_x64.zip")) /* build jdk */ val default_base_url = "https://cdn.azul.com/zulu/bin" val default_jdk_version = "17.0.5" val default_zulu_version = "17.38.21-ca" def build_jdk( target_dir: Path = Path.current, base_url: String = default_base_url, jdk_version: String = default_jdk_version, zulu_version: String = default_zulu_version, progress: Progress = new Progress, ): Unit = { if (Platform.is_windows) error("Cannot build on Windows") /* component */ val component = "jdk-" + jdk_version val component_dir = Components.Directory.create(target_dir + Path.basic(component), progress = progress) /* download */ for (platform <- platforms) { Isabelle_System.with_tmp_dir("download", component_dir.path.file) { dir => val url = platform.url(base_url, jdk_version, zulu_version) val name = Library.take_suffix(_ != '/', url.toList)._2.mkString val file = dir + Path.basic(name) Isabelle_System.download_file(url, file, progress = progress) - Isabelle_System.extract(file, dir) - val jdk_dir = File.get_dir(dir, title = url) val platform_dir = component_dir.path + Path.basic(platform.name) - Isabelle_System.move_file(jdk_dir, platform_dir) + Isabelle_System.extract(file, platform_dir, strip = true) } } /* permissions */ for (file <- File.find_files(component_dir.path.file, include_dirs = true)) { val path = file.toPath val perms = Files.getPosixFilePermissions(path) perms.add(PosixFilePermission.OWNER_READ) perms.add(PosixFilePermission.GROUP_READ) perms.add(PosixFilePermission.OTHERS_READ) perms.add(PosixFilePermission.OWNER_WRITE) if (file.isDirectory) { perms.add(PosixFilePermission.OWNER_WRITE) perms.add(PosixFilePermission.OWNER_EXECUTE) perms.add(PosixFilePermission.GROUP_EXECUTE) perms.add(PosixFilePermission.OTHERS_EXECUTE) } Files.setPosixFilePermissions(path, perms) } /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: case "$ISABELLE_PLATFORM_FAMILY" in linux) ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; windows) ISABELLE_JAVA_PLATFORM="$ISABELLE_WINDOWS_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; macos) if [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$COMPONENT/$ISABELLE_APPLE_PLATFORM64" ] then ISABELLE_JAVA_PLATFORM="$ISABELLE_APPLE_PLATFORM64" else ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64" fi ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; esac """) /* README */ File.write(component_dir.README, """This is OpenJDK """ + jdk_version + """ based on downloads by Azul, see also https://www.azul.com/downloads/?package=jdk The main license is GPL2, but some modules are covered by other (more liberal) licenses, see legal/* for details. Linux, Windows, macOS all work uniformly, depending on platform-specific subdirectories. """) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_jdk", "build Isabelle jdk component using downloads from Azul", Scala_Project.here, { args => var target_dir = Path.current var base_url = default_base_url var jdk_version = default_jdk_version var zulu_version = default_zulu_version val getopts = Getopts(""" Usage: isabelle build_jdk [OPTIONS] Options are: -D DIR target directory (default ".") -U URL base URL (default: """" + default_base_url + """") -V NAME JDK version (default: """" + default_jdk_version + """") -Z NAME Zulu version (default: """" + default_zulu_version + """") Build Isabelle jdk component using downloads from Azul. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => base_url = arg), "V:" -> (arg => jdk_version = arg), "Z:" -> (arg => zulu_version = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_jdk(target_dir = target_dir, base_url = base_url, jdk_version = jdk_version, zulu_version = zulu_version, progress = progress) }) } diff --git a/src/Pure/Admin/build_minisat.scala b/src/Pure/Admin/build_minisat.scala --- a/src/Pure/Admin/build_minisat.scala +++ b/src/Pure/Admin/build_minisat.scala @@ -1,153 +1,152 @@ /* Title: Pure/Admin/build_minisat.scala Author: Makarius Build Isabelle Minisat from sources. */ package isabelle object Build_Minisat { val default_download_url = "https://github.com/stp/minisat/archive/releases/2.2.1.tar.gz" def make_component_name(version: String): String = "minisat-" + version /* build Minisat */ def build_minisat( download_url: String = default_download_url, component_name: String = "", verbose: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current ): Unit = { Isabelle_System.with_tmp_dir("build") { tmp_dir => /* component */ val Archive_Name = """^.*?([^/]+)$""".r val Version = """^v?([0-9.]+)\.tar.gz$""".r val archive_name = download_url match { case Archive_Name(name) => name case _ => error("Failed to determine source archive name from " + quote(download_url)) } val version = archive_name match { case Version(version) => version case _ => error("Failed to determine component version from " + quote(archive_name)) } val component = proper_string(component_name) getOrElse make_component_name(version) val component_dir = Components.Directory.create(target_dir + Path.basic(component), progress = progress) /* platform */ 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 + Path.basic(platform_name)) /* download source */ val archive_path = tmp_dir + Path.basic(archive_name) Isabelle_System.download_file(download_url, archive_path, progress = progress) Isabelle_System.extract(archive_path, tmp_dir) val source_dir = File.get_dir(tmp_dir, title = download_url) - Isabelle_System.extract(archive_path, component_dir.path) - Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src) + Isabelle_System.extract(archive_path, component_dir.src, strip = true) /* build */ progress.echo("Building Minisat for " + platform_name + " ...") Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path) if (Platform.is_macos) { File.change(source_dir + Path.explode("Makefile")) { _.replaceAll("--static", "").replaceAll("-Wl,-soname\\S+", "") } } progress.bash("make r", source_dir.file, echo = verbose).check Isabelle_System.copy_file( source_dir + Path.explode("build/release/bin/minisat").platform_exe, platform_dir) if (Platform.is_windows) { Isabelle_System.copy_file(Path.explode("/bin/cygwin1.dll"), platform_dir) } /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: MINISAT_HOME="$COMPONENT/$ISABELLE_PLATFORM64" ISABELLE_MINISAT="$MINISAT_HOME/minisat" """) /* README */ File.write(component_dir.README, "This Isabelle component provides Minisat " + version + """ using the sources from """.stripMargin + download_url + """ The executables have been built via "make r"; macOS requires to remove options "--static" and "-Wl,-soname,..." from the Makefile. Makarius """ + Date.Format.date(Date.now()) + "\n") } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_minisat", "build prover component from sources", Scala_Project.here, { args => var target_dir = Path.current var download_url = default_download_url var component_name = "" var verbose = false val getopts = Getopts(""" Usage: isabelle build_minisat [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_download_url + """") -n NAME component name (default: """" + make_component_name("VERSION") + """") -v verbose Build prover component from official download. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => download_url = arg), "n:" -> (arg => component_name = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_minisat(download_url = download_url, component_name = component_name, verbose = verbose, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/build_spass.scala b/src/Pure/Admin/build_spass.scala --- a/src/Pure/Admin/build_spass.scala +++ b/src/Pure/Admin/build_spass.scala @@ -1,176 +1,175 @@ /* Title: Pure/Admin/build_spass.scala Author: Makarius Build Isabelle SPASS component from unofficial download. */ package isabelle object Build_SPASS { /* build SPASS */ val default_download_url = "https://www.cs.vu.nl/~jbe248/spass-3.8ds-src.tar.gz" val standard_version = "3.8ds" def build_spass( download_url: String = default_download_url, verbose: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current): Unit = { Isabelle_System.with_tmp_dir("build") { tmp_dir => Isabelle_System.require_command("bison") Isabelle_System.require_command("flex") /* component */ val Archive_Name = """^.*?([^/]+)$""".r val Component_Name = """^(.+)-src\.tar.gz$""".r val Version = """^[^-]+-([^-]+)$""".r val archive_name = download_url match { case Archive_Name(name) => name case _ => error("Failed to determine source archive name from " + quote(download_url)) } val component_name = archive_name match { case Component_Name(name) => name case _ => error("Failed to determine component name from " + quote(archive_name)) } val version = component_name match { case Version(version) => version case _ => error("Failed to determine component version from " + quote(component_name)) } if (version != standard_version) { progress.echo_warning("Odd SPASS version " + version + " (expected " + standard_version + ")") } val component_dir = Components.Directory.create(target_dir + Path.basic(component_name), progress = progress) 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 + Path.basic(platform_name)) /* download source */ val archive_path = tmp_dir + Path.basic(archive_name) Isabelle_System.download_file(download_url, archive_path, progress = progress) Isabelle_System.extract(archive_path, tmp_dir) val source_dir = File.get_dir(tmp_dir, title = download_url) - Isabelle_System.extract(archive_path, component_dir.path) - Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src) + Isabelle_System.extract(archive_path, component_dir.src, strip = true) /* build */ progress.echo("Building SPASS for " + platform_name + " ...") if (Platform.is_windows) { File.change(source_dir + Path.basic("misc.c")) { _.replace("""#include "execinfo.h" """, "") .replaceAll("""void misc_DumpCore\(void\)[^}]+}""", "void misc_DumpCore(void) { abort(); }") } } Isabelle_System.bash("make", cwd = source_dir.file, progress_stdout = progress.echo_if(verbose, _), progress_stderr = progress.echo_if(verbose, _)).check /* install */ Isabelle_System.copy_file(source_dir + Path.basic("LICENCE"), component_dir.LICENSE) val install_files = List("SPASS") for (name <- install_files ::: install_files.map(_ + ".exe")) { val path = source_dir + Path.basic(name) if (path.is_file) Isabelle_System.copy_file(path, platform_dir) } /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: SPASS_HOME="$COMPONENT/$ISABELLE_PLATFORM64" SPASS_VERSION=""" + quote(version) + """ """) /* README */ File.write(component_dir.README, """This distribution of SPASS 3.8ds, described in Blanchette, Popescu, Wand, and Weidenbach's ITP 2012 paper "More SPASS with Isabelle", has been compiled from sources available at """ + download_url + """ via "make". The Windows/Cygwin compilation required commenting out the line #include "execinfo.h" in "misc.c" as well as most of the body of the "misc_DumpCore" function. The latest official SPASS sources can be downloaded from http://www.spass-prover.org/. Be aware, however, that the official SPASS releases are not compatible with Isabelle. Viel SPASS! Jasmin Blanchette 16-May-2018 Makarius """ + Date.Format.date(Date.now()) + "\n") } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_spass", "build prover component from source distribution", Scala_Project.here, { args => var target_dir = Path.current var download_url = default_download_url var verbose = false val getopts = Getopts(""" Usage: isabelle build_spass [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_download_url + """") -v verbose Build prover component from the specified source distribution. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => download_url = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_spass(download_url = download_url, verbose = verbose, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/build_vampire.scala b/src/Pure/Admin/build_vampire.scala --- a/src/Pure/Admin/build_vampire.scala +++ b/src/Pure/Admin/build_vampire.scala @@ -1,162 +1,161 @@ /* Title: Pure/Admin/build_vampire.scala Author: Makarius Build Isabelle Vampire component from official download. */ package isabelle object Build_Vampire { val default_download_url = "https://github.com/vprover/vampire/archive/refs/tags/v4.6.tar.gz" val default_jobs = 1 def make_component_name(version: String): String = "vampire-" + Library.try_unprefix("v", version).getOrElse(version) /* build Vampire */ def build_vampire( download_url: String = default_download_url, jobs: Int = default_jobs, component_name: String = "", verbose: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current ): Unit = { Isabelle_System.require_command("cmake") Isabelle_System.with_tmp_dir("build") { tmp_dir => /* component */ val Archive_Name = """^.*?([^/]+)$""".r val Version = """^v?([0-9.]+)\.tar.gz$""".r val archive_name = download_url match { case Archive_Name(name) => name case _ => error("Failed to determine source archive name from " + quote(download_url)) } val version = archive_name match { case Version(version) => version case _ => error("Failed to determine component version from " + quote(archive_name)) } val component = proper_string(component_name) getOrElse make_component_name(version) val component_dir = Components.Directory.create(target_dir + Path.basic(component), progress = progress) /* platform */ 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 + Path.basic(platform_name)) /* download source */ val archive_path = tmp_dir + Path.basic(archive_name) Isabelle_System.download_file(download_url, archive_path, progress = progress) Isabelle_System.extract(archive_path, tmp_dir) val source_dir = File.get_dir(tmp_dir, title = download_url) - Isabelle_System.extract(archive_path, component_dir.path) - Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src) + Isabelle_System.extract(archive_path, component_dir.src, strip = true) /* build */ progress.echo("Building Vampire for " + platform_name + " ...") Isabelle_System.copy_file(source_dir + Path.explode("LICENCE"), component_dir.path) val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else "" val cmake_out = progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" .""", cwd = source_dir.file, echo = verbose).check.out val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r val binary = split_lines(cmake_out).collectFirst({ case Pattern(name) => name }) .getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out)) progress.bash("make -j" + jobs, cwd = source_dir.file, echo = verbose).check Isabelle_System.copy_file(source_dir + Path.basic("bin") + Path.basic(binary).platform_exe, platform_dir + Path.basic("vampire").platform_exe) /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: VAMPIRE_HOME="$COMPONENT/$ISABELLE_PLATFORM64" ISABELLE_VAMPIRE="$VAMPIRE_HOME/vampire" """) /* README */ File.write(component_dir.README, "This Isabelle component provides Vampire " + version + """using the original sources from """.stripMargin + download_url + """ The executables have been built via "cmake . && make" Makarius """ + Date.Format.date(Date.now()) + "\n") } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_vampire", "build prover component from official download", Scala_Project.here, { args => var target_dir = Path.current var download_url = default_download_url var jobs = default_jobs var component_name = "" var verbose = false val getopts = Getopts(""" Usage: isabelle build_vampire [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_download_url + """") -j NUMBER parallel jobs for make (default: """ + default_jobs + """) -n NAME component name (default: """" + make_component_name("VERSION") + """") -v verbose Build prover component from official download. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => download_url = arg), "j:" -> (arg => jobs = Value.Nat.parse(arg)), "n:" -> (arg => component_name = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_vampire(download_url = download_url, component_name = component_name, jobs = jobs, verbose = verbose, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/build_verit.scala b/src/Pure/Admin/build_verit.scala --- a/src/Pure/Admin/build_verit.scala +++ b/src/Pure/Admin/build_verit.scala @@ -1,155 +1,154 @@ /* Title: Pure/Admin/build_csdp.scala Author: Makarius Build Isabelle veriT component from official download. */ package isabelle object Build_VeriT { val default_download_url = "https://verit.loria.fr/rmx/2021.06.2/verit-2021.06.2-rmx.tar.gz" /* build veriT */ def build_verit( download_url: String = default_download_url, verbose: Boolean = false, progress: Progress = new Progress, target_dir: Path = Path.current, mingw: MinGW = MinGW.none ): Unit = { mingw.check Isabelle_System.with_tmp_dir("build") { tmp_dir => /* component */ val Archive_Name = """^.*?([^/]+)$""".r val Version = """^[^-]+-(.+)\.tar.gz$""".r val archive_name = download_url match { case Archive_Name(name) => name case _ => error("Failed to determine source archive name from " + quote(download_url)) } val version = archive_name match { case Version(version) => version case _ => error("Failed to determine component version from " + quote(archive_name)) } val component_name = "verit-" + version val component_dir = Components.Directory.create(target_dir + Path.basic(component_name), progress = progress) /* platform */ val platform_name = proper_string(Isabelle_System.getenv("ISABELLE_WINDOWS_PLATFORM64")) orElse proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse error("No 64bit platform") val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name)) /* download source */ val archive_path = tmp_dir + Path.basic(archive_name) Isabelle_System.download_file(download_url, archive_path, progress = progress) Isabelle_System.extract(archive_path, tmp_dir) val source_dir = File.get_dir(tmp_dir, title = download_url) - Isabelle_System.extract(archive_path, component_dir.path) - Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src) + Isabelle_System.extract(archive_path, component_dir.src, strip = true) /* build */ progress.echo("Building veriT for " + platform_name + " ...") val configure_options = if (Platform.is_linux) "LDFLAGS=-Wl,-rpath,_DUMMY_" else "" progress.bash(mingw.bash_script("set -e\n./configure " + configure_options + "\nmake"), cwd = source_dir.file, echo = verbose).check /* install */ Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path) val exe_path = Path.basic("veriT").platform_exe Isabelle_System.copy_file(source_dir + exe_path, platform_dir) Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp"), mingw = mingw) /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: ISABELLE_VERIT="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/veriT" """) /* README */ File.write(component_dir.README, """This is veriT """ + version + """ from """ + download_url + """ It has been built from sources like this: cd src ./configure make Makarius """ + Date.Format.date(Date.now()) + "\n") } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_verit", "build prover component from official download", Scala_Project.here, { args => var target_dir = Path.current var mingw = MinGW.none var download_url = default_download_url var verbose = false val getopts = Getopts(""" Usage: isabelle build_verit [OPTIONS] Options are: -D DIR target directory (default ".") -M DIR msys/mingw root specification for Windows -U URL download URL (default: """" + default_download_url + """") -v verbose Build prover component from official download. """, "D:" -> (arg => target_dir = Path.explode(arg)), "M:" -> (arg => mingw = MinGW(Path.explode(arg))), "U:" -> (arg => download_url = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_verit(download_url = download_url, verbose = verbose, progress = progress, target_dir = target_dir, mingw = mingw) }) } 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,528 +1,529 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Miscellaneous Isabelle system operations. */ package isabelle import java.util.{Map => JMap, HashMap} import java.io.{File => JFile, IOException} import java.net.ServerSocket import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult, StandardCopyOption, FileSystemException} import java.nio.file.attribute.BasicFileAttributes object Isabelle_System { /* settings environment */ def settings(putenv: List[(String, String)] = Nil): JMap[String, String] = { val env0 = isabelle.setup.Environment.settings() if (putenv.isEmpty) env0 else { val env = new HashMap(env0) for ((a, b) <- putenv) env.put(a, b) env } } 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)) /* services */ type Service = Classpath.Service @volatile private var _classpath: Option[Classpath] = None def classpath(): Classpath = { if (_classpath.isEmpty) init() // unsynchronized check _classpath.get } def make_services[C](c: Class[C]): List[C] = classpath().make_services(c) /* init settings + classpath */ def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = { isabelle.setup.Environment.init(isabelle_root, cygwin_root) synchronized { if (_classpath.isEmpty) _classpath = Some(Classpath()) } } /* 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) orElse Mercurial.id_repository(root, rev = "") getOrElse error("Failed to identify Isabelle distribution " + root.expand) 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 export_isabelle_identifier(isabelle_identifier: String): String = "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" 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" + (try { "/" + isabelle_id () } catch { case ERROR(_) => "" }) + isabelle_heading() /** file-system operations **/ /* scala functions */ private def apply_paths( args: List[String], fun: PartialFunction[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.java_path) } 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) } } def with_copy_dir[A](dir1: Path, dir2: Path)(body: => A): A = { if (dir2.is_file || dir2.is_dir) error("Directory already exists: " + dir2.absolute) else { try { copy_dir(dir1, dir2); body } finally { rm_tree(dir2 ) } } } 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, native: 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 = { if (native) { error("Failed to create native symlink on Windows: " + quote(src_file.toString) + "\n(but it could work as Administrator)") } else isabelle.setup.Environment.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(), initialized: Boolean = true ): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile if (initialized) file.deleteOnExit() else file.delete() file } def with_tmp_file[A]( name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix() )(body: Path => A): A = { val file = tmp_file(name, ext, base_dir = base_dir) 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, base_dir: JFile = isabelle_tmp_prefix() )(body: Path => A): A = { val dir = tmp_dir(name, base_dir = base_dir) 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) } /* TCP/IP ports */ def local_port(): Int = { val socket = new ServerSocket(0) val port = socket.getLocalPort socket.close() port } /* JVM shutdown hook */ def create_shutdown_hook(body: => Unit): Thread = { val shutdown_hook = Isabelle_Thread.create(new Runnable { def run: Unit = body }) try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } shutdown_hook } def remove_shutdown_hook(shutdown_hook: Thread): Unit = try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } /** external processes **/ /* GNU bash */ def bash(script: String, description: String = "", cwd: JFile = null, env: JMap[String, String] = settings(), redirect: Boolean = false, input: String = "", 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, description = description, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(input = input, progress_stdout = progress_stdout, progress_stderr = progress_stderr, watchdog = watchdog, strict = strict) } /* command-line tools */ def require_command(cmd: String, test: String = "--version"): Unit = { if (!bash(Bash.string(cmd) + " " + test).ok) error("Missing system command: " + quote(cmd)) } 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: Boolean = false, redirect: Boolean = false ): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") + (if (!strip) "" else "--strip-components=1 ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } def extract(archive: Path, dir: Path, strip: Boolean = false): Unit = { val name = archive.file_name + make_directory(dir) if (File.is_zip(name)) { require(!strip, "Cannot use unzip with strip") Isabelle_System.bash("unzip -x " + File.bash_path(archive.absolute), cwd = dir.file).check } else if (File.is_tar_bz2(name) || File.is_tgz(name) || File.is_tar_gz(name)) { val flags = if (File.is_tar_bz2(name)) "-xjf " else "-xzf " Isabelle_System.gnutar(flags + File.bash_path(archive), dir = dir, strip = strip).check } else error("Cannot extract " + archive) } def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = { with_tmp_file("patch") { patch => Isabelle_System.bash( "diff -ru " + diff_options + " -- " + File.bash_path(src) + " " + File.bash_path(dst) + " > " + File.bash_path(patch), cwd = base_dir.file).check_rc(_ <= 1) File.read(patch) } } 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 } /** 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.map(url => 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"))) }