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,213 +1,213 @@ /* 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 => " " + p._1 + "=" + p._2) .mkString("\n")) def change(path: Path) { def change_line(line: String, entry: (String, String)): String = line.replaceAll(entry._1 + "=.*", entry._1 + "=" + entry._2) File.change(path, s => split_lines(s).map(line => (line /: changed)(change_line)).mkString("\n")) } } 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) { 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 = Isabelle_System.new_directory(target_dir + Path.basic(component_name)) progress.echo("Component " + component_dir) /* 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.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 " + File.bash_path(archive_path), cwd = tmp_dir.file).check val source_name = File.get_dir(tmp_dir) Isabelle_System.bash( "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src", cwd = component_dir.file).check /* build */ progress.echo("Building CSDP for " + platform_name + " ...") val build_dir = tmp_dir + Path.basic(source_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(build_dir.file, pred = file => file.getName == "Makefile"). foreach(file => flags.change(File.path(file))) } progress.bash(mingw.bash_script("make"), cwd = build_dir.file, echo = verbose).check /* install */ File.copy(build_dir + Path.explode("LICENSE"), component_dir) if (!Platform.is_windows) { File.copy(build_dir + Path.explode("solver/csdp"), platform_dir) } else { File.copy(build_dir + Path.explode("solver/csdp.exe"), platform_dir) val libs = List("libblas", "liblapack", "libgfortran-5", "libgcc_s_seh-1", "libquadmath-0", "libwinpthread-1") for (name <- libs) { File.copy(mingw.get_root + Path.explode("mingw64/bin") + Path.basic(name).ext("dll"), 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: ISABELLE_CSDP="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/csdp" """) /* README */ File.write(component_dir + Path.basic("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") + Makarius + """ + Date.Format.date(Date.now()) + "\n") }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_csdp", "build prover component from official download", 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,144 +1,144 @@ /* Title: Pure/Admin/build_e.scala Author: Makarius Build Isabelle E prover component from official downloads. */ package isabelle object Build_E { /* build E prover */ val default_version = "2.5" val default_download_url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD" 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) { Isabelle_System.with_tmp_dir("build")(tmp_dir => { /* component */ val component_name = "e-" + version val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name)) progress.echo("Component " + component_dir) val platform_name = proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) .getOrElse(error("No 64bit platform")) val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name)) /* download source */ val archive_url = download_url + "/V_" + version + "/E.tgz" val archive_path = tmp_dir + Path.explode("E.tgz") Isabelle_System.download(archive_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 E src", cwd = component_dir.file).check /* build */ progress.echo("Building E prover for " + platform_name + " ...") val build_dir = tmp_dir + Path.basic("E") val build_options = { val result = Isabelle_System.bash("./configure --help", cwd = build_dir.file) if (result.check.out.containsSlice("--enable-ho")) " --enable-ho" else "" } val build_script = "./configure" + build_options + " && make" Isabelle_System.bash(build_script, cwd = build_dir.file, progress_stdout = progress.echo_if(verbose, _), progress_stderr = progress.echo_if(verbose, _)).check /* install */ File.copy(build_dir + Path.basic("COPYING"), component_dir + Path.basic("LICENSE")) val install_files = List("epclextract", "eprover", "eprover-ho") for (name <- install_files ::: install_files.map(_ + ".exe")) { val path = build_dir + Path.basic("PROVER") + Path.basic(name) if (path.is_file) File.copy(path, platform_dir) } Isabelle_System.bash("if [ -f eprover-ho ]; then mv eprover-ho eprover; fi", cwd = platform_dir.file).check /* settings */ val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) File.write(etc_dir + Path.basic("settings"), """# -*- shell-script -*- :mode=shellscript: E_HOME="$COMPONENT/$ISABELLE_PLATFORM64" E_VERSION=""" + quote(version) + """ """) /* README */ File.write(component_dir + Path.basic("README"), "This is E prover " + version + " from\n" + 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") + Makarius + """ + Date.Format.date(Date.now()) + "\n") }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_e", "build prover component from source distribution", 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_spass.scala b/src/Pure/Admin/build_spass.scala --- a/src/Pure/Admin/build_spass.scala +++ b/src/Pure/Admin/build_spass.scala @@ -1,182 +1,182 @@ /* 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 for " + platform_name + " ...") val build_dir = tmp_dir + Path.basic(archive_base_name) if (Platform.is_windows) { File.change(build_dir + Path.basic("misc.c"), _.replace("""#include "execinfo.h" """, "") .replaceAll("""void misc_DumpCore\(void\)[^}]+}""", "void misc_DumpCore(void) { abort(); }")) } 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 + Jasmin Blanchette + 16-May-2018 - Makarius - """ + Date.Format.date(Date.now()) + "\n") + 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 --git a/src/Pure/Admin/build_sqlite.scala b/src/Pure/Admin/build_sqlite.scala --- a/src/Pure/Admin/build_sqlite.scala +++ b/src/Pure/Admin/build_sqlite.scala @@ -1,113 +1,113 @@ /* Title: Pure/Admin/build_sqlite.scala Author: Makarius Build Isabelle sqlite-jdbc component from official download. */ package isabelle object Build_SQLite { /* build sqlite */ def build_sqlite( download_url: String, progress: Progress = new Progress, target_dir: Path = Path.current) { val Download_Name = """^.*/([^/]+)\.jar""".r val download_name = download_url match { case Download_Name(download_name) => download_name case _ => error("Malformed jar download URL: " + quote(download_url)) } /* component */ val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(download_name)) progress.echo("Component " + component_dir) /* README */ File.write(component_dir + Path.basic("README"), "This is " + download_name + " from\n" + download_url + - "\n\n Makarius\n " + Date.Format.date(Date.now()) + "\n") + "\n\n Makarius\n " + Date.Format.date(Date.now()) + "\n") /* settings */ val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) File.write(etc_dir + Path.basic("settings"), """# -*- shell-script -*- :mode=shellscript: ISABELLE_SQLITE_HOME="$COMPONENT" classpath "$ISABELLE_SQLITE_HOME/""" + download_name + """.jar" """) /* jar */ val jar = component_dir + Path.basic(download_name).ext("jar") Isabelle_System.download(download_url, jar, progress = progress) Isabelle_System.with_tmp_dir("sqlite")(jar_dir => { progress.echo("Unpacking " + jar) Isabelle_System.bash("isabelle_jdk jar xf " + File.bash_path(jar.absolute), cwd = jar_dir.file).check val jar_files = List( "META-INF/maven/org.xerial/sqlite-jdbc/LICENSE" -> ".", "META-INF/maven/org.xerial/sqlite-jdbc/LICENSE.zentus" -> ".", "org/sqlite/native/Linux/aarch64/libsqlitejdbc.so" -> "arm64-linux", "org/sqlite/native/Linux/x86_64/libsqlitejdbc.so" -> "x86_64-linux", "org/sqlite/native/Mac/x86_64/libsqlitejdbc.jnilib" -> "x86_64-darwin", "org/sqlite/native/Windows/x86_64/sqlitejdbc.dll" -> "x86_64-windows") for ((file, dir) <- jar_files) { val target = Isabelle_System.make_directory(component_dir + Path.explode(dir)) File.copy(jar_dir + Path.explode(file), target) } File.set_executable(component_dir + Path.explode("x86_64-windows/sqlitejdbc.dll"), true) }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_sqlite", "build Isabelle sqlite-jdbc component from official download", args => { var target_dir = Path.current val getopts = Getopts(""" Usage: isabelle build_sqlite [OPTIONS] DOWNLOAD Options are: -D DIR target directory (default ".") Build sqlite-jdbc component from the specified download URL (JAR), see also https://github.com/xerial/sqlite-jdbc/releases """, "D:" -> (arg => target_dir = Path.explode(arg))) val more_args = getopts(args) val download_url = more_args match { case List(download_url) => download_url case _ => getopts.usage() } val progress = new Console_Progress() build_sqlite(download_url, progress = progress, target_dir = target_dir) }) }