# HG changeset patch # User wenzelm # Date 1602241976 -7200 # Node ID b8cc129ece05d6a11bf31f17ab1b5c991a11bbf6 # Parent f98f764239a4bda6a7b9cb16cfe2659b7a28d57b build Isabelle SPASS component from unofficial download; diff -r f98f764239a4 -r b8cc129ece05 src/Pure/Admin/build_spass.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Admin/build_spass.scala Fri Oct 09 13:12:56 2020 +0200 @@ -0,0 +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) + { + Isabelle_System.with_tmp_dir("build")(tmp_dir => + { + /* required commands */ + + List("bison", "flex").foreach(cmd => + if (!Isabelle_System.bash(cmd + " --version").ok) error("Missing command: " + cmd)) + + + /* component */ + + val Archive_Name = """^.*?([^/]+)$""".r + val Component_Name = """^(.+)-src\.tar.gz$""".r + val Version = """^[^-]+-([^-]+)$""".r + + val (archive_name, archive_base_name) = + download_url match { + case Archive_Name(name) => (name, Library.perhaps_unsuffix(".tar.gz", 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 = 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)) + + + /* download source */ + + val archive_path = tmp_dir + Path.basic(archive_name) + Isabelle_System.download(download_url, archive_path, progress = progress) + + Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check + Isabelle_System.bash( + "tar xzf " + archive_path + " && mv " + Bash.string(archive_base_name) + " src", + cwd = component_dir.file).check + + + /* build */ + + progress.echo("Building SPASS ...") + + val build_dir = tmp_dir + Path.basic(archive_base_name) + Isabelle_System.bash("make", + cwd = build_dir.file, + progress_stdout = progress.echo_if(verbose, _), + progress_stderr = progress.echo_if(verbose, _)).check + + + /* install */ + + File.copy(build_dir + Path.basic("LICENCE"), component_dir + Path.basic("LICENSE")) + + val install_files = List("SPASS") + for (name <- install_files ::: install_files.map(_ + ".exe")) { + val path = build_dir + Path.basic(name) + if (path.is_file) File.copy(path, platform_dir) + } + + + /* settings */ + + val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) + File.write(etc_dir + Path.basic("settings"), + """# -*- shell-script -*- :mode=shellscript: + +SPASS_HOME="$COMPONENT/$ISABELLE_PLATFORM64" +SPASS_VERSION=""" + quote(version) + """ +""") + + /* README */ + + File.write(component_dir + Path.basic("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", + 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 -r f98f764239a4 -r b8cc129ece05 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Fri Oct 09 12:28:04 2020 +0200 +++ b/src/Pure/System/isabelle_tool.scala Fri Oct 09 13:12:56 2020 +0200 @@ -177,6 +177,7 @@ Build_JDK.isabelle_tool, Build_PolyML.isabelle_tool1, Build_PolyML.isabelle_tool2, + Build_SPASS.isabelle_tool, Build_SQLite.isabelle_tool, Build_Status.isabelle_tool, Check_Sources.isabelle_tool, diff -r f98f764239a4 -r b8cc129ece05 src/Pure/build-jars --- a/src/Pure/build-jars Fri Oct 09 12:28:04 2020 +0200 +++ b/src/Pure/build-jars Fri Oct 09 13:12:56 2020 +0200 @@ -20,6 +20,7 @@ src/Pure/Admin/build_log.scala src/Pure/Admin/build_polyml.scala src/Pure/Admin/build_release.scala + src/Pure/Admin/build_spass.scala src/Pure/Admin/build_sqlite.scala src/Pure/Admin/build_status.scala src/Pure/Admin/check_sources.scala