--- a/src/Pure/Admin/component_polyml.scala Mon Apr 07 12:36:56 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala Wed Apr 09 15:31:27 2025 +0200
@@ -34,6 +34,22 @@
setup = MinGW.environment_export,
libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread")))
+ def bash(
+ cwd: Path,
+ platform: Isabelle_Platform,
+ mingw: MinGW,
+ script: String,
+ redirect: Boolean = false,
+ progress: Progress = new Progress
+ ): Process_Result = {
+ val script1 =
+ if (platform.is_arm && platform.is_macos) {
+ "arch -arch arm64 bash -c " + Bash.string(script)
+ }
+ else mingw.bash_script(script)
+ progress.bash(script1, cwd = cwd, redirect = redirect, echo = progress.verbose)
+ }
+
def polyml_platform(arch_64: Boolean): String = {
val platform = Isabelle_Platform.self
(if (arch_64) platform.arch_64 else platform.arch_64_32) + "-" + platform.os_name
@@ -41,6 +57,7 @@
def make_polyml(
root: Path,
+ gmp_root: Option[Path] = None,
sha1_root: Option[Path] = None,
target_dir: Path = Path.current,
arch_64: Boolean = false,
@@ -62,29 +79,29 @@
if (platform.is_linux) Isabelle_System.require_command("patchelf")
- /* bash */
+ /* configure and make */
+
+ val configure_options = {
+ val options1 = if (gmp_root.nonEmpty) List("--with-gmp") else List("--without-gmp")
- def bash(
- cwd: Path, script: String,
- redirect: Boolean = false,
- echo: Boolean = false
- ): Process_Result = {
- val script1 =
- if (platform.is_arm && platform.is_macos) {
- "arch -arch arm64 bash -c " + Bash.string(script)
+ val options2 =
+ for (opt <- info.options) yield {
+ if (opt.startsWith("CFLAGS=") && gmp_root.nonEmpty) {
+ val root0 = gmp_root.get.absolute
+ val root1 = mingw.standard_path(root0)
+ require(root0.implode == File.bash_path(root0), "Bad directory name " + root0)
+ opt + " " + "-I" + root1 + "/include -L" + root1 + "/lib"
+ }
+ else opt
}
- else mingw.bash_script(script)
- progress.bash(script1, cwd = cwd, redirect = redirect, echo = echo)
+
+ val options3 = if (arch_64) Nil else List("--enable-compact32bit")
+
+ List("--disable-shared", "--enable-intinf-as-int") :::
+ options1 ::: options2 ::: options ::: options3
}
-
- /* configure and make */
-
- val configure_options =
- List("--disable-shared", "--enable-intinf-as-int", "--with-gmp") :::
- info.options ::: options ::: (if (arch_64) Nil else List("--enable-compact32bit"))
-
- bash(root,
+ bash(root, platform, mingw,
info.setup + "\n" +
"""
[ -f Makefile ] && make distclean
@@ -93,7 +110,7 @@
rm -rf target
make && make install
} || { echo "Build failed" >&2; exit 2; }
- """, redirect = true, echo = true).check
+ """, redirect = true, progress = progress).check
/* sha1 library */
@@ -101,7 +118,8 @@
val sha1_files =
if (sha1_root.isDefined) {
val dir1 = sha1_root.get
- bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check
+ bash(dir1, platform, mingw, "./build " + sha1_platform, redirect = true,
+ progress = progress).check
val dir2 = dir1 + Path.explode(sha1_platform)
File.read_dir(dir2).map(entry => dir2 + Path.basic(entry))
@@ -152,6 +170,8 @@
/** skeleton for component **/
+ val standard_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"
val default_polyml_name = "polyml-5.9.1"
@@ -181,6 +201,7 @@
options: List[String] = Nil,
mingw: MinGW = MinGW.none,
component_name: String = "",
+ gmp_url: String = "",
polyml_url: String = default_polyml_url,
polyml_version: String = default_polyml_version,
polyml_name: String = default_polyml_name,
@@ -189,6 +210,9 @@
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
+ val platform = Isabelle_Platform.self
+
+
/* component */
val component_name1 = if (component_name.isEmpty) "polyml-" + polyml_version else component_name
@@ -199,6 +223,43 @@
/* download and build */
Isabelle_System.with_tmp_dir("download") { download_dir =>
+ /* GMP library */
+
+ val gmp_root: Option[Path] =
+ if (gmp_url.isEmpty) None
+ else {
+ val gmp_dir = Isabelle_System.make_directory(download_dir + Path.basic("gmp"))
+
+ val archive_name =
+ Url.get_base_name(gmp_url).getOrElse(error("No base name in " + quote(gmp_url)))
+ val archive = download_dir + Path.basic(archive_name)
+ Isabelle_System.download_file(gmp_url, archive, progress = progress)
+ Isabelle_System.extract(archive, gmp_dir, strip = true)
+
+ val platform_arch = if (platform.is_arm) "aarch64" else "x86_64"
+ val platform_os =
+ if (platform.is_linux) "unknown-linux-gnu"
+ else if (platform.is_windows) "w64-mingw32"
+ else if (platform.is_macos) """apple-darwin"$(uname -r)""""
+ else error("Bad platform " + platform)
+
+ progress.echo("Building GMP library ...")
+ bash(gmp_dir, platform, mingw, progress = progress,
+ script = Library.make_lines(
+ "set -e",
+ "./configure --enable-cxx --build=" + platform_arch + "-" + platform_os +
+ """ --prefix="$PWD/target"""",
+ "make",
+ "make check",
+ "make install"
+ )).check
+
+ Some(gmp_dir + Path.explode("target"))
+ }
+
+
+ /* Poly/ML */
+
val List(polyml_download, sha1_download) =
for {
(url, version, target) <-
@@ -220,6 +281,7 @@
progress.echo("Building " + polyml_platform(arch_64))
make_polyml(
root = polyml_download,
+ gmp_root = gmp_root,
sha1_root = Some(sha1_download),
target_dir = component_dir.path,
arch_64 = arch_64,
@@ -290,39 +352,11 @@
* Linux and macOS
- $ isabelle component_polyml
+ $ isabelle component_polyml -G:
* Windows (Cygwin shell)
- $ isabelle component_polyml -M /cygdrive/c/msys64
-
-
-Building libgmp on macOS
-========================
-
-The build_polyml invocations above implicitly use the GNU Multiple Precision
-Arithmetic Library (libgmp), but that is not available on macOS by default.
-Appending "--without-gmp" to the command-line omits this library. Building
-libgmp properly from sources works as follows (library headers and binaries
-will be placed in /usr/local).
-
-* Download:
-
- $ curl https://gmplib.org/download/gmp/gmp-6.3.0.tar.bz2 | tar xjf -
- $ cd gmp-6.3.0
-
-* build:
-
- $ make distclean
-
- #Intel
- $ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
-
- #ARM
- $ ./configure --enable-cxx --build=aarch64-apple-darwin"$(uname -r)"
-
- $ make && make check
- $ sudo make install
+ $ isabelle component_polyml -G: -M /cygdrive/c/msys64
Makarius
@@ -336,6 +370,7 @@
val isabelle_tool1 =
Isabelle_Tool("make_polyml", "make Poly/ML from existing sources", Scala_Project.here,
{ args =>
+ var gmp_root: Option[Path] = None
var mingw = MinGW.none
var arch_64 = false
var sha1_root: Option[Path] = None
@@ -344,14 +379,16 @@
Usage: isabelle make_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
Options are:
+ -G DIR GMP library root
-M DIR msys/mingw root specification for Windows
-m ARCH processor architecture (32 or 64, default: """ +
(if (arch_64) "64" else "32") + """)
-s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1
Make Poly/ML in the ROOT directory of its sources, with additional
- CONFIGURE_OPTIONS (e.g. --without-gmp).
+ CONFIGURE_OPTIONS.
""",
+ "G:" -> (arg => gmp_root = Some(Path.explode(arg))),
"M:" -> (arg => mingw = MinGW(Path.explode(arg))),
"m:" ->
{
@@ -367,8 +404,8 @@
case root :: options => (Path.explode(root), options)
case Nil => getopts.usage()
}
- make_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
- arch_64 = arch_64, options = options, mingw = mingw)
+ make_polyml(root, gmp_root = gmp_root, sha1_root = sha1_root,
+ progress = new Console_Progress, arch_64 = arch_64, options = options, mingw = mingw)
})
val isabelle_tool2 =
@@ -376,6 +413,7 @@
Scala_Project.here,
{ args =>
var target_dir = Path.current
+ var gmp_url = ""
var mingw = MinGW.none
var component_name = ""
var sha1_url = default_sha1_url
@@ -384,12 +422,14 @@
var polyml_version = default_polyml_version
var polyml_name = default_polyml_name
var verbose = false
-
+
val getopts = Getopts("""
Usage: isabelle component_polyml [OPTIONS] [CONFIGURE_OPTIONS]
Options are:
-D DIR target directory (default ".")
+ -G URL build GMP library from source: explicit URL or ":" for
+ """ + standard_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
@@ -402,9 +442,10 @@
-v verbose
Download and build Poly/ML component from source repositories, with additional
- CONFIGURE_OPTIONS (e.g. --without-gmp).
+ CONFIGURE_OPTIONS.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
+ "G:" -> (arg => gmp_url = if (arg == ":") standard_gmp_url else arg),
"M:" -> (arg => mingw = MinGW(Path.explode(arg))),
"N:" -> (arg => component_name = arg),
"S:" -> (arg => sha1_url = arg),
@@ -419,8 +460,8 @@
val progress = new Console_Progress(verbose = verbose)
build_polyml(options = options, mingw = mingw, component_name = component_name,
- polyml_url = polyml_url, polyml_version = polyml_version, polyml_name = polyml_name,
- sha1_url = sha1_url, sha1_version = sha1_version, target_dir = target_dir,
- progress = progress)
+ 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, progress = progress)
})
}