clarified Windows: always use MinGW version (it is unclear how to build libgmp-10.dll);

--- a/src/Pure/Admin/component_polyml.scala	Wed Apr 09 22:29:11 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala	Wed Apr 09 22:37:58 2025 +0200
@@ -31,7 +31,7 @@
       Platform_Info(
         options =
           List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
-        setup = MinGW.env_prefix(),
+        setup = MinGW.env_prefix,
         libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread")))
 
   sealed case class Platform_Context(
@@ -80,7 +80,9 @@
     /* configure and make */
 
     val configure_options = {
-      val options1 = if (gmp_root.nonEmpty) List("--with-gmp") else List("--without-gmp")
+      val options1 =
+        if (gmp_root.nonEmpty || platform.is_windows) List("--with-gmp")
+        else List("--without-gmp")
 
       val options2 =
         for (opt <- info.options) yield {
@@ -225,6 +227,7 @@
 
       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")
         else {
           val gmp_dir = Isabelle_System.make_directory(download_dir + Path.basic("gmp"))
 

--- a/src/Pure/System/mingw.scala	Wed Apr 09 22:29:11 2025 +0200
+++ b/src/Pure/System/mingw.scala	Wed Apr 09 22:37:58 2025 +0200
@@ -8,12 +8,8 @@
 
 
 object MinGW {
-  def env_prefix(pre_path: String = "", post_path: String = ""): String = {
-    val path =
-      if_proper(pre_path, pre_path + ":") + "/usr/bin:/bin:/mingw64/bin" +
-      if_proper(post_path, ":" + post_path)
-    Bash.exports("PATH=" + path, "CONFIG_SITE=/mingw64/etc/config.site")
-  }
+  def env_prefix: String =
+    Bash.exports("PATH=/usr/bin:/bin:/mingw64/bin", "CONFIG_SITE=/mingw64/etc/config.site")
 
   val none: MinGW = new MinGW(None)
   def apply(path: Path) = new MinGW(Some(path))
@@ -38,7 +34,7 @@
       case _ => File.standard_path(path)
     }
 
-  def bash_script(script: String, env_prefix: String = MinGW.env_prefix()): String =
+  def bash_script(script: String, env_prefix: String = MinGW.env_prefix): String =
     root match {
       case None => script
       case Some(msys_root) =>