clarified platforms;
authorwenzelm
Tue, 11 May 2021 16:30:24 +0200
changeset 73928 7404f2e1d092
parent 73926 4121fc47432b
child 73929 70d3c7009a65
clarified platforms;
NEWS
lib/scripts/isabelle-platform
src/Doc/System/Environment.thy
src/Pure/Admin/build_history.scala
src/Pure/System/isabelle_platform.scala
src/Pure/System/platform.scala
--- a/NEWS	Tue May 11 14:04:36 2021 +0200
+++ b/NEWS	Tue May 11 16:30:24 2021 +0200
@@ -173,6 +173,12 @@
 * Command-line tool "isabelle version" supports repository archives
 (without full .hg directory). More options.
 
+* Obsolete settings variable ISABELLE_PLATFORM32 has been discontinued.
+Note that only Windows supports old 32 bit executables, via settings
+variable ISABELLE_WINDOWS_PLATFORM32. Everything else should be
+ISABELLE_PLATFORM64 (generic Posix) or ISABELLE_WINDOWS_PLATFORM64
+(native Windows) or ISABELLE_APPLE_PLATFORM64 (Apple Silicon).
+
 
 
 New in Isabelle2021 (February 2021)
--- a/lib/scripts/isabelle-platform	Tue May 11 14:04:36 2021 +0200
+++ b/lib/scripts/isabelle-platform	Tue May 11 16:30:24 2021 +0200
@@ -4,7 +4,6 @@
 #
 
 ISABELLE_PLATFORM_FAMILY=""
-ISABELLE_PLATFORM32=""
 ISABELLE_PLATFORM64=""
 ISABELLE_APPLE_PLATFORM64=""
 ISABELLE_WINDOWS_PLATFORM32=""
@@ -17,11 +16,7 @@
       aarch64)
         ISABELLE_PLATFORM64=arm64-linux
         ;;
-      arm*)
-        ISABELLE_PLATFORM32=arm32-linux
-        ;;
       *)
-        ISABELLE_PLATFORM32=x86-linux
         ISABELLE_PLATFORM64=x86_64-linux
         ;;
     esac
@@ -30,7 +25,6 @@
     ISABELLE_PLATFORM_FAMILY="macos"
     case $(sw_vers -productVersion) in
       10.10*|10.11*|10.12*|10.13*|10.14*)
-        ISABELLE_PLATFORM32=x86-darwin
         ISABELLE_PLATFORM64=x86_64-darwin
         ;;
       *)
@@ -53,9 +47,6 @@
       x86_64)
         ISABELLE_PLATFORM64=x86_64-cygwin
         ;;
-      i?86)
-        ISABELLE_PLATFORM32=x86-cygwin
-        ;;
     esac
     ;;
 esac
--- a/src/Doc/System/Environment.thy	Tue May 11 14:04:36 2021 +0200
+++ b/src/Doc/System/Environment.thy	Tue May 11 16:30:24 2021 +0200
@@ -110,39 +110,28 @@
   defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.
 
   \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the
-  general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
+  general platform family (\<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>). Note that
   platform-dependent tools usually need to refer to the more specific
   identification according to @{setting ISABELLE_PLATFORM64}, @{setting
-  ISABELLE_PLATFORM32}, @{setting ISABELLE_WINDOWS_PLATFORM64}, @{setting
-  ISABELLE_WINDOWS_PLATFORM32}.
-
-  \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>, @{setting_def
-  ISABELLE_PLATFORM32}\<open>\<^sup>*\<close>] indicate the standard Posix platform: \<^verbatim>\<open>x86_64\<close>
-  for 64 bit and \<^verbatim>\<open>x86\<close> for 32 bit, together with a symbolic name for the
-  operating system (\<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>darwin\<close>, \<^verbatim>\<open>cygwin\<close>). All platforms support 64
-  bit executables, some platforms also support 32 bit executables.
+  ISABELLE_WINDOWS_PLATFORM64}, @{setting ISABELLE_APPLE_PLATFORM64}.
 
