src/Pure/System/isabelle_platform.scala
author wenzelm
Thu, 07 Aug 2025 22:42:21 +0200
changeset 82968 b2b88d5b01b6
parent 82717 8d42bf3b821d
permissions -rw-r--r--
update to jdk-21.0.8; enforce rebuild of Isabelle/ML and Isabelle/Scala;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/isabelle_platform.scala
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
     3
82611
cf64152e9f51 tuned comments;
wenzelm
parents: 82610
diff changeset
     4
Isabelle/Scala platform information, based on settings environment.
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
     5
*/
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
     6
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
     7
package isabelle
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
     8
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
     9
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73716
diff changeset
    10
object Isabelle_Platform {
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    11
  val settings: List[String] =
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    12
    List(
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    13
      "ISABELLE_PLATFORM_FAMILY",
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    14
      "ISABELLE_PLATFORM64",
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    15
      "ISABELLE_WINDOWS_PLATFORM32",
73667
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
    16
      "ISABELLE_WINDOWS_PLATFORM64",
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
    17
      "ISABELLE_APPLE_PLATFORM64")
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    18
82717
8d42bf3b821d tuned signature: more operations;
wenzelm
parents: 82612
diff changeset
    19
  def make(env: Isabelle_System.Settings = Isabelle_System.Settings()): Isabelle_Platform =
8d42bf3b821d tuned signature: more operations;
wenzelm
parents: 82612
diff changeset
    20
    new Isabelle_Platform(settings.map(a => (a, Isabelle_System.getenv(a, env = env))))
8d42bf3b821d tuned signature: more operations;
wenzelm
parents: 82612
diff changeset
    21
8d42bf3b821d tuned signature: more operations;
wenzelm
parents: 82612
diff changeset
    22
  lazy val local: Isabelle_Platform = make()
82610
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    23
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    24
  def remote(ssh: SSH.Session): Isabelle_Platform = {
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    25
    val script =
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    26
      File.read(Path.explode("~~/lib/scripts/isabelle-platform")) + "\n" +
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    27
        settings.map(a => "echo \"" + Bash.string(a) + "=$" + Bash.string(a) + "\"").mkString("\n")
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    28
    val result = ssh.execute("bash -c " + Bash.string(script)).check
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    29
    new Isabelle_Platform(
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    30
      result.out_lines.map(line =>
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    31
        Properties.Eq.unapply(line) getOrElse error("Bad output: " + quote(result.out))))
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    32
  }
82612
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    33
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    34
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    35
  /* system context for progress/process */
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    36
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    37
  object Context {
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    38
    def apply(
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    39
      isabelle_platform: Isabelle_Platform = local,
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    40
      mingw: MinGW = MinGW.none,
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    41
      progress: Progress = new Progress
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    42
    ): Context = {
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    43
      val context_platform = isabelle_platform
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    44
      val context_mingw = mingw
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    45
      val context_progress = progress
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    46
      new Context {
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    47
        override def isabelle_platform: Isabelle_Platform = context_platform
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    48
        override def mingw: MinGW = context_mingw
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    49
        override def progress: Progress = context_progress
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    50
      }
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    51
    }
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    52
  }
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    53
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    54
  trait Context {
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    55
    def isabelle_platform: Isabelle_Platform
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    56
    def mingw: MinGW
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    57
    def progress: Progress
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    58
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    59
    def standard_path(path: Path): String =
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    60
      mingw.standard_path(File.standard_path(path))
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    61
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    62
    def execute(cwd: Path, script_lines: String*): Process_Result = {
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    63
      val script = cat_lines("set -e" :: script_lines.toList)
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    64
      val script1 =
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    65
        if (isabelle_platform.is_arm && isabelle_platform.is_macos) {
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    66
          "arch -arch arm64 bash -c " + Bash.string(script)
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    67
        }
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    68
        else mingw.bash_script(script)
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    69
      progress.bash(script1, cwd = cwd, echo = progress.verbose).check
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    70
    }
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    71
  }
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    72
}
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    73
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73716
diff changeset
    74
class Isabelle_Platform private(val settings: List[(String, String)]) {
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    75
  private def get(name: String): String =
72339
626920749f5d tuned signature;
wenzelm
parents: 72338
diff changeset
    76
    settings.collectFirst({ case (a, b) if a == name => b }).
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    77
      getOrElse(error("Bad platform settings variable: " + quote(name)))
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    78
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    79
  val ISABELLE_PLATFORM64: String = get("ISABELLE_PLATFORM64")
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    80
  val ISABELLE_WINDOWS_PLATFORM64: String = get("ISABELLE_WINDOWS_PLATFORM64")
73667
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
    81
  val ISABELLE_APPLE_PLATFORM64: String = get("ISABELLE_APPLE_PLATFORM64")
72349
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    82
80009
ac10e32938df clarified signature: more operations;
wenzelm
parents: 79562
diff changeset
    83
  def ISABELLE_PLATFORM(windows: Boolean = false, apple: Boolean = false): String =
ac10e32938df clarified signature: more operations;
wenzelm
parents: 79562
diff changeset
    84
    proper_string(if_proper(windows, ISABELLE_WINDOWS_PLATFORM64)) orElse
ac10e32938df clarified signature: more operations;
wenzelm
parents: 79562
diff changeset
    85
    proper_string(if_proper(apple, ISABELLE_APPLE_PLATFORM64)) orElse
ac10e32938df clarified signature: more operations;
wenzelm
parents: 79562
diff changeset
    86
    proper_string(ISABELLE_PLATFORM64) getOrElse error("Missing ISABELLE_PLATFORM64")
ac10e32938df clarified signature: more operations;
wenzelm
parents: 79562
diff changeset
    87
72349
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    88
  def is_arm: Boolean =
73667
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
    89
    ISABELLE_PLATFORM64.startsWith("arm64-") ||
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
    90
    ISABELLE_APPLE_PLATFORM64.startsWith("arm64-")
72349
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    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
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
   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
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
   102
  def arch_64_32: String = if (is_arm) "arm64_32" else "x86_64_32"
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
   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
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
   106
  override def toString: String = ISABELLE_PLATFORM_FAMILY
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
   107
}