| author | haftmann | 
| Tue, 02 May 2023 08:39:46 +0000 | |
| changeset 77927 | f041d5060892 | 
| parent 75393 | 87ebf5a50283 | 
| child 78610 | fd1fec53665b | 
| permissions | -rw-r--r-- | 
| 31825 | 1 | /* Title: Pure/System/platform.scala | 
| 2 | Author: Makarius | |
| 3 | ||
| 69112 | 4 | System platform identification. | 
| 31825 | 5 | */ | 
| 6 | ||
| 7 | package isabelle | |
| 8 | ||
| 31828 | 9 | |
| 75393 | 10 | object Platform {
 | 
| 69112 | 11 | /* platform family */ | 
| 31828 | 12 | |
| 73906 | 13 | val is_windows: Boolean = isabelle.setup.Environment.is_windows() | 
| 71383 | 14 |   val is_linux: Boolean = System.getProperty("os.name", "") == "Linux"
 | 
| 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: 
73193diff
changeset | 16 | val is_unix: Boolean = is_linux || is_macos | 
| 31825 | 17 | |
| 73637 | 18 |   def is_arm: Boolean = cpu_arch.startsWith("arm")
 | 
| 19 | ||
| 69410 | 20 | def family: Family.Value = | 
| 73637 | 21 | if (is_linux && is_arm) Family.linux_arm | 
| 22 | else if (is_linux) Family.linux | |
| 69410 | 23 | else if (is_macos) Family.macos | 
| 24 | else if (is_windows) Family.windows | |
| 25 |     else error("Failed to determine current platform family")
 | |
| 26 | ||
| 75393 | 27 |   object Family extends Enumeration {
 | 
| 73637 | 28 | val linux_arm, linux, macos, windows = Value | 
| 73642 | 29 | val list0: List[Value] = List(linux, windows, macos) | 
| 75212 | 30 | val list: List[Value] = List(linux, linux_arm, windows, macos) | 
| 69410 | 31 | |
| 32 | def unapply(name: String): Option[Value] = | |
| 33 |       try { Some(withName(name)) }
 | |
| 34 |       catch { case _: NoSuchElementException => None }
 | |
| 35 | ||
| 36 | def parse(name: String): Value = | |
| 37 |       unapply(name) getOrElse error("Bad platform family: " + quote(name))
 | |
| 73637 | 38 | |
| 39 | def standard(platform: Value): String = | |
| 40 | if (platform == linux_arm) "arm64-linux" | |
| 41 | else if (platform == linux) "x86_64-linux" | |
| 42 | else if (platform == macos) "x86_64-darwin" | |
| 43 | else if (platform == windows) "x86_64-cygwin" | |
| 73638 | 44 |       else error("Bad platform family: " + quote(platform.toString))
 | 
| 75083 | 45 | |
| 46 | def native(platform: Value): String = | |
| 47 | if (platform == macos) "arm64-darwin" | |
| 48 | else if (platform == windows) "x86_64-windows" | |
| 49 | else standard(platform) | |
| 69410 | 50 | } | 
| 51 | ||
| 31828 | 52 | |
| 69112 | 53 | /* platform identifiers */ | 
| 31828 | 54 | |
| 69112 | 55 | private val X86_64 = """amd64|x86_64""".r | 
| 72344 | 56 | private val Arm64 = """arm64|aarch64""".r | 
| 31825 | 57 | |
| 69726 | 58 | def cpu_arch: String = | 
| 59 |     System.getProperty("os.arch", "") match {
 | |
| 60 | case X86_64() => "x86_64" | |
| 72344 | 61 | case Arm64() => "arm64" | 
| 69726 | 62 |       case _ => error("Failed to determine CPU architecture")
 | 
| 63 | } | |
| 64 | ||
| 65 | def os_name: String = | |
| 66 |     family match {
 | |
| 73639 
e1432539df35
proper jvm_platform, notably for org.sqlite.lib.path;
 wenzelm parents: 
73638diff
changeset | 67 | case Family.linux_arm => "linux" | 
| 69726 | 68 | case Family.macos => "darwin" | 
| 69 | case _ => family.toString | |
| 70 | } | |
| 71 | ||
| 72 | lazy val jvm_platform: String = cpu_arch + "-" + os_name | |
| 31828 | 73 | |
| 74 | ||
| 61001 | 75 | /* JVM version */ | 
| 76 | ||
| 69112 | 77 | private val Version = """1\.(\d+)\.0_(\d+)""".r | 
| 71383 | 78 | lazy val jvm_version: String = | 
| 61001 | 79 |     System.getProperty("java.version") match {
 | 
| 80 | case Version(a, b) => a + "u" + b | |
| 81 | case a => a | |
| 82 | } | |
| 83 | ||
| 84 | ||
| 41381 | 85 | /* JVM name */ | 
| 86 | ||
| 53582 | 87 |   val jvm_name: String = System.getProperty("java.vm.name", "")
 | 
| 31825 | 88 | } |