src/Pure/System/mingw.scala
author Manuel Eberl <eberlm@in.tum.de>
Wed, 23 Apr 2025 01:38:06 +0200
changeset 82541 5160b68e78a9
parent 82511 f887c0decc26
permissions -rw-r--r--
some material on power series and infinite products
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
72421
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/mingw.scala
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     3
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     4
Support for MSYS2/MinGW64 on Windows.
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     5
*/
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     6
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     7
package isabelle
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     8
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
     9
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    10
object MinGW {
82468
40a609d67b33 clarified Windows: always use MinGW version (it is unclear how to build libgmp-10.dll);
wenzelm
parents: 82467
diff changeset
    11
  def env_prefix: String =
82511
f887c0decc26 update to recent MSYS2 / MinGW, which also works via Cygwin;
wenzelm
parents: 82497
diff changeset
    12
    Bash.exports("PATH=/usr/bin:/ucrt64/bin", "CONFIG_SITE=/ucrt64/etc/config.site")
72421
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    13
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    14
  val none: MinGW = new MinGW(None)
72431
b8b97c49e339 tuned signature;
wenzelm
parents: 72428
diff changeset
    15
  def apply(path: Path) = new MinGW(Some(path))
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    16
}
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    17
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    18
class MinGW private(val root: Option[Path]) {
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    19
  override def toString: String =
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    20
    root match {
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    21
      case None => "MinGW.none"
72431
b8b97c49e339 tuned signature;
wenzelm
parents: 72428
diff changeset
    22
      case Some(msys_root) => "MinGW(" + msys_root.toString + ")"
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    23
    }
72421
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    24
82497
b7554954d697 more accurate MinGW path conversion: support locations outside of mingw.root;
wenzelm
parents: 82468
diff changeset
    25
  private def convert_path(str: String, opt: String): Option[String] =
82463
3125fd1ee69c added option -G to build GMP library from sources;
wenzelm
parents: 75393
diff changeset
    26
    root match {
3125fd1ee69c added option -G to build GMP library from sources;
wenzelm
parents: 75393
diff changeset
    27
      case Some(msys_root) if Platform.is_windows =>
3125fd1ee69c added option -G to build GMP library from sources;
wenzelm
parents: 75393
diff changeset
    28
        val command_line =
3125fd1ee69c added option -G to build GMP library from sources;
wenzelm
parents: 75393
diff changeset
    29
          java.util.List.of(
82497
b7554954d697 more accurate MinGW path conversion: support locations outside of mingw.root;
wenzelm
parents: 82468
diff changeset
    30
            File.platform_path(msys_root) + "\\usr\\bin\\cygpath", opt, str)
82463
3125fd1ee69c added option -G to build GMP library from sources;
wenzelm
parents: 75393
diff changeset
    31
        val res = isabelle.setup.Environment.exec_process(command_line, null, null, false)
82497
b7554954d697 more accurate MinGW path conversion: support locations outside of mingw.root;
wenzelm
parents: 82468
diff changeset
    32
        if (res.ok) Some(Library.trim_line(res.out))
82463
3125fd1ee69c added option -G to build GMP library from sources;
wenzelm
parents: 75393
diff changeset
    33
        else error("Error: " + quote(Library.trim_line(res.err)))
82497
b7554954d697 more accurate MinGW path conversion: support locations outside of mingw.root;
wenzelm
parents: 82468
diff changeset
    34
      case _ => None
82463
3125fd1ee69c added option -G to build GMP library from sources;
wenzelm
parents: 75393
diff changeset
    35
    }
3125fd1ee69c added option -G to build GMP library from sources;
wenzelm
parents: 75393
diff changeset
    36
82497
b7554954d697 more accurate MinGW path conversion: support locations outside of mingw.root;
wenzelm
parents: 82468
diff changeset
    37
  def standard_path(platform_path: String): String =
b7554954d697 more accurate MinGW path conversion: support locations outside of mingw.root;
wenzelm
parents: 82468
diff changeset
    38
    convert_path(platform_path, "-u") getOrElse File.standard_path(platform_path)
b7554954d697 more accurate MinGW path conversion: support locations outside of mingw.root;
wenzelm
parents: 82468
diff changeset
    39
b7554954d697 more accurate MinGW path conversion: support locations outside of mingw.root;
wenzelm
parents: 82468
diff changeset
    40
  def platform_path(standard_path: String): String =
b7554954d697 more accurate MinGW path conversion: support locations outside of mingw.root;
wenzelm
parents: 82468
diff changeset
    41
    convert_path(standard_path, "-w") getOrElse File.platform_path(standard_path)
b7554954d697 more accurate MinGW path conversion: support locations outside of mingw.root;
wenzelm
parents: 82468
diff changeset
    42
82468
40a609d67b33 clarified Windows: always use MinGW version (it is unclear how to build libgmp-10.dll);
wenzelm
parents: 82467
diff changeset
    43
  def bash_script(script: String, env_prefix: String = MinGW.env_prefix): String =
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    44
    root match {
72428
b7351ffe0dbc clarified signature: allow complex bash script;
wenzelm
parents: 72427
diff changeset
    45
      case None => script
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    46
      case Some(msys_root) =>
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    47
        File.bash_path(msys_root + Path.explode("usr/bin/bash")) +
82465
3cc075052033 tuned signature;
wenzelm
parents: 82463
diff changeset
    48
          " -c " + Bash.string(env_prefix + script)
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    49
    }
72421
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    50
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    51
  def get_root: Path =
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    52
    if (!Platform.is_windows) error("Windows platform required")
72425
d0937d55eb90 clarified errors;
wenzelm
parents: 72424
diff changeset
    53
    else if (root.isEmpty) error("Windows platform requires msys/mingw root specification")
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    54
    else root.get
72421
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    55
82467
b0740dce1f1d clarified signature: fewer warnings in IntelliJ IDEA;
wenzelm
parents: 82465
diff changeset
    56
  def check(): Unit = {
72424
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    57
    if (Platform.is_windows) {
10c07d224035 tuned signature;
wenzelm
parents: 72421
diff changeset
    58
      get_root
72428
b7351ffe0dbc clarified signature: allow complex bash script;
wenzelm
parents: 72427
diff changeset
    59
      try { require(Isabelle_System.bash(bash_script("uname -s")).check.out.startsWith("MSYS")) }
72432
86f8fcdcff4a clarified message;
wenzelm
parents: 72431
diff changeset
    60
      catch { case ERROR(msg) => cat_error("Bad msys/mingw installation " + get_root, msg) }
72421
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    61
    }
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    62
  }
9a8bc089890d support for MSYS2/MinGW64 on Windows;
wenzelm
parents:
diff changeset
    63
}