-  In GNU bash scripts, it is possible to use the following expressions (with
-  quotes) to specify a preference of 64 bit over 32 bit:
-
-  @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"\<close>}
-
-  In contrast, the subsequent expression prefers the old 32 bit variant (which
-  is only relevant for unusual applications):
-
-  @{verbatim [display] \<open>"${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}"\<close>}
+  \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] indicates the standard Posix
+  platform (\<^verbatim>\<open>x86_64\<close>, \<^verbatim>\<open>arm64\<close>), together with a symbolic name for the
+  operating system (\<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>darwin\<close>, \<^verbatim>\<open>cygwin\<close>).
 
   \<^descr>[@{setting_def ISABELLE_WINDOWS_PLATFORM64}\<open>\<^sup>*\<close>, @{setting_def
-  ISABELLE_WINDOWS_PLATFORM32}\<open>\<^sup>*\<close>] indicate the native Windows platform.
-  These settings are analogous (but independent) of those for the standard
-  Posix subsystem: @{setting ISABELLE_PLATFORM64}, @{setting
-  ISABELLE_PLATFORM32}.
+  ISABELLE_WINDOWS_PLATFORM32}\<open>\<^sup>*\<close>] indicate the native Windows platform: both
+  64\,bit and 32\,bit executables are supported here.
 
   In GNU bash scripts, a preference for native Windows platform variants may
   be specified like this (first 64 bit, second 32 bit):
 
   @{verbatim [display] \<open>"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-
-  ${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"\<close>}
+  $ISABELLE_PLATFORM64}}"\<close>}
+
+  \<^descr>[@{setting_def ISABELLE_APPLE_PLATFORM64}\<open>\<^sup>*\<close>] indicates the native Apple
+  Silicon platform (\<^verbatim>\<open>arm64-darwin\<close> if available), instead of Intel emulation
+  via Rosetta (\<^verbatim>\<open>ISABELLE_PLATFORM64=x86_64-darwin\<close>).
 
   \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
   of the @{executable isabelle} executable.
--- a/src/Pure/Admin/build_history.scala	Tue May 11 14:04:36 2021 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue May 11 16:30:24 2021 +0200
@@ -27,6 +27,7 @@
   {
     val (ml_platform, ml_settings) =
     {
+      val cygwin_32 = "x86-cygwin"
       val windows_32 = "x86-windows"
       val windows_64 = "x86_64-windows"
       val windows_64_32 = "x86_64_32-windows"
@@ -52,8 +53,9 @@
         }
         else if (Platform.is_windows && !arch_64) {
           if (check_dir(windows_64_32)) windows_64_32
+          else if (check_dir(cygwin_32)) cygwin_32
           else if (check_dir(windows_32)) windows_32
-          else platform_32  // x86-cygwin
+          else err(windows_32)
         }
         else if (arch_64) {
           if (check_dir(platform_64)) platform_64 else err(platform_64)
--- a/src/Pure/System/isabelle_platform.scala	Tue May 11 14:04:36 2021 +0200
+++ b/src/Pure/System/isabelle_platform.scala	Tue May 11 16:30:24 2021 +0200
@@ -12,7 +12,6 @@
   val settings: List[String] =
     List(
       "ISABELLE_PLATFORM_FAMILY",
-      "ISABELLE_PLATFORM32",
       "ISABELLE_PLATFORM64",
       "ISABELLE_WINDOWS_PLATFORM32",
       "ISABELLE_WINDOWS_PLATFORM64",
--- a/src/Pure/System/platform.scala	Tue May 11 14:04:36 2021 +0200
+++ b/src/Pure/System/platform.scala	Tue May 11 16:30:24 2021 +0200
@@ -49,17 +49,13 @@
 
   /* platform identifiers */
 
-  private val X86 = """i.86|x86""".r
   private val X86_64 = """amd64|x86_64""".r
   private val Arm64 = """arm64|aarch64""".r
-  private val Arm32 = """arm""".r
 
   def cpu_arch: String =
     System.getProperty("os.arch", "") match {
-      case X86() => "x86"
       case X86_64() => "x86_64"
       case Arm64() => "arm64"
-      case Arm32() => "arm32"
       case _ => error("Failed to determine CPU architecture")
     }