| 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-- |
| 72421 | 1 |
/* Title: Pure/System/mingw.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Support for MSYS2/MinGW64 on Windows. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
| 75393 | 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 | 13 |
|
| 72424 | 14 |
val none: MinGW = new MinGW(None) |
| 72431 | 15 |
def apply(path: Path) = new MinGW(Some(path)) |
| 72424 | 16 |
} |
17 |
||
| 75393 | 18 |
class MinGW private(val root: Option[Path]) {
|
| 72424 | 19 |
override def toString: String = |
20 |
root match {
|
|
21 |
case None => "MinGW.none" |
|
| 72431 | 22 |
case Some(msys_root) => "MinGW(" + msys_root.toString + ")"
|
| 72424 | 23 |
} |
| 72421 | 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 | 44 |
root match {
|
| 72428 | 45 |
case None => script |
| 72424 | 46 |
case Some(msys_root) => |
47 |
File.bash_path(msys_root + Path.explode("usr/bin/bash")) +
|
|
| 82465 | 48 |
" -c " + Bash.string(env_prefix + script) |
| 72424 | 49 |
} |
| 72421 | 50 |
|
| 72424 | 51 |
def get_root: Path = |
52 |
if (!Platform.is_windows) error("Windows platform required")
|
|
| 72425 | 53 |
else if (root.isEmpty) error("Windows platform requires msys/mingw root specification")
|
| 72424 | 54 |
else root.get |
| 72421 | 55 |
|
|
82467
b0740dce1f1d
clarified signature: fewer warnings in IntelliJ IDEA;
wenzelm
parents:
82465
diff
changeset
|
56 |
def check(): Unit = {
|
| 72424 | 57 |
if (Platform.is_windows) {
|
58 |
get_root |
|
| 72428 | 59 |
try { require(Isabelle_System.bash(bash_script("uname -s")).check.out.startsWith("MSYS")) }
|
| 72432 | 60 |
catch { case ERROR(msg) => cat_error("Bad msys/mingw installation " + get_root, msg) }
|
| 72421 | 61 |
} |
62 |
} |
|
63 |
} |