src/Pure/System/isabelle_platform.scala
author wenzelm
Fri, 12 Sep 2025 17:31:38 +0200
changeset 83139 c87375585b9f
parent 83138 c66d77fb729e
permissions -rw-r--r--
more explicit python_exe;
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
83139
c87375585b9f more explicit python_exe;
wenzelm
parents: 83138
diff changeset
    10
import java.util.{Map => JMap}
c87375585b9f more explicit python_exe;
wenzelm
parents: 83138
diff changeset
    11
c87375585b9f more explicit python_exe;
wenzelm
parents: 83138
diff changeset
    12
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73716
diff changeset
    13
object Isabelle_Platform {
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    14
  val settings: List[String] =
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    15
    List(
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    16
      "ISABELLE_PLATFORM_FAMILY",
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    17
      "ISABELLE_PLATFORM64",
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    18
      "ISABELLE_WINDOWS_PLATFORM32",
73667
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
    19
      "ISABELLE_WINDOWS_PLATFORM64",
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
    20
      "ISABELLE_APPLE_PLATFORM64")
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    21
82717
8d42bf3b821d tuned signature: more operations;
wenzelm
parents: 82612
diff changeset
    22
  def make(env: Isabelle_System.Settings = Isabelle_System.Settings()): Isabelle_Platform =
8d42bf3b821d tuned signature: more operations;
wenzelm
parents: 82612
diff changeset
    23
    new Isabelle_Platform(settings.map(a => (a, Isabelle_System.getenv(a, env = env))))
8d42bf3b821d tuned signature: more operations;
wenzelm
parents: 82612
diff changeset
    24
8d42bf3b821d tuned signature: more operations;
wenzelm
parents: 82612
diff changeset
    25
  lazy val local: Isabelle_Platform = make()
82610
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    26
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    27
  def remote(ssh: SSH.Session): Isabelle_Platform = {
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    28
    val script =
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    29
      File.read(Path.explode("~~/lib/scripts/isabelle-platform")) + "\n" +
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    30
        settings.map(a => "echo \"" + Bash.string(a) + "=$" + Bash.string(a) + "\"").mkString("\n")
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    31
    val result = ssh.execute("bash -c " + Bash.string(script)).check
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    32
    new Isabelle_Platform(
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    33
      result.out_lines.map(line =>
3133f9748ea8 clarified signature;
wenzelm
parents: 80009
diff changeset
    34
        Properties.Eq.unapply(line) getOrElse error("Bad output: " + quote(result.out))))
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    35
  }
82612
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    36
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    37
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    38
  /* system context for progress/process */
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    39
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    40
  object Context {
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    41
    def apply(
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    42
      isabelle_platform: Isabelle_Platform = local,
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    43
      mingw: MinGW = MinGW.none,
83124
921ca143fd94 support Intel platform on Apple Silicon;
wenzelm
parents: 83111
diff changeset
    44
      apple: Boolean = true,
82612
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    45
      progress: Progress = new Progress
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    46
    ): Context = {
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    47
      val context_platform = isabelle_platform
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    48
      val context_mingw = mingw
83124
921ca143fd94 support Intel platform on Apple Silicon;
wenzelm
parents: 83111
diff changeset
    49
      val context_apple = apple
82612
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    50
      val context_progress = progress
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    51
      new Context {
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    52
        override def isabelle_platform: Isabelle_Platform = context_platform
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    53
        override def mingw: MinGW = context_mingw
83124
921ca143fd94 support Intel platform on Apple Silicon;
wenzelm
parents: 83111
diff changeset
    54
        override def apple: Boolean = context_apple
82612
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    55
        override def progress: Progress = context_progress
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    56
      }
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    57
    }
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    58
  }
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    59
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    60
  trait Context {
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    61
    def isabelle_platform: Isabelle_Platform
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    62
    def mingw: MinGW
83124
921ca143fd94 support Intel platform on Apple Silicon;
wenzelm
parents: 83111
diff changeset
    63
    def apple: Boolean
82612
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    64
    def progress: Progress
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    65
83124
921ca143fd94 support Intel platform on Apple Silicon;
wenzelm
parents: 83111
diff changeset
    66
    def ISABELLE_PLATFORM: String = isabelle_platform.ISABELLE_PLATFORM(windows = true, apple = apple)
921ca143fd94 support Intel platform on Apple Silicon;
wenzelm
parents: 83111
diff changeset
    67
    def is_linux_arm: Boolean = isabelle_platform.is_linux && isabelle_platform.is_arm
921ca143fd94 support Intel platform on Apple Silicon;
wenzelm
parents: 83111
diff changeset
    68
    def is_macos_arm: Boolean = isabelle_platform.is_macos && isabelle_platform.is_arm && apple
921ca143fd94 support Intel platform on Apple Silicon;
wenzelm
parents: 83111
diff changeset
    69
    def is_arm: Boolean = is_linux_arm || is_macos_arm
921ca143fd94 support Intel platform on Apple Silicon;
wenzelm
parents: 83111
diff changeset
    70
82612
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    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
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    73
83139
c87375585b9f more explicit python_exe;
wenzelm
parents: 83138
diff changeset
    74
    def bash(script: String,
c87375585b9f more explicit python_exe;
wenzelm
parents: 83138
diff changeset
    75
      cwd: Path = Path.current,
c87375585b9f more explicit python_exe;
wenzelm
parents: 83138
diff changeset
    76
      env: JMap[String, String] = Isabelle_System.Settings.env(),
c87375585b9f more explicit python_exe;
wenzelm
parents: 83138
diff changeset
    77
    ): Process_Result = {
83138
c66d77fb729e clarified signature: closer to regular bash();
wenzelm
parents: 83124
diff changeset
    78
      progress.bash(
83124
921ca143fd94 support Intel platform on Apple Silicon;
wenzelm
parents: 83111
diff changeset
    79
        if (is_macos_arm) "arch -arch arm64 bash -c " + Bash.string(script)
83138
c66d77fb729e clarified signature: closer to regular bash();
wenzelm
parents: 83124
diff changeset
    80
        else mingw.bash_script(script),
83139
c87375585b9f more explicit python_exe;
wenzelm
parents: 83138
diff changeset
    81
        cwd = cwd, env = env, echo = progress.verbose)
c87375585b9f more explicit python_exe;
wenzelm
parents: 83138
diff changeset
    82
    }
82612
2757f73abda7 clarified signature and modules;
wenzelm
parents: 82611
diff changeset
    83
  }
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    84
}
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    85
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73716
diff changeset
    86
class Isabelle_Platform private(val settings: List[(String, String)]) {
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    87
  private def get(name: String): String =
72339
626920749f5d tuned signature;
wenzelm
parents: 72338
diff changeset
    88
    settings.collectFirst({ case (a, b) if a == name => b }).
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    89
      getOrElse(error("Bad platform settings variable: " + quote(name)))
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    90
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    91
  val ISABELLE_PLATFORM64: String = get("ISABELLE_PLATFORM64")
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    92
  val ISABELLE_WINDOWS_PLATFORM64: String = get("ISABELLE_WINDOWS_PLATFORM64")
73667
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
    93
  val ISABELLE_APPLE_PLATFORM64: String = get("ISABELLE_APPLE_PLATFORM64")
72349
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    94
80009
ac10e32938df clarified signature: more operations;
wenzelm
parents: 79562
diff changeset
    95
  def ISABELLE_PLATFORM(windows: Boolean = false, apple: Boolean = false): String =
ac10e32938df clarified signature: more operations;
wenzelm
parents: 79562
diff changeset
    96
    proper_string(if_proper(windows, ISABELLE_WINDOWS_PLATFORM64)) orElse
ac10e32938df clarified signature: more operations;
wenzelm
parents: 79562
diff changeset
    97
    proper_string(if_proper(apple, ISABELLE_APPLE_PLATFORM64)) orElse
ac10e32938df clarified signature: more operations;
wenzelm
parents: 79562
diff changeset
    98
    proper_string(ISABELLE_PLATFORM64) getOrElse error("Missing ISABELLE_PLATFORM64")
ac10e32938df clarified signature: more operations;
wenzelm
parents: 79562
diff changeset
    99
72349
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
   100
  def is_arm: Boolean =
73667
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
   101
    ISABELLE_PLATFORM64.startsWith("arm64-") ||
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
   102
    ISABELLE_APPLE_PLATFORM64.startsWith("arm64-")
72349
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
   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
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
   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
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
   114
  def arch_64_32: String = if (is_arm) "arm64_32" else "x86_64_32"
442460fba2a4 clarified platforms;
wenzelm
parents: 72352
diff changeset
   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
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
   118
  override def toString: String = ISABELLE_PLATFORM_FAMILY
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
   119
}