--- a/src/Pure/Admin/component_polyml.scala Sat Apr 12 22:42:32 2025 +0100
+++ b/src/Pure/Admin/component_polyml.scala Sun Apr 13 20:21:57 2025 +0200
@@ -17,29 +17,34 @@
setup: String = "",
libs: Set[String] = Set.empty)
- private val platform_info = Map(
- "linux" ->
- Platform_Info(
- options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"),
- libs = Set("libgmp")),
- "darwin" ->
- Platform_Info(
- options = List("CFLAGS=-O3", "CXXFLAGS=-O3", "LDFLAGS=-segprot POLY rwx rwx"),
- setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin",
- libs = Set("libpolyml", "libgmp")),
- "windows" ->
- Platform_Info(
- options =
- List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
- setup = MinGW.env_prefix,
- libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread")))
-
sealed case class Platform_Context(
platform: Isabelle_Platform = Isabelle_Platform.self,
mingw: MinGW = MinGW.none,
progress: Progress = new Progress
) {
- def standard_path(path: Path): String = mingw.standard_path(path)
+ def info: Platform_Info =
+ if (platform.is_linux) {
+ Platform_Info(
+ options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"),
+ libs = Set("libgmp"))
+ }
+ else if (platform.is_macos) {
+ Platform_Info(
+ options = List("CFLAGS=-O3", "CXXFLAGS=-O3", "LDFLAGS=-segprot POLY rwx rwx"),
+ setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin",
+ libs = Set("libpolyml", "libgmp"))
+ }
+ else if (platform.is_windows) {
+ Platform_Info(
+ options =
+ List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
+ setup = MinGW.env_prefix,
+ libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread"))
+ }
+ else error("Bad platform: " + quote(platform.toString))
+
+ def standard_path(path: Path): String =
+ mingw.standard_path(File.standard_path(path))
def polyml(arch_64: Boolean): String =
(if (arch_64) platform.arch_64 else platform.arch_64_32) + "-" + platform.os_name
@@ -84,12 +89,18 @@
"[ -f Makefile ] && make distclean",
"./configure --disable-static --enable-shared --enable-cxx" +
" --build=" + platform_arch + "-" + platform_os +
- " --prefix=" + Bash.string(platform_context.standard_path(target_dir)) +
- if_proper(options, " " + Bash.strings(options)),
+ """ --prefix="$PWD/target" """ + Bash.strings(options),
+ "rm -rf target",
"make",
"make check",
"make install")
+ if (platform.is_windows) {
+ val bin_dir = target_dir + Path.explode("bin")
+ val lib_dir = target_dir + Path.explode("lib")
+ Isabelle_System.copy_dir(bin_dir, lib_dir, direct = true)
+ }
+
target_dir
}
@@ -107,19 +118,14 @@
val platform = platform_context.platform
- val info =
- platform_info.getOrElse(platform.os_name,
- error("Bad OS platform: " + quote(platform.os_name)))
-
- if (platform.is_linux) Isabelle_System.require_command("patchelf")
+ val info = platform_context.info
/* configure and make */
val configure_options = {
val options1 =
- if (gmp_root.nonEmpty || platform.is_windows) List("--with-gmp")
- else List("--without-gmp")
+ if (gmp_root.nonEmpty) List("--with-gmp") else List("--without-gmp")
def detect_CFLAGS(s: String): Boolean = s.startsWith("CFLAGS=")
@@ -190,7 +196,7 @@
for (file <- sha1_files) Isabelle_System.copy_file(file, platform_dir)
- Executable.libraries_closure(
+ Executable.library_closure(
platform_dir + Path.basic("poly").platform_exe,
env_prefix = gmp_setup + "\n",
mingw = platform_context.mingw,
@@ -218,7 +224,7 @@
/** skeleton for component **/
- val standard_gmp_url = "https://gmplib.org/download/gmp/gmp-6.3.0.tar.bz2"
+ val default_gmp_url = "https://gmplib.org/download/gmp/gmp-6.3.0.tar.bz2"
val default_polyml_url = "https://github.com/polyml/polyml/archive"
val default_polyml_version = "90c0dbb2514e"
@@ -250,6 +256,7 @@
options: List[String] = Nil,
component_name: String = "",
gmp_url: String = "",
+ gmp_root: Option[Path] = None,
polyml_url: String = default_polyml_url,
polyml_version: String = default_polyml_version,
polyml_name: String = default_polyml_name,
@@ -273,9 +280,8 @@
Isabelle_System.with_tmp_dir("build") { build_dir =>
/* GMP library */
- val gmp_root: Option[Path] =
- if (gmp_url.isEmpty) None
- else if (platform.is_windows) error("Bad GMP source for Windows: use MinGW version instead")
+ val gmp_root1: Option[Path] =
+ if (gmp_url.isEmpty) gmp_root
else {
val gmp_dir = Isabelle_System.make_directory(build_dir + Path.basic("gmp"))
@@ -309,11 +315,11 @@
init_src_root(component_dir.src, "RootX86.ML", "ROOT.ML")
for (arch_64 <- List(false, true)) {
- progress.echo("Building " + platform_context.polyml(arch_64))
+ progress.echo("Building Poly/ML " + platform_context.polyml(arch_64))
make_polyml(
platform_context,
root = polyml_download,
- gmp_root = gmp_root,
+ gmp_root = gmp_root1,
sha1_root = Some(sha1_download),
target_dir = component_dir.path,
arch_64 = arch_64,
@@ -382,11 +388,11 @@
* Linux and macOS
- $ isabelle component_polyml -G:
+ $ isabelle component_polyml
* Windows (Cygwin shell)
- $ isabelle component_polyml -G: -M /cygdrive/c/msys64
+ $ isabelle component_polyml -M /cygdrive/c/msys64
Makarius
@@ -423,8 +429,12 @@
}
val progress = new Console_Progress(verbose = verbose)
- make_polyml_gmp(Platform_Context(mingw = mingw, progress = progress),
- root, options = options)
+
+ val target_dir =
+ make_polyml_gmp(Platform_Context(mingw = mingw, progress = progress),
+ root, options = options)
+
+ progress.echo("GMP installation directory: " + target_dir)
})
val isabelle_tool2 =
@@ -477,7 +487,7 @@
Scala_Project.here,
{ args =>
var target_dir = Path.current
- var gmp_url = ""
+ var gmp_url = default_gmp_url
var mingw = MinGW.none
var component_name = ""
var sha1_url = default_sha1_url
@@ -485,6 +495,7 @@
var polyml_url = default_polyml_url
var polyml_version = default_polyml_version
var polyml_name = default_polyml_name
+ var gmp_root: Option[Path] = None
var verbose = false
val getopts = Getopts("""
@@ -492,8 +503,8 @@
Options are:
-D DIR target directory (default ".")
- -G URL build GMP library from source: explicit URL or ":" for
- """ + standard_gmp_url + """
+ -G URL build GMP library from source (overrides option -g)
+ (default """ + quote(default_gmp_url) + """)
-M DIR msys/mingw root specification for Windows
-N NAME component name (default: derived from Poly/ML version)
-S URL SHA1 repository archive area
@@ -503,13 +514,14 @@
(default: """ + quote(default_polyml_url) + """)
-V VERSION Poly/ML version (default: """ + quote(default_polyml_version) + """)
-W NAME Poly/ML name (default: """ + quote(default_polyml_name) + """)
+ -g DIR use existing GMP library (overrides option -G)
-v verbose
Download and build Poly/ML component from source repositories, with additional
CONFIGURE_OPTIONS.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
- "G:" -> (arg => gmp_url = if (arg == ":") standard_gmp_url else arg),
+ "G:" -> (arg => { gmp_url = arg; gmp_root = None }),
"M:" -> (arg => mingw = MinGW(Path.explode(arg))),
"N:" -> (arg => component_name = arg),
"S:" -> (arg => sha1_url = arg),
@@ -517,6 +529,7 @@
"U:" -> (arg => polyml_url = arg),
"V:" -> (arg => polyml_version = arg),
"W:" -> (arg => polyml_name = arg),
+ "g:" -> (arg => { gmp_root = Some(Path.explode(arg)); gmp_url = "" }),
"v" -> (_ => verbose = true))
val options = getopts(args)
@@ -525,8 +538,8 @@
val platform_context = Platform_Context(mingw = mingw, progress = progress)
build_polyml(platform_context, options = options, component_name = component_name,
- gmp_url = gmp_url, polyml_url = polyml_url, polyml_version = polyml_version,
- polyml_name = polyml_name, sha1_url = sha1_url, sha1_version = sha1_version,
- target_dir = target_dir)
+ gmp_url = gmp_url, gmp_root = gmp_root, polyml_url = polyml_url,
+ polyml_version = polyml_version, polyml_name = polyml_name, sha1_url = sha1_url,
+ sha1_version = sha1_version, target_dir = target_dir)
})
}