# HG changeset patch # User wenzelm # Date 1602613723 -7200 # Node ID e2e9ef9aa2df093944c02eca0ee58920d5a54fba # Parent 15fc6320da6807a5f29ba853a71ab3ac637e060f# Parent 96f56191aaeadddd18b4f2c3e8bd8ff44f3e6a26 merged diff -r 15fc6320da68 -r e2e9ef9aa2df NEWS --- 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. diff -r 15fc6320da68 -r e2e9ef9aa2df lib/scripts/getfunctions --- 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 diff -r 15fc6320da68 -r e2e9ef9aa2df src/Pure/Admin/build_csdp.scala --- 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")) } diff -r 15fc6320da68 -r e2e9ef9aa2df src/Pure/Admin/build_polyml.scala --- 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 = diff -r 15fc6320da68 -r e2e9ef9aa2df src/Pure/Admin/build_zipperposition.scala --- /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) + }) +} diff -r 15fc6320da68 -r e2e9ef9aa2df src/Pure/General/path.scala --- 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) = diff -r 15fc6320da68 -r e2e9ef9aa2df src/Pure/System/executable.scala --- 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 = diff -r 15fc6320da68 -r e2e9ef9aa2df src/Pure/System/isabelle_tool.scala --- 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) diff -r 15fc6320da68 -r e2e9ef9aa2df src/Pure/build-jars --- 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