# HG changeset patch
# User wenzelm
# Date 1744539828 -7200
# Node ID b7554954d697a202fe102f32de182e09e5131d0b
# Parent  0366d0139f15541983f814d1ba17ab87984f0c0f
more accurate MinGW path conversion: support locations outside of mingw.root;
uniform treatment of GMP, including Windows;

diff -r 0366d0139f15 -r b7554954d697 src/Pure/Admin/component_polyml.scala
--- a/src/Pure/Admin/component_polyml.scala	Sat Apr 12 22:10:57 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala	Sun Apr 13 12:23:48 2025 +0200
@@ -43,7 +43,8 @@
       }
       else error("Bad platform: " + quote(platform.toString))
 
-    def standard_path(path: Path): String = mingw.standard_path(path)
+    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
@@ -124,8 +125,7 @@
 
     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=")
 
@@ -224,9 +224,7 @@
 
   /** skeleton for component **/
 
-  def default_gmp_url: String =
-    if (Platform.is_windows) ""
-    else "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"
@@ -284,7 +282,6 @@
 
       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"))
 
diff -r 0366d0139f15 -r b7554954d697 src/Pure/System/executable.scala
--- a/src/Pure/System/executable.scala	Sat Apr 12 22:10:57 2025 +0200
+++ b/src/Pure/System/executable.scala	Sun Apr 13 12:23:48 2025 +0200
@@ -43,13 +43,8 @@
       }
       else {
         val Pattern = """^.*=>\s*(/.+)\s+\(.*\)$""".r
-        val prefix =
-          mingw.root match {
-            case None => ""
-            case Some(path) => path.absolute.implode
-          }
         for { case Pattern(lib) <- ldd_lines if filter(lib_name(lib)) }
-          yield prefix + lib
+          yield File.standard_path(mingw.platform_path(lib))
       }
 
     if (libs.nonEmpty) {
diff -r 0366d0139f15 -r b7554954d697 src/Pure/System/mingw.scala
--- a/src/Pure/System/mingw.scala	Sat Apr 12 22:10:57 2025 +0200
+++ b/src/Pure/System/mingw.scala	Sun Apr 13 12:23:48 2025 +0200
@@ -22,18 +22,24 @@
       case Some(msys_root) => "MinGW(" + msys_root.toString + ")"
     }
 
-  def standard_path(path: Path): String =
+  private def convert_path(str: String, opt: String): Option[String] =
     root match {
       case Some(msys_root) if Platform.is_windows =>
         val command_line =
           java.util.List.of(
-            File.platform_path(msys_root) + "\\usr\\bin\\cygpath", "-u", File.platform_path(path))
+            File.platform_path(msys_root) + "\\usr\\bin\\cygpath", opt, str)
         val res = isabelle.setup.Environment.exec_process(command_line, null, null, false)
-        if (res.ok) Library.trim_line(res.out)
+        if (res.ok) Some(Library.trim_line(res.out))
         else error("Error: " + quote(Library.trim_line(res.err)))
-      case _ => File.standard_path(path)
+      case _ => None
     }
 
+  def standard_path(platform_path: String): String =
+    convert_path(platform_path, "-u") getOrElse File.standard_path(platform_path)
+
+  def platform_path(standard_path: String): String =
+    convert_path(standard_path, "-w") getOrElse File.platform_path(standard_path)
+
   def bash_script(script: String, env_prefix: String = MinGW.env_prefix): String =
     root match {
       case None => script