--- a/NEWS Tue Oct 13 16:45:38 2020 +0200
+++ b/NEWS Tue Oct 13 20:28:43 2020 +0200
@@ -186,7 +186,7 @@
*** System ***
* Update/rebuild external provers on currently supported OS platforms,
-notably E Prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
+notably E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
* Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
variable.
--- a/lib/scripts/getfunctions Tue Oct 13 16:45:38 2020 +0200
+++ b/lib/scripts/getfunctions Tue Oct 13 20:28:43 2020 +0200
@@ -38,7 +38,7 @@
echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" >&2
return 127
else
- env OPAMROOT="$ISABELLE_OPAM_ROOT" "$ISABELLE_OPAM" "$@"
+ env OPAMROOT="$ISABELLE_OPAM_ROOT" OPAMCOLOR="never" "$ISABELLE_OPAM" "$@"
fi
}
export -f isabelle_opam
--- a/src/Pure/Admin/build_csdp.scala Tue Oct 13 16:45:38 2020 +0200
+++ b/src/Pure/Admin/build_csdp.scala Tue Oct 13 20:28:43 2020 +0200
@@ -125,19 +125,13 @@
/* install */
File.copy(build_dir + Path.explode("LICENSE"), component_dir)
+ File.copy(build_dir + Path.explode("solver/csdp").platform_exe, platform_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)
- }
+ 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"))
}
--- a/src/Pure/Admin/build_polyml.scala Tue Oct 13 16:45:38 2020 +0200
+++ b/src/Pure/Admin/build_polyml.scala Tue Oct 13 20:28:43 2020 +0200
@@ -17,14 +17,13 @@
sealed case class Platform_Info(
options: List[String] = Nil,
setup: String = "",
- copy_files: List[String] = Nil,
- ldd_pattern: Option[(String, Regex)] = None)
+ libs: Set[String] = Set.empty)
private val platform_info = Map(
"linux" ->
Platform_Info(
options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"),
- ldd_pattern = Some(("ldd", """\s*libgmp.*=>\s*(\S+).*""".r))),
+ libs = Set("libgmp")),
"darwin" ->
Platform_Info(
options =
@@ -32,17 +31,13 @@
"CXXFLAGS=-arch x86_64 -O3 -I../libffi/include", "CCASFLAGS=-arch x86_64",
"LDFLAGS=-segprot POLY rwx rwx"),
setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin",
- ldd_pattern = Some(("otool -L", """\s*(\S+lib(?:polyml|gmp).*dylib).*""".r))),
+ libs = Set("libpolyml", "libgmp")),
"windows" ->
Platform_Info(
options =
List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
setup = MinGW.environment_export,
- copy_files =
- List("$MSYS/mingw64/bin/libgcc_s_seh-1.dll",
- "$MSYS/mingw64/bin/libgmp-10.dll",
- "$MSYS/mingw64/bin/libstdc++-6.dll",
- "$MSYS/mingw64/bin/libwinpthread-1.dll")))
+ libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread")))
def build_polyml(
root: Path,
@@ -68,10 +63,6 @@
platform_info.getOrElse(platform.os_name,
error("Bad OS platform: " + quote(platform.os_name)))
- val settings =
- if (!Platform.is_windows) Isabelle_System.settings()
- else Isabelle_System.settings() + ("MSYS" -> mingw.get_root.expand.implode)
-
if (platform.is_linux) Isabelle_System.require_command("chrpath")
@@ -101,16 +92,6 @@
} || { echo "Build failed" >&2; exit 2; }
""", redirect = true, echo = true).check
- val ldd_files =
- {
- info.ldd_pattern match {
- case Some((ldd, pattern)) =>
- val lines = bash(root, ldd + " target/bin/poly").check.out_lines
- for { line <- lines; List(lib) <- pattern.unapplySeq(line) } yield lib
- case None => Nil
- }
- }
-
/* sha1 library */
@@ -120,45 +101,33 @@
bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check
val dir2 = dir1 + Path.explode(sha1_platform)
- File.read_dir(dir2).map(entry => dir2.implode + "/" + entry)
+ File.read_dir(dir2).map(entry => dir2 + Path.basic(entry))
}
else Nil
- /* target */
+ /* install */
- val target = Path.explode(polyml_platform)
- Isabelle_System.rm_tree(target)
- Isabelle_System.make_directory(target)
+ val platform_dir = Path.explode(polyml_platform)
+ Isabelle_System.rm_tree(platform_dir)
+ Isabelle_System.make_directory(platform_dir)
- for (file <- info.copy_files ::: ldd_files ::: sha1_files)
- File.copy(Path.explode(file).expand_env(settings), target)
+ for (file <- sha1_files) File.copy(file, platform_dir)
for {
d <- List("target/bin", "target/lib")
dir = root + Path.explode(d)
entry <- File.read_dir(dir)
- } File.move(dir + Path.explode(entry), target)
-
-
- /* poly: library path */
+ } File.move(dir + Path.explode(entry), platform_dir)
- if (platform.is_linux) {
- bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check
- }
- else if (platform.is_macos) {
- for (file <- ldd_files) {
- bash(target,
- """install_name_tool -change """ + Bash.string(file) + " " +
- Bash.string("@executable_path/" + Path.explode(file).file_name) + " poly").check
- }
- }
+ Executable.libraries_closure(
+ platform_dir + Path.basic("poly").platform_exe, mingw = mingw, filter = info.libs)
/* polyc: directory prefix */
val Header = "#! */bin/sh".r
- File.change(target + Path.explode("polyc"), txt =>
+ File.change(platform_dir + Path.explode("polyc"), txt =>
split_lines(txt) match {
case Header() :: lines =>
val lines1 =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_zipperposition.scala Tue Oct 13 20:28:43 2020 +0200
@@ -0,0 +1,118 @@
+/* Title: Pure/Admin/build_zipperposition.scala
+ Author: Makarius
+
+Build Isabelle Zipperposition component from OPAM repository.
+*/
+
+package isabelle
+
+
+object Build_Zipperposition
+{
+ val default_version = "1.6"
+
+
+ /* build Zipperposition */
+
+ def build_zipperposition(
+ version: String = default_version,
+ verbose: Boolean = false,
+ progress: Progress = new Progress,
+ target_dir: Path = Path.current)
+ {
+ Isabelle_System.with_tmp_dir("build")(build_dir =>
+ {
+ /* component */
+
+ val component_name = "zipperposition-" + 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_PLATFORM64")) getOrElse
+ error("No 64bit platform")
+
+ val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name))
+
+
+ /* build */
+
+ progress.echo("OCaml/OPAM setup ...")
+ progress.bash("isabelle ocaml_setup", echo = verbose).check
+
+ progress.echo("Building Zipperposition for " + platform_name + " ...")
+ progress.bash(cwd = build_dir.file, echo = verbose,
+ script = "isabelle_opam install -y --destdir=" + File.bash_path(build_dir) +
+ " zipperposition=" + Bash.string(version)).check
+
+
+ /* install */
+
+ File.copy(build_dir + Path.explode("doc/zipperposition/LICENSE"), component_dir)
+
+ val prg_path = Path.basic("zipperposition")
+ val exe_path = prg_path.platform_exe
+ File.copy(build_dir + Path.basic("bin") + prg_path, platform_dir + exe_path)
+
+ Executable.libraries_closure(
+ platform_dir + exe_path, filter = Set("libgmp"), patchelf = true)
+
+
+ /* 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_ZIPPERPOSITION="$COMPONENT/$ISABELLE_PLATFORM64/zipperposition"
+""")
+
+
+ /* README */
+
+ File.write(component_dir + Path.basic("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("build_zipperposition", "build prover component from OPAM repository",
+ args =>
+ {
+ var target_dir = Path.current
+ var version = default_version
+ var verbose = false
+
+ val getopts = Getopts("""
+Usage: isabelle build_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()
+
+ build_zipperposition(version = version, verbose = verbose, progress = progress,
+ target_dir = target_dir)
+ })
+}
--- a/src/Pure/General/path.scala Tue Oct 13 16:45:38 2020 +0200
+++ b/src/Pure/General/path.scala Tue Oct 13 20:28:43 2020 +0200
@@ -204,6 +204,9 @@
prfx + Path.basic(s + "~~")
}
+ def platform_exe: Path =
+ if (Platform.is_windows) ext("exe") else this
+
private val Ext = new Regex("(.*)\\.([^.]*)")
def split_ext: (Path, String) =
--- a/src/Pure/System/executable.scala Tue Oct 13 16:45:38 2020 +0200
+++ b/src/Pure/System/executable.scala Tue Oct 13 20:28:43 2020 +0200
@@ -9,11 +9,12 @@
object Executable
{
- def libraries_closure(exe_path0: Path,
+ def libraries_closure(path: Path,
mingw: MinGW = MinGW.none,
- filter: String => Boolean = _ => true): List[String] =
+ filter: String => Boolean = _ => true,
+ patchelf: Boolean = false): List[String] =
{
- val exe_path = exe_path0.expand
+ val exe_path = path.expand
val exe_dir = exe_path.dir
val exe = exe_path.base
@@ -25,7 +26,7 @@
}
def lib_name(lib: String): String =
- Library.take_prefix[Char](_ != '.',
+ Library.take_prefix[Char](c => c != '.' && c != '-',
Library.take_suffix[Char](_ != '/', lib.toList)._2)._1.mkString
val libs =
@@ -51,8 +52,16 @@
libs.foreach(lib => File.copy(Path.explode(lib), exe_dir))
if (Platform.is_linux) {
- // requires "LDFLAGS=-Wl,-rpath,_DUMMY_"
- Isabelle_System.bash("chrpath -r '$ORIGIN' " + File.bash_path(exe_path)).check
+ if (patchelf) {
+ // requires e.g. Ubuntu 16.04 LTS
+ Isabelle_System.require_command("patchelf")
+ Isabelle_System.bash("patchelf --force-rpath --set-rpath '$ORIGIN' " + File.bash_path(exe_path)).check
+ }
+ else {
+ // requires e.g. LDFLAGS=-Wl,-rpath,_DUMMY_
+ Isabelle_System.require_command("chrpath")
+ Isabelle_System.bash("chrpath -r '$ORIGIN' " + File.bash_path(exe_path)).check
+ }
}
else if (Platform.is_macos) {
val script =
--- a/src/Pure/System/isabelle_tool.scala Tue Oct 13 16:45:38 2020 +0200
+++ b/src/Pure/System/isabelle_tool.scala Tue Oct 13 20:28:43 2020 +0200
@@ -182,6 +182,7 @@
Build_SQLite.isabelle_tool,
Build_Status.isabelle_tool,
Build_VeriT.isabelle_tool,
+ Build_Zipperposition.isabelle_tool,
Check_Sources.isabelle_tool,
Components.isabelle_tool,
isabelle.vscode.Build_VSCode.isabelle_tool)
--- a/src/Pure/build-jars Tue Oct 13 16:45:38 2020 +0200
+++ b/src/Pure/build-jars Tue Oct 13 20:28:43 2020 +0200
@@ -25,6 +25,7 @@
src/Pure/Admin/build_sqlite.scala
src/Pure/Admin/build_status.scala
src/Pure/Admin/build_verit.scala
+ src/Pure/Admin/build_zipperposition.scala
src/Pure/Admin/check_sources.scala
src/Pure/Admin/ci_profile.scala
src/Pure/Admin/components.scala