diff --git a/src/Pure/Admin/component_bash_process.scala b/src/Pure/Admin/component_bash_process.scala --- a/src/Pure/Admin/component_bash_process.scala +++ b/src/Pure/Admin/component_bash_process.scala @@ -1,222 +1,218 @@ /* Title: Pure/Admin/component_bash_process.scala Author: Makarius Build bash_process component from C source. */ package isabelle object Component_Bash_Process { /* build bash_process */ def build_bash_process( progress: Progress = new Progress, target_dir: Path = Path.current, ): Unit = { Isabelle_System.require_command("cc") /* component */ val component_date = Date.Format.alt_date(Date.now()) val component_name = "bash_process-" + component_date val component_dir = Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress) component_dir.write_platforms() /* platform */ - val platform_name = - proper_string(Isabelle_System.getenv("ISABELLE_APPLE_PLATFORM64")) orElse - proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse - error("Missing ISABELLE_PLATFORM64") - + val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(apple = true) val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name)) /* source */ val source_file = Path.explode("bash_process.c") File.write(component_dir.path + source_file, """/* Author: Makarius License: Isabelle BSD-3 Bash process with separate process group id. */ #include #include #include #include #include #include #include #include #include #include static void fail(const char *msg) { fprintf(stderr, "%s\n", msg); fflush(stderr); exit(2); } static time_t now() { struct timeval tv; if (gettimeofday(&tv, NULL) == 0) { return tv.tv_sec * 1000 + tv.tv_usec / 1000; } else { return time(NULL) * 1000; } } int main(int argc, char *argv[]) { /* args */ if (argc < 2) { fprintf(stderr, "Bad arguments: missing TIMING_FILE\n"); fflush(stderr); exit(1); } char *timing_name = argv[1]; /* potential fork */ time_t time_start = now(); if (strlen(timing_name) > 0 || setsid() == -1) { pid_t pid = fork(); if (pid == -1) fail("Cannot set session id (failed to fork)"); else if (pid != 0) { int status; // ingore SIGINT struct sigaction sa; memset(&sa, 0, sizeof(sa)); sa.sa_handler = SIG_IGN; sigaction(SIGINT, &sa, 0); if (waitpid(pid, &status, 0) == -1) { fail("Cannot join forked process"); } /* report timing */ if (strlen(timing_name) > 0) { long long timing_elapsed = now() - time_start; struct rusage ru; getrusage(RUSAGE_CHILDREN, &ru); long long timing_cpu = ru.ru_utime.tv_sec * 1000 + ru.ru_utime.tv_usec / 1000 + ru.ru_stime.tv_sec * 1000 + ru.ru_stime.tv_usec / 1000; FILE *timing_file = fopen(timing_name, "w"); if (timing_file == NULL) fail("Cannot open timing file"); fprintf(timing_file, "%lld %lld", timing_elapsed, timing_cpu); fclose(timing_file); } if (WIFEXITED(status)) { exit(WEXITSTATUS(status)); } else if (WIFSIGNALED(status)) { exit(128 + WTERMSIG(status)); } else { fail("Unknown status of forked process"); } } else if (setsid() == -1) fail("Cannot set session id (after fork)"); } /* report pid */ fprintf(stdout, "%d\n", getpid()); fflush(stdout); /* shift command line */ int i; for (i = 2; i < argc; i++) { argv[i - 2] = argv[i]; } argv[argc - 2] = NULL; argv[argc - 1] = NULL; /* exec */ execvp("bash", argv); fail("Cannot exec process"); } """) /* build */ progress.echo("Building bash_process for " + platform_name + " ...") progress.bash("cc ../bash_process.c -o bash_process", cwd = platform_dir.file).check /* settings */ component_dir.write_settings(""" ISABELLE_BASH_PROCESS_HOME="$COMPONENT" ISABELLE_BASH_PROCESS="$ISABELLE_BASH_PROCESS_HOME/${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}/bash_process" """) /* README */ File.write(component_dir.README, """The bash_process executable has been built like this: cc -Wall bash_process.c -o bash_process Makarius """ + Date.Format.date(Date.now()) + "\n") } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("component_bash_process", "build bash_process component from C source", Scala_Project.here, { args => var target_dir = Path.current val getopts = Getopts(""" Usage: isabelle component_bash_process [OPTIONS] Options are: -D DIR target directory (default ".") Build prover component from official download. """, "D:" -> (arg => target_dir = Path.explode(arg))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_bash_process(progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/component_csdp.scala b/src/Pure/Admin/component_csdp.scala --- a/src/Pure/Admin/component_csdp.scala +++ b/src/Pure/Admin/component_csdp.scala @@ -1,197 +1,193 @@ /* Title: Pure/Admin/component_csdp.scala Author: Makarius Build Isabelle CSDP component from official download. */ package isabelle object Component_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, 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(target_dir + Path.basic(component_name)).create(progress = progress) /* platform */ - val platform_name = - proper_string(Isabelle_System.getenv("ISABELLE_WINDOWS_PLATFORM64")) orElse - proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse - error("Missing ISABELLE_PLATFORM64") - + val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true) 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.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 = progress.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 */ component_dir.write_settings(""" 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("component_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 component_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(verbose = verbose) build_csdp(download_url = download_url, progress = progress, target_dir = target_dir, mingw = mingw) }) } diff --git a/src/Pure/Admin/component_e.scala b/src/Pure/Admin/component_e.scala --- a/src/Pure/Admin/component_e.scala +++ b/src/Pure/Admin/component_e.scala @@ -1,139 +1,136 @@ /* Title: Pure/Admin/component_e.scala Author: Makarius Build Isabelle E prover component from official downloads. */ package isabelle object Component_E { /* build E prover */ val default_version = "3.0.03" 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, 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(target_dir + Path.basic(component_name)).create(progress = progress) - val platform_name = - proper_string(Isabelle_System.getenv("ISABELLE_APPLE_PLATFORM64")) orElse - proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse error("Bad platform") - + val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(apple = true) 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.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(_, verbose = true), progress_stderr = progress.echo(_, verbose = true)).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 */ component_dir.write_settings(""" E_HOME="$COMPONENT/${ISABELLE_APPLE_PLATFORM64:-$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("component_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 component_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(verbose = verbose) build_e(version = version, download_url = download_url, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/component_minisat.scala b/src/Pure/Admin/component_minisat.scala --- a/src/Pure/Admin/component_minisat.scala +++ b/src/Pure/Admin/component_minisat.scala @@ -1,149 +1,146 @@ /* Title: Pure/Admin/component_minisat.scala Author: Makarius Build Isabelle Minisat from sources. */ package isabelle object Component_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 = "", 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(target_dir + Path.basic(component)).create(progress = progress) /* platform */ - val platform_name = - proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse - error("Missing ISABELLE_PLATFORM64") - + val platform_name = Isabelle_Platform.self.ISABELLE_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.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 = progress.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 */ component_dir.write_settings(""" 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 """ + 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("component_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 component_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(verbose = verbose) build_minisat(download_url = download_url, component_name = component_name, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/component_rsync.scala b/src/Pure/Admin/component_rsync.scala --- a/src/Pure/Admin/component_rsync.scala +++ b/src/Pure/Admin/component_rsync.scala @@ -1,158 +1,155 @@ /* Title: Pure/Admin/component_rsync.scala Author: Makarius Build Isabelle rsync component from official source distribution. */ package isabelle object Component_Rsync { /* resources */ def home: Path = Path.explode("$ISABELLE_RSYNC_HOME") def local_program: Path = Path.explode("$ISABELLE_RSYNC") def remote_program(directory: Components.Directory): Path = { val platform = "platform_" + directory.ssh.isabelle_platform.ISABELLE_PLATFORM64 directory.path + Path.basic(platform) + Path.basic("rsync") } /* build rsync */ val default_version = "3.2.7" val default_download_url = "https://github.com/WayneD/rsync/archive/refs/tags" val default_build_options: List[String] = List( "--disable-acl-support", "--disable-lz4", "--disable-md2man", "--disable-openssl", "--disable-xattr-support", "--disable-xxhash", "--disable-zstd") def build_rsync( version: String = default_version, download_url: String = default_download_url, progress: Progress = new Progress, target_dir: Path = Path.current, build_options: List[String] = default_build_options ): Unit = { Isabelle_System.with_tmp_dir("build") { tmp_dir => /* component */ val component_name = "rsync-" + version val component_dir = Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress) - val platform_name = - proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) - .getOrElse(error("Missing ISABELLE_PLATFORM64")) - + val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM() val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic("platform_" + platform_name)) /* download source */ val archive_name = "v" + version + ".tar.gz" val archive_path = tmp_dir + Path.explode(archive_name) val archive_url = Url.append_path(download_url, archive_name) 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.src, strip = true) /* build */ progress.echo("Building rsync for " + platform_name + " ...") val build_script = List("./configure " + Bash.strings(build_options.sorted), "make") Isabelle_System.bash(build_script.mkString(" && "), cwd = source_dir.file, progress_stdout = progress.echo(_, verbose = true), progress_stderr = progress.echo(_, verbose = true)).check /* install */ Isabelle_System.copy_file(source_dir + Path.explode("COPYING"), component_dir.LICENSE) Isabelle_System.copy_file(source_dir + Path.explode("rsync").platform_exe, platform_dir) /* settings */ component_dir.write_settings(""" ISABELLE_RSYNC_HOME="$COMPONENT" ISABELLE_RSYNC="$ISABELLE_RSYNC_HOME/platform_${ISABELLE_PLATFORM64}/rsync" """) /* README */ File.write(component_dir.README, "This is rsync " + version + " from " + download_url + """ The distribution has been built like this: """ + ("cd src" :: build_script).map(s => " " + s + "\n").mkString + """ See also: * https://github.com/WayneD/rsync * https://rsync.samba.org Makarius """ + Date.Format.date(Date.now()) + "\n") } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("component_rsync", "build rsync component from source distribution", Scala_Project.here, { args => var target_dir = Path.current var build_options = default_build_options var version = default_version var download_url = default_download_url var verbose = false val getopts = Getopts(""" Usage: isabelle component_rsync [OPTIONS] Options are: -D DIR target directory (default ".") -O OPT add build option -R OPT remove build option -U URL download URL (default: """" + default_download_url + """") -V VERSION version (default: """ + default_version + """) -v verbose Build rsync component from the specified source distribution. The default build options (for ./configure) are: """ + default_build_options.map(opt => " " + opt + "\n").mkString, "D:" -> (arg => target_dir = Path.explode(arg)), "O:" -> (arg => build_options = Library.insert(arg)(build_options)), "R:" -> (arg => build_options = Library.remove(arg)(build_options)), "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(verbose = verbose) build_rsync(version = version, download_url = download_url, progress = progress, target_dir = target_dir, build_options = build_options) }) } diff --git a/src/Pure/Admin/component_spass.scala b/src/Pure/Admin/component_spass.scala --- a/src/Pure/Admin/component_spass.scala +++ b/src/Pure/Admin/component_spass.scala @@ -1,174 +1,171 @@ /* Title: Pure/Admin/component_spass.scala Author: Makarius Build Isabelle SPASS component from unofficial download. */ package isabelle object Component_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, 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(target_dir + Path.basic(component_name)).create(progress = progress) - val platform_name = - proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) - .getOrElse(error("Missing ISABELLE_PLATFORM64")) - + val platform_name = Isabelle_Platform.self.ISABELLE_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.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(_, verbose = true), progress_stderr = progress.echo(_, verbose = true)).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 */ component_dir.write_settings(""" 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("component_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 component_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(verbose = verbose) build_spass(download_url = download_url, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/component_vampire.scala b/src/Pure/Admin/component_vampire.scala --- a/src/Pure/Admin/component_vampire.scala +++ b/src/Pure/Admin/component_vampire.scala @@ -1,162 +1,159 @@ /* Title: Pure/Admin/component_vampire.scala Author: Makarius Build Isabelle Vampire component from official download. */ package isabelle object Component_Vampire { val default_download_url = "https://github.com/vprover/vampire/archive/refs/tags/v4.8HO4Sledgahammer.tar.gz" val default_version = "4.8" 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 = "", component_version: String = default_version, 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 archive_name = download_url match { case Archive_Name(name) => name case _ => error("Failed to determine source archive name from " + quote(download_url)) } if (component_version.isEmpty) error("Missing component version") val component = proper_string(component_name) getOrElse make_component_name(component_version) val component_dir = Components.Directory(target_dir + Path.basic(component)).create(progress = progress) /* platform */ - val platform_name = - proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse - error("Missing ISABELLE_PLATFORM64") - + val platform_name = Isabelle_Platform.self.ISABELLE_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.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 = "-DCMAKE_BUILD_TYPE=Release -DCMAKE_BUILD_HOL=On -DCMAKE_DISABLE_FIND_PACKAGE_Z3=ON " + (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 = progress.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 = progress.verbose).check Isabelle_System.copy_file(source_dir + Path.basic("bin") + Path.basic(binary).platform_exe, platform_dir + Path.basic("vampire").platform_exe) /* settings */ component_dir.write_settings(""" VAMPIRE_HOME="$COMPONENT/$ISABELLE_PLATFORM64" VAMPIRE_VERSION=""" + quote(component_version) + """ ISABELLE_VAMPIRE="$VAMPIRE_HOME/vampire" """) /* README */ File.write(component_dir.README, "This Isabelle component provides Vampire " + component_version + """ using the original sources from """ + 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("component_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 component_version = default_version var verbose = false val getopts = Getopts(""" Usage: isabelle component_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 VERSION component version (default: """ + default_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:" -> (arg => component_version = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress(verbose = verbose) build_vampire(download_url = download_url, component_name = component_name, component_version = component_version, jobs = jobs, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/component_verit.scala b/src/Pure/Admin/component_verit.scala --- a/src/Pure/Admin/component_verit.scala +++ b/src/Pure/Admin/component_verit.scala @@ -1,151 +1,147 @@ /* Title: Pure/Admin/component_verit.scala Author: Makarius Build Isabelle veriT component from official download. */ package isabelle object Component_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, 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(target_dir + Path.basic(component_name)).create(progress = progress) /* platform */ - val platform_name = - proper_string(Isabelle_System.getenv("ISABELLE_WINDOWS_PLATFORM64")) orElse - proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse - error("Missing ISABELLE_PLATFORM64") - + val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true) 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.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 = progress.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 */ component_dir.write_settings(""" 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("component_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 component_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(verbose = verbose) build_verit(download_url = download_url, progress = progress, target_dir = target_dir, mingw = mingw) }) } diff --git a/src/Pure/Admin/component_zipperposition.scala b/src/Pure/Admin/component_zipperposition.scala --- a/src/Pure/Admin/component_zipperposition.scala +++ b/src/Pure/Admin/component_zipperposition.scala @@ -1,117 +1,114 @@ /* Title: Pure/Admin/component_zipperposition.scala Author: Makarius Build Isabelle Zipperposition component from OPAM repository. */ package isabelle object Component_Zipperposition { val default_version = "2.1" /* build Zipperposition */ def build_zipperposition( version: String = default_version, progress: Progress = new Progress, target_dir: Path = Path.current ): Unit = { Isabelle_System.with_tmp_dir("build") { build_dir => if (Platform.is_linux) Isabelle_System.require_command("patchelf") /* component */ val component_name = "zipperposition-" + version val component_dir = Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress) /* platform */ - val platform_name = - proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse - error("Missing ISABELLE_PLATFORM64") - + val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM() val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name)) /* build */ progress.echo("OCaml/OPAM setup ...") progress.bash("isabelle ocaml_setup", echo = progress.verbose).check progress.echo("Building Zipperposition for " + platform_name + " ...") progress.bash(cwd = build_dir.file, echo = progress.verbose, script = "isabelle_opam install -y --destdir=" + File.bash_path(build_dir) + " zipperposition=" + Bash.string(version)).check /* install */ Isabelle_System.copy_file(build_dir + Path.explode("doc/zipperposition/LICENSE"), component_dir.path) val prg_path = Path.basic("zipperposition") val exe_path = prg_path.platform_exe Isabelle_System.copy_file(build_dir + Path.basic("bin") + prg_path, platform_dir + exe_path) if (!Platform.is_windows) { Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp")) } /* settings */ component_dir.write_settings(""" ZIPPERPOSITION_HOME="$COMPONENT/$ISABELLE_PLATFORM64" """) /* README */ File.write(component_dir.README, """This is Zipperposition """ + version + """ from the OCaml/OPAM repository. Makarius """ + Date.Format.date(Date.now()) + "\n") } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("component_zipperposition", "build prover component from OPAM repository", Scala_Project.here, { args => var target_dir = Path.current var version = default_version var verbose = false val getopts = Getopts(""" Usage: isabelle component_zipperposition [OPTIONS] Options are: -D DIR target directory (default ".") -V VERSION version (default: """" + default_version + """") -v verbose Build prover component from OPAM repository. """, "D:" -> (arg => target_dir = Path.explode(arg)), "V:" -> (arg => version = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress(verbose = verbose) build_zipperposition(version = version, progress = progress, target_dir = target_dir) }) }