src/Pure/Admin/component_polyml.scala

         options =
           List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
         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
   }
 
   def make_polyml(
     root: Path,
+    gmp_root: Option[Path] = None,
     sha1_root: Option[Path] = None,
     target_dir: Path = Path.current,
     arch_64: Boolean = false,
     options: List[String] = Nil,
     mingw: MinGW = MinGW.none,

         error("Bad OS platform: " + quote(platform.os_name)))
 
     if (platform.is_linux) Isabelle_System.require_command("patchelf")
 
 
-    /* bash */
-
-    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)
+    /* configure and make */
+
+    val configure_options = {
+      val options1 = if (gmp_root.nonEmpty) List("--with-gmp") else List("--without-gmp")
+
+      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
         {
           ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """
           rm -rf target
           make && make install
         } || { echo "Build failed" >&2; exit 2; }
-      """, redirect = true, echo = true).check
+      """, redirect = true, progress = progress).check
 
 
     /* sha1 library */
 
     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))
       }
       else Nil

 
 
 
   /** 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"
 
   val default_sha1_url = "https://isabelle.sketis.net/repos/sha1/archive"

 
   def build_polyml(
     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,
     sha1_url: String = default_sha1_url,
     sha1_version: String = default_sha1_version,
     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
     val component_dir =
       Components.Directory(target_dir + Path.basic(component_name1)).create(progress = progress)
 
 
     /* 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) <-
             List((polyml_url, polyml_version, "src"), (sha1_url, sha1_version, "sha1"))
         } yield {

 
       for (arch_64 <- List(false, true)) {
         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,
           options = options,
           mingw = mingw,

 component_polyml", which can be used in the polyml component directory as
 follows:
 
 * 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
         """ + Date.Format.date(Date.now()) + "\n")
   }

   /** Isabelle tool wrappers **/
 
   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
 
         val getopts = Getopts("""
 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:" ->
             {
               case "32" => arch_64 = false
               case "64" => arch_64 = true

         val (root, options) =
           more_args match {
             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 =
     Isabelle_Tool("component_polyml", "build Poly/ML component from official repository",
       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
         var sha1_version = default_sha1_version
         var polyml_url = default_polyml_url
         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
                  (default: """ + quote(default_sha1_url) + """)
     -T VERSION   SHA1 version (default: """ + quote(default_sha1_version) + """)

     -V VERSION   Poly/ML version (default: """ + quote(default_polyml_version) + """)
     -W NAME      Poly/ML name (default: """ + quote(default_polyml_name) + """)
     -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),
           "T:" -> (arg => sha1_version = arg),
           "U:" -> (arg => polyml_url = arg),

         val options = getopts(args)
 
         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)
       })
 }