# HG changeset patch # User wenzelm # Date 1744470771 -7200 # Node ID 537e81b823290fd78c73cab2422a335a157f0ca1 # Parent 5df2050f1c312ba53a3e755ce8d270a16b90a22a clarified options: explicit use of existing GMP library; diff -r 5df2050f1c31 -r 537e81b82329 src/Pure/Admin/component_polyml.scala --- a/src/Pure/Admin/component_polyml.scala Sat Apr 12 16:00:56 2025 +0200 +++ b/src/Pure/Admin/component_polyml.scala Sat Apr 12 17:12:51 2025 +0200 @@ -252,6 +252,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, @@ -275,8 +276,8 @@ Isabelle_System.with_tmp_dir("build") { build_dir => /* GMP library */ - val gmp_root: Option[Path] = - if (gmp_url.isEmpty) None + val gmp_root1: Option[Path] = + if (gmp_url.isEmpty) gmp_root else if (platform.is_windows) error("Bad GMP source for Windows: use MinGW version instead") else { val gmp_dir = Isabelle_System.make_directory(build_dir + Path.basic("gmp")) @@ -315,7 +316,7 @@ 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, @@ -487,6 +488,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(""" @@ -494,7 +496,7 @@ Options are: -D DIR target directory (default ".") - -G URL GMP library source archive, or "" for none (--without-gmp) + -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) @@ -505,13 +507,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 = 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), @@ -519,6 +522,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) @@ -527,8 +531,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) }) }