| author | wenzelm |
| Fri, 12 Sep 2025 17:31:38 +0200 | |
| changeset 83139 | c87375585b9f |
| parent 83138 | c66d77fb729e |
| 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 |
||
| 83139 | 10 |
import java.util.{Map => JMap}
|
11 |
||
12 |
||
| 75393 | 13 |
object Isabelle_Platform {
|
| 72338 | 14 |
val settings: List[String] = |
15 |
List( |
|
16 |
"ISABELLE_PLATFORM_FAMILY", |
|
17 |
"ISABELLE_PLATFORM64", |
|
18 |
"ISABELLE_WINDOWS_PLATFORM32", |
|
| 73667 | 19 |
"ISABELLE_WINDOWS_PLATFORM64", |
20 |
"ISABELLE_APPLE_PLATFORM64") |
|
| 72338 | 21 |
|
| 82717 | 22 |
def make(env: Isabelle_System.Settings = Isabelle_System.Settings()): Isabelle_Platform = |
23 |
new Isabelle_Platform(settings.map(a => (a, Isabelle_System.getenv(a, env = env)))) |
|
24 |
||
25 |
lazy val local: Isabelle_Platform = make() |
|
| 82610 | 26 |
|
27 |
def remote(ssh: SSH.Session): Isabelle_Platform = {
|
|
28 |
val script = |
|
29 |
File.read(Path.explode("~~/lib/scripts/isabelle-platform")) + "\n" +
|
|
30 |
settings.map(a => "echo \"" + Bash.string(a) + "=$" + Bash.string(a) + "\"").mkString("\n")
|
|
31 |
val result = ssh.execute("bash -c " + Bash.string(script)).check
|
|
32 |
new Isabelle_Platform( |
|
33 |
result.out_lines.map(line => |
|
34 |
Properties.Eq.unapply(line) getOrElse error("Bad output: " + quote(result.out))))
|
|
| 72338 | 35 |
} |
| 82612 | 36 |
|
37 |
||
38 |
/* system context for progress/process */ |
|
39 |
||
40 |
object Context {
|
|
41 |
def apply( |
|
42 |
isabelle_platform: Isabelle_Platform = local, |
|
43 |
mingw: MinGW = MinGW.none, |
|
| 83124 | 44 |
apple: Boolean = true, |
| 82612 | 45 |
progress: Progress = new Progress |
46 |
): Context = {
|
|
47 |
val context_platform = isabelle_platform |
|
48 |
val context_mingw = mingw |
|
| 83124 | 49 |
val context_apple = apple |
| 82612 | 50 |
val context_progress = progress |
51 |
new Context {
|
|
52 |
override def isabelle_platform: Isabelle_Platform = context_platform |
|
53 |
override def mingw: MinGW = context_mingw |
|
| 83124 | 54 |
override def apple: Boolean = context_apple |
| 82612 | 55 |
override def progress: Progress = context_progress |
56 |
} |
|
57 |
} |
|
58 |
} |
|
59 |
||
60 |
trait Context {
|
|
61 |
def isabelle_platform: Isabelle_Platform |
|
62 |
def mingw: MinGW |
|
| 83124 | 63 |
def apple: Boolean |
| 82612 | 64 |
def progress: Progress |
65 |
||
| 83124 | 66 |
def ISABELLE_PLATFORM: String = isabelle_platform.ISABELLE_PLATFORM(windows = true, apple = apple) |
67 |
def is_linux_arm: Boolean = isabelle_platform.is_linux && isabelle_platform.is_arm |
|
68 |
def is_macos_arm: Boolean = isabelle_platform.is_macos && isabelle_platform.is_arm && apple |
|
69 |
def is_arm: Boolean = is_linux_arm || is_macos_arm |
|
70 |
||
| 82612 | 71 |
def standard_path(path: Path): String = |
|
83111
a908a0d5168b
proper Path conversion for Windows (amending b7554954d697);
wenzelm
parents:
82717
diff
changeset
|
72 |
mingw.standard_path(File.platform_path(path)) |
| 82612 | 73 |
|
| 83139 | 74 |
def bash(script: String, |
75 |
cwd: Path = Path.current, |
|
76 |
env: JMap[String, String] = Isabelle_System.Settings.env(), |
|
77 |
): Process_Result = {
|
|
| 83138 | 78 |
progress.bash( |
| 83124 | 79 |
if (is_macos_arm) "arch -arch arm64 bash -c " + Bash.string(script) |
| 83138 | 80 |
else mingw.bash_script(script), |
| 83139 | 81 |
cwd = cwd, env = env, echo = progress.verbose) |
82 |
} |
|
| 82612 | 83 |
} |
| 72338 | 84 |
} |
85 |
||
| 75393 | 86 |
class Isabelle_Platform private(val settings: List[(String, String)]) {
|
| 72338 | 87 |
private def get(name: String): String = |
| 72339 | 88 |
settings.collectFirst({ case (a, b) if a == name => b }).
|
| 72338 | 89 |
getOrElse(error("Bad platform settings variable: " + quote(name)))
|
90 |
||
91 |
val ISABELLE_PLATFORM64: String = get("ISABELLE_PLATFORM64")
|
|
92 |
val ISABELLE_WINDOWS_PLATFORM64: String = get("ISABELLE_WINDOWS_PLATFORM64")
|
|
| 73667 | 93 |
val ISABELLE_APPLE_PLATFORM64: String = get("ISABELLE_APPLE_PLATFORM64")
|
| 72349 | 94 |
|
| 80009 | 95 |
def ISABELLE_PLATFORM(windows: Boolean = false, apple: Boolean = false): String = |
96 |
proper_string(if_proper(windows, ISABELLE_WINDOWS_PLATFORM64)) orElse |
|
97 |
proper_string(if_proper(apple, ISABELLE_APPLE_PLATFORM64)) orElse |
|
98 |
proper_string(ISABELLE_PLATFORM64) getOrElse error("Missing ISABELLE_PLATFORM64")
|
|
99 |
||
| 72349 | 100 |
def is_arm: Boolean = |
| 73667 | 101 |
ISABELLE_PLATFORM64.startsWith("arm64-") ||
|
102 |
ISABELLE_APPLE_PLATFORM64.startsWith("arm64-")
|
|
| 72349 | 103 |
|
|
79548
a33a6e541cbb
proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;
wenzelm
parents:
77328
diff
changeset
|
104 |
val ISABELLE_PLATFORM_FAMILY: String = {
|
|
a33a6e541cbb
proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;
wenzelm
parents:
77328
diff
changeset
|
105 |
val family0 = get("ISABELLE_PLATFORM_FAMILY")
|
|
a33a6e541cbb
proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;
wenzelm
parents:
77328
diff
changeset
|
106 |
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
|
107 |
} |
|
a33a6e541cbb
proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;
wenzelm
parents:
77328
diff
changeset
|
108 |
|
|
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
|
109 |
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
|
110 |
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
|
111 |
def is_windows: Boolean = ISABELLE_PLATFORM_FAMILY.startsWith("windows")
|
| 72338 | 112 |
|
|
72352
f4bd6f123fdf
more systematic platform support, including arm64-linux;
wenzelm
parents:
72349
diff
changeset
|
113 |
def arch_64: String = if (is_arm) "arm64" else "x86_64" |
| 73667 | 114 |
def arch_64_32: String = if (is_arm) "arm64_32" else "x86_64_32" |
115 |
||
|
79562
ceaef5bae253
proper os_name "linux" instead of "linux_arm" (amending a33a6e541cbb);
wenzelm
parents:
79556
diff
changeset
|
116 |
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
|
117 |
|
| 72338 | 118 |
override def toString: String = ISABELLE_PLATFORM_FAMILY |
119 |
} |