author | wenzelm |
Thu, 07 Aug 2025 22:42:21 +0200 | |
changeset 82968 | b2b88d5b01b6 |
parent 82717 | 8d42bf3b821d |
permissions | -rw-r--r-- |
72338 | 1 |
/* Title: Pure/System/isabelle_platform.scala |
2 |
Author: Makarius |
|
3 |
||
82611 | 4 |
Isabelle/Scala platform information, based on settings environment. |
72338 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
75393 | 10 |
object Isabelle_Platform { |
72338 | 11 |
val settings: List[String] = |
12 |
List( |
|
13 |
"ISABELLE_PLATFORM_FAMILY", |
|
14 |
"ISABELLE_PLATFORM64", |
|
15 |
"ISABELLE_WINDOWS_PLATFORM32", |
|
73667 | 16 |
"ISABELLE_WINDOWS_PLATFORM64", |
17 |
"ISABELLE_APPLE_PLATFORM64") |
|
72338 | 18 |
|
82717 | 19 |
def make(env: Isabelle_System.Settings = Isabelle_System.Settings()): Isabelle_Platform = |
20 |
new Isabelle_Platform(settings.map(a => (a, Isabelle_System.getenv(a, env = env)))) |
|
21 |
||
22 |
lazy val local: Isabelle_Platform = make() |
|
82610 | 23 |
|
24 |
def remote(ssh: SSH.Session): Isabelle_Platform = { |
|
25 |
val script = |
|
26 |
File.read(Path.explode("~~/lib/scripts/isabelle-platform")) + "\n" + |
|
27 |
settings.map(a => "echo \"" + Bash.string(a) + "=$" + Bash.string(a) + "\"").mkString("\n") |
|
28 |
val result = ssh.execute("bash -c " + Bash.string(script)).check |
|
29 |
new Isabelle_Platform( |
|
30 |
result.out_lines.map(line => |
|
31 |
Properties.Eq.unapply(line) getOrElse error("Bad output: " + quote(result.out)))) |
|
72338 | 32 |
} |
82612 | 33 |
|
34 |
||
35 |
/* system context for progress/process */ |
|
36 |
||
37 |
object Context { |
|
38 |
def apply( |
|
39 |
isabelle_platform: Isabelle_Platform = local, |
|
40 |
mingw: MinGW = MinGW.none, |
|
41 |
progress: Progress = new Progress |
|
42 |
): Context = { |
|
43 |
val context_platform = isabelle_platform |
|
44 |
val context_mingw = mingw |
|
45 |
val context_progress = progress |
|
46 |
new Context { |
|
47 |
override def isabelle_platform: Isabelle_Platform = context_platform |
|
48 |
override def mingw: MinGW = context_mingw |
|
49 |
override def progress: Progress = context_progress |
|
50 |
} |
|
51 |
} |
|
52 |
} |
|
53 |
||
54 |
trait Context { |
|
55 |
def isabelle_platform: Isabelle_Platform |
|
56 |
def mingw: MinGW |
|
57 |
def progress: Progress |
|
58 |
||
59 |
def standard_path(path: Path): String = |
|
60 |
mingw.standard_path(File.standard_path(path)) |
|
61 |
||
62 |
def execute(cwd: Path, script_lines: String*): Process_Result = { |
|
63 |
val script = cat_lines("set -e" :: script_lines.toList) |
|
64 |
val script1 = |
|
65 |
if (isabelle_platform.is_arm && isabelle_platform.is_macos) { |
|
66 |
"arch -arch arm64 bash -c " + Bash.string(script) |
|
67 |
} |
|
68 |
else mingw.bash_script(script) |
|
69 |
progress.bash(script1, cwd = cwd, echo = progress.verbose).check |
|
70 |
} |
|
71 |
} |
|
72338 | 72 |
} |
73 |
||
75393 | 74 |
class Isabelle_Platform private(val settings: List[(String, String)]) { |
72338 | 75 |
private def get(name: String): String = |
72339 | 76 |
settings.collectFirst({ case (a, b) if a == name => b }). |
72338 | 77 |
getOrElse(error("Bad platform settings variable: " + quote(name))) |
78 |
||
79 |
val ISABELLE_PLATFORM64: String = get("ISABELLE_PLATFORM64") |
|
80 |
val ISABELLE_WINDOWS_PLATFORM64: String = get("ISABELLE_WINDOWS_PLATFORM64") |
|
73667 | 81 |
val ISABELLE_APPLE_PLATFORM64: String = get("ISABELLE_APPLE_PLATFORM64") |
72349 | 82 |
|
80009 | 83 |
def ISABELLE_PLATFORM(windows: Boolean = false, apple: Boolean = false): String = |
84 |
proper_string(if_proper(windows, ISABELLE_WINDOWS_PLATFORM64)) orElse |
|
85 |
proper_string(if_proper(apple, ISABELLE_APPLE_PLATFORM64)) orElse |
|
86 |
proper_string(ISABELLE_PLATFORM64) getOrElse error("Missing ISABELLE_PLATFORM64") |
|
87 |
||
72349 | 88 |
def is_arm: Boolean = |
73667 | 89 |
ISABELLE_PLATFORM64.startsWith("arm64-") || |
90 |
ISABELLE_APPLE_PLATFORM64.startsWith("arm64-") |
|
72349 | 91 |
|
79548
a33a6e541cbb
proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;
wenzelm
parents:
77328
diff
changeset
|
92 |
val ISABELLE_PLATFORM_FAMILY: String = { |
a33a6e541cbb
proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;
wenzelm
parents:
77328
diff
changeset
|
93 |
val family0 = get("ISABELLE_PLATFORM_FAMILY") |
a33a6e541cbb
proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;
wenzelm
parents:
77328
diff
changeset
|
94 |
if (family0 == "linux" && is_arm) "linux_arm" else family0 |
a33a6e541cbb
proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;
wenzelm
parents:
77328
diff
changeset
|
95 |
} |
a33a6e541cbb
proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;
wenzelm
parents:
77328
diff
changeset
|
96 |
|
79556
0631dfc0db07
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
wenzelm
parents:
79548
diff
changeset
|
97 |
def is_linux: Boolean = ISABELLE_PLATFORM_FAMILY.startsWith("linux") |
0631dfc0db07
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
wenzelm
parents:
79548
diff
changeset
|
98 |
def is_macos: Boolean = ISABELLE_PLATFORM_FAMILY.startsWith("macos") |
0631dfc0db07
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
wenzelm
parents:
79548
diff
changeset
|
99 |
def is_windows: Boolean = ISABELLE_PLATFORM_FAMILY.startsWith("windows") |
72338 | 100 |
|
72352
f4bd6f123fdf
more systematic platform support, including arm64-linux;
wenzelm
parents:
72349
diff
changeset
|
101 |
def arch_64: String = if (is_arm) "arm64" else "x86_64" |
73667 | 102 |
def arch_64_32: String = if (is_arm) "arm64_32" else "x86_64_32" |
103 |
||
79562
ceaef5bae253
proper os_name "linux" instead of "linux_arm" (amending a33a6e541cbb);
wenzelm
parents:
79556
diff
changeset
|
104 |
def os_name: String = if (is_macos) "darwin" else if (is_windows) "windows" else "linux" |
72352
f4bd6f123fdf
more systematic platform support, including arm64-linux;
wenzelm
parents:
72349
diff
changeset
|
105 |
|
72338 | 106 |
override def toString: String = ISABELLE_PLATFORM_FAMILY |
107 |
} |