# HG changeset patch
# User wenzelm
# Date 1601562682 -7200
# Node ID f4bd6f123fdfe63a20f0549e954ec2c060c932e0
# Parent  68902f8a1ef072819049959ea74e06b8b6f1ef42
more systematic platform support, including arm64-linux;

diff -r 68902f8a1ef0 -r f4bd6f123fdf src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Thu Oct 01 15:56:34 2020 +0200
+++ b/src/Pure/Admin/build_polyml.scala	Thu Oct 01 16:31:22 2020 +0200
@@ -57,25 +57,28 @@
     if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
       error("Bad Poly/ML root directory: " + root)
 
-    val platform_arch = if (arch_64) "x86_64" else "x86_64_32"
-    val platform_os = Platform.os_name
+    val platform = Isabelle_Platform.self
+    val platform_arch =
+      if (arch_64) platform.arch_64
+      else if (platform.is_intel) "x86_64_32"
+      else platform.arch_32
 
-    val platform = platform_arch + "-" + platform_os
-    val platform_64 = "x86_64-" + platform_os
+    val polyml_platform = platform_arch + "-" + platform.os_name
+    val sha1_platform = platform.arch_64 + "-" + platform.os_name
 
     val info =
-      platform_info.getOrElse(platform_os,
-        error("Bad OS platform: " + quote(platform_os)))
+      platform_info.getOrElse(platform.os_name,
+        error("Bad OS platform: " + quote(platform.os_name)))
 
     val settings =
       msys_root match {
-        case None if Platform.is_windows =>
+        case None if platform.is_windows =>
           error("Windows requires specification of msys root directory")
         case None => Isabelle_System.settings()
         case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode)
       }
 
-    if (Platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) {
+    if (platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) {
       error("""Missing "chrpath" executable on Linux""")
     }
 
@@ -128,9 +131,9 @@
     val sha1_files =
       if (sha1_root.isDefined) {
         val dir1 = sha1_root.get
-        bash(dir1, "./build " + platform_64, redirect = true, echo = true).check
+        bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check
 
-        val dir2 = dir1 + Path.explode(platform_64)
+        val dir2 = dir1 + Path.explode(sha1_platform)
         File.read_dir(dir2).map(entry => dir2.implode + "/" + entry)
       }
       else Nil
@@ -138,7 +141,7 @@
 
     /* target */
 
-    val target = Path.explode(platform)
+    val target = Path.explode(polyml_platform)
     Isabelle_System.rm_tree(target)
     Isabelle_System.mkdirs(target)
 
@@ -154,10 +157,10 @@
 
     /* poly: library path */
 
-    if (Platform.is_linux) {
+    if (platform.is_linux) {
       bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check
     }
-    else if (Platform.is_macos) {
+    else if (platform.is_macos) {
       for (file <- ldd_files) {
         bash(target,
           """install_name_tool -change """ + Bash.string(file) + " " +
@@ -257,7 +260,7 @@
     Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
     {
       var msys_root: Option[Path] = None
-      var arch_64 = false
+      var arch_64 = Isabelle_Platform.self.is_arm
       var sha1_root: Option[Path] = None
 
       val getopts = Getopts("""
@@ -265,7 +268,8 @@
 
   Options are:
     -M DIR       msys root directory (for Windows)
-    -m ARCH      processor architecture (32=x86_64_32, 64=x86_64, default: 32)
+    -m ARCH      processor architecture (32 or 64, default: """ +
+        (if (arch_64) "64" else "32") + """)
     -s DIR       sha1 sources, see https://isabelle.sketis.net/repos/sha1
 
   Build Poly/ML in the ROOT directory of its sources, with additional
@@ -274,8 +278,8 @@
         "M:" -> (arg => msys_root = Some(Path.explode(arg))),
         "m:" ->
           {
-            case "32" | "x86_64_32" => arch_64 = false
-            case "64" | "x86_64" => arch_64 = true
+            case "32" => arch_64 = false
+            case "64" => arch_64 = true
             case bad => error("Bad processor architecture: " + quote(bad))
           },
         "s:" -> (arg => sha1_root = Some(Path.explode(arg))))
diff -r 68902f8a1ef0 -r f4bd6f123fdf src/Pure/System/isabelle_platform.scala
--- a/src/Pure/System/isabelle_platform.scala	Thu Oct 01 15:56:34 2020 +0200
+++ b/src/Pure/System/isabelle_platform.scala	Thu Oct 01 16:31:22 2020 +0200
@@ -63,5 +63,9 @@
   def is_macos: Boolean = ISABELLE_PLATFORM_FAMILY == "macos"
   def is_windows: Boolean = ISABELLE_PLATFORM_FAMILY == "windows"
 
+  def arch_32: String = if (is_arm) "arm32" else "x86"
+  def arch_64: String = if (is_arm) "arm64" else "x86_64"
+  def os_name: String = if (is_macos) "darwin" else ISABELLE_PLATFORM_FAMILY
+
   override def toString: String = ISABELLE_PLATFORM_FAMILY
 }