src/Pure/System/isabelle_platform.scala
author wenzelm
Wed, 10 Feb 2021 22:30:51 +0100
changeset 73246 b9c480878663
parent 72352 f4bd6f123fdf
child 73667 442460fba2a4
permissions -rw-r--r--
tuned comments;
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
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
     4
General hardware and operating system type for Isabelle system tools.
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
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    10
object Isabelle_Platform
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    11
{
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    12
  val settings: List[String] =
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    13
    List(
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    14
      "ISABELLE_PLATFORM_FAMILY",
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    15
      "ISABELLE_PLATFORM32",
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    16
      "ISABELLE_PLATFORM64",
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    17
      "ISABELLE_WINDOWS_PLATFORM32",
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    18
      "ISABELLE_WINDOWS_PLATFORM64")
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    19
72340
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    20
  def apply(ssh: Option[SSH.Session] = None): Isabelle_Platform =
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    21
  {
72340
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    22
    ssh match {
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    23
      case None =>
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    24
        new Isabelle_Platform(settings.map(a => (a, Isabelle_System.getenv(a))))
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    25
      case Some(ssh) =>
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    26
        val script =
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    27
          File.read(Path.explode("~~/lib/scripts/isabelle-platform")) + "\n" +
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    28
            settings.map(a => "echo \"" + Bash.string(a) + "=$" + Bash.string(a) + "\"").mkString("\n")
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    29
        val result = ssh.execute("bash -c " + Bash.string(script)).check
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    30
        new Isabelle_Platform(
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    31
          result.out_lines.map(line =>
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    32
            space_explode('=', line) match {
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    33
              case List(a, b) => (a, b)
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    34
              case _ => error("Bad output: " + quote(result.out))
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    35
            }))
676066aa4798 clarified signature;
wenzelm
parents: 72339
diff changeset
    36
    }
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    37
  }
72349
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    38
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    39
  lazy val self: Isabelle_Platform = apply()
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    40
}
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    41
72339
626920749f5d tuned signature;
wenzelm
parents: 72338
diff changeset
    42
class Isabelle_Platform private(val settings: List[(String, String)])
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    43
{
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    44
  private def get(name: String): String =
72339
626920749f5d tuned signature;
wenzelm
parents: 72338
diff changeset
    45
    settings.collectFirst({ case (a, b) if a == name => b }).
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    46
      getOrElse(error("Bad platform settings variable: " + quote(name)))
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    47
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    48
  val ISABELLE_PLATFORM_FAMILY: String = get("ISABELLE_PLATFORM_FAMILY")
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    49
  val ISABELLE_PLATFORM32: String = get("ISABELLE_PLATFORM32")
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    50
  val ISABELLE_PLATFORM64: String = get("ISABELLE_PLATFORM64")
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    51
  val ISABELLE_WINDOWS_PLATFORM32: String = get("ISABELLE_WINDOWS_PLATFORM32")
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    52
  val ISABELLE_WINDOWS_PLATFORM64: String = get("ISABELLE_WINDOWS_PLATFORM64")
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    53
72349
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    54
  def is_intel: Boolean =
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    55
    ISABELLE_PLATFORM32.startsWith("x86-") ||
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    56
    ISABELLE_PLATFORM64.startsWith("x86_64-")
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    57
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    58
  def is_arm: Boolean =
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    59
    ISABELLE_PLATFORM32.startsWith("arm32-") ||
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    60
    ISABELLE_PLATFORM64.startsWith("arm64-")
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    61
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    62
  def is_linux: Boolean = ISABELLE_PLATFORM_FAMILY == "linux"
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    63
  def is_macos: Boolean = ISABELLE_PLATFORM_FAMILY == "macos"
e7284278796b clarified signature;
wenzelm
parents: 72340
diff changeset
    64
  def is_windows: Boolean = ISABELLE_PLATFORM_FAMILY == "windows"
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    65
72352
f4bd6f123fdf more systematic platform support, including arm64-linux;
wenzelm
parents: 72349
diff changeset
    66
  def arch_32: String = if (is_arm) "arm32" else "x86"
f4bd6f123fdf more systematic platform support, including arm64-linux;
wenzelm
parents: 72349
diff changeset
    67
  def arch_64: String = if (is_arm) "arm64" else "x86_64"
f4bd6f123fdf more systematic platform support, including arm64-linux;
wenzelm
parents: 72349
diff changeset
    68
  def os_name: String = if (is_macos) "darwin" else ISABELLE_PLATFORM_FAMILY
f4bd6f123fdf more systematic platform support, including arm64-linux;
wenzelm
parents: 72349
diff changeset
    69
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    70
  override def toString: String = ISABELLE_PLATFORM_FAMILY
54871a086193 formal platform information, notably for ssh;
wenzelm
parents:
diff changeset
    71
}