src/Pure/System/platform.scala
author wenzelm
Sat, 27 Jan 2024 22:15:40 +0100
changeset 79536 d39976404aa7
parent 78610 fd1fec53665b
child 79981 bdea4eccd8d5
permissions -rw-r--r--
routine build + test for linux_arm;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/platform.scala
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     3
69112
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
     4
System platform identification.
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     5
*/
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     6
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     7
package isabelle
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
     8
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
     9
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75212
diff changeset
    10
object Platform {
69112
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
    11
  /* platform family */
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    12
73906
f627ffab387b support for Isabelle setup in pure Java;
wenzelm
parents: 73904
diff changeset
    13
  val is_windows: Boolean = isabelle.setup.Environment.is_windows()
71383
8313dca6dee9 misc tuning, following hint by IntelliJ;
wenzelm
parents: 69726
diff changeset
    14
  val is_linux: Boolean = System.getProperty("os.name", "") == "Linux"
8313dca6dee9 misc tuning, following hint by IntelliJ;
wenzelm
parents: 69726
diff changeset
    15
  val is_macos: Boolean = System.getProperty("os.name", "") == "Mac OS X"
73602
37243ad3ecb6 fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
wenzelm
parents: 73193
diff changeset
    16
  val is_unix: Boolean = is_linux || is_macos
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    17
73637
f3a356c64193 support for platform family "linux_arm";
wenzelm
parents: 73602
diff changeset
    18
  def is_arm: Boolean = cpu_arch.startsWith("arm")
f3a356c64193 support for platform family "linux_arm";
wenzelm
parents: 73602
diff changeset
    19
78610
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    20
  def family: Family =
73637
f3a356c64193 support for platform family "linux_arm";
wenzelm
parents: 73602
diff changeset
    21
    if (is_linux && is_arm) Family.linux_arm
f3a356c64193 support for platform family "linux_arm";
wenzelm
parents: 73602
diff changeset
    22
    else if (is_linux) Family.linux
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    23
    else if (is_macos) Family.macos
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    24
    else if (is_windows) Family.windows
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    25
    else error("Failed to determine current platform family")
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    26
78610
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    27
  object Family {
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    28
    val list: List[Family] = List(Family.linux, Family.linux_arm, Family.windows, Family.macos)
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    29
78610
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    30
    def unapply(name: String): Option[Family] =
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    31
      try { Some(Family.valueOf(name)) }
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    32
      catch { case _: IllegalArgumentException => None }
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    33
78610
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    34
    def parse(name: String): Family =
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    35
      unapply(name) getOrElse error("Bad platform family: " + quote(name))
73637
f3a356c64193 support for platform family "linux_arm";
wenzelm
parents: 73602
diff changeset
    36
78610
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    37
    val standard: Family => String =
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    38
      {
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    39
        case Family.linux_arm => "arm64-linux"
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    40
        case Family.linux => "x86_64-linux"
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    41
        case Family.macos => "x86_64-darwin"
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    42
        case Family.windows => "x86_64-cygwin"
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    43
      }
75083
35a5c4b16024 setup VSCode from VSCodium distribution;
wenzelm
parents: 73906
diff changeset
    44
78610
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    45
    val native: Family => String =
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    46
      {
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    47
        case Family.macos => "arm64-darwin"
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    48
        case Family.windows => "x86_64-windows"
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    49
        case platform => standard(platform)
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    50
      }
69410
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    51
  }
c071fcec4323 more explicit Platform.Family;
wenzelm
parents: 69112
diff changeset
    52
78610
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    53
  enum Family { case linux_arm, linux, macos, windows }
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 75393
diff changeset
    54
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    55
69112
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
    56
  /* platform identifiers */
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    57
69112
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
    58
  private val X86_64 = """amd64|x86_64""".r
72344
728da67527b9 detect arm64-linux platform;
wenzelm
parents: 72250
diff changeset
    59
  private val Arm64 = """arm64|aarch64""".r
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    60
69726
461f0615faa3 clarified signature;
wenzelm
parents: 69410
diff changeset
    61
  def cpu_arch: String =
461f0615faa3 clarified signature;
wenzelm
parents: 69410
diff changeset
    62
    System.getProperty("os.arch", "") match {
461f0615faa3 clarified signature;
wenzelm
parents: 69410
diff changeset
    63
      case X86_64() => "x86_64"
72344
728da67527b9 detect arm64-linux platform;
wenzelm
parents: 72250
diff changeset
    64
      case Arm64() => "arm64"
69726
461f0615faa3 clarified signature;
wenzelm
parents: 69410
diff changeset
    65
      case _ => error("Failed to determine CPU architecture")
461f0615faa3 clarified signature;
wenzelm
parents: 69410
diff changeset
    66
    }
461f0615faa3 clarified signature;
wenzelm
parents: 69410
diff changeset
    67
461f0615faa3 clarified signature;
wenzelm
parents: 69410
diff changeset
    68
  def os_name: String =
461f0615faa3 clarified signature;
wenzelm
parents: 69410
diff changeset
    69
    family match {
73639
e1432539df35 proper jvm_platform, notably for org.sqlite.lib.path;
wenzelm
parents: 73638
diff changeset
    70
      case Family.linux_arm => "linux"
69726
461f0615faa3 clarified signature;
wenzelm
parents: 69410
diff changeset
    71
      case Family.macos => "darwin"
461f0615faa3 clarified signature;
wenzelm
parents: 69410
diff changeset
    72
      case _ => family.toString
461f0615faa3 clarified signature;
wenzelm
parents: 69410
diff changeset
    73
    }
461f0615faa3 clarified signature;
wenzelm
parents: 69410
diff changeset
    74
461f0615faa3 clarified signature;
wenzelm
parents: 69410
diff changeset
    75
  lazy val jvm_platform: String = cpu_arch + "-" + os_name
31828
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    76
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31825
diff changeset
    77
61001
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    78
  /* JVM version */
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    79
69112
5b749aa452c6 misc tuning and modernization;
wenzelm
parents: 64493
diff changeset
    80
  private val Version = """1\.(\d+)\.0_(\d+)""".r
71383
8313dca6dee9 misc tuning, following hint by IntelliJ;
wenzelm
parents: 69726
diff changeset
    81
  lazy val jvm_version: String =
61001
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    82
    System.getProperty("java.version") match {
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    83
      case Version(a, b) => a + "u" + b
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    84
      case a => a
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    85
    }
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    86
ea38a1922a0b more version information;
wenzelm
parents: 55618
diff changeset
    87
41381
77990a6cd558 more explicit jvm_name;
wenzelm
parents: 36786
diff changeset
    88
  /* JVM name */
77990a6cd558 more explicit jvm_name;
wenzelm
parents: 36786
diff changeset
    89
53582
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 51617
diff changeset
    90
  val jvm_name: String = System.getProperty("java.vm.name", "")
31825
d47a9dc1f064 moved platform identification to platform.scala;
wenzelm
parents:
diff changeset
    91
}