# HG changeset patch # User wenzelm # Date 1620743424 -7200 # Node ID 7404f2e1d0926951fec2e184d9225bd8ca45d1fa # Parent 4121fc47432b70a071a849335703056dbeabe64c clarified platforms; diff -r 4121fc47432b -r 7404f2e1d092 NEWS --- 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) diff -r 4121fc47432b -r 7404f2e1d092 lib/scripts/isabelle-platform --- 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 diff -r 4121fc47432b -r 7404f2e1d092 src/Doc/System/Environment.thy --- 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>\$ISABELLE_HOME_USER/etc/settings\. \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\\<^sup>*\] is automatically set to the - general platform family: \<^verbatim>\linux\, \<^verbatim>\macos\, \<^verbatim>\windows\. Note that + general platform family (\<^verbatim>\linux\, \<^verbatim>\macos\, \<^verbatim>\windows\). 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}\\<^sup>*\, @{setting_def - ISABELLE_PLATFORM32}\\<^sup>*\] indicate the standard Posix platform: \<^verbatim>\x86_64\ - for 64 bit and \<^verbatim>\x86\ for 32 bit, together with a symbolic name for the - operating system (\<^verbatim>\linux\, \<^verbatim>\darwin\, \<^verbatim>\cygwin\). 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] \"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"\} - - In contrast, the subsequent expression prefers the old 32 bit variant (which - is only relevant for unusual applications): - - @{verbatim [display] \"${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}"\} + \<^descr>[@{setting_def ISABELLE_PLATFORM64}\\<^sup>*\] indicates the standard Posix + platform (\<^verbatim>\x86_64\, \<^verbatim>\arm64\), together with a symbolic name for the + operating system (\<^verbatim>\linux\, \<^verbatim>\darwin\, \<^verbatim>\cygwin\). \<^descr>[@{setting_def ISABELLE_WINDOWS_PLATFORM64}\\<^sup>*\, @{setting_def - ISABELLE_WINDOWS_PLATFORM32}\\<^sup>*\] 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}\\<^sup>*\] 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] \"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:- - ${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"\} + $ISABELLE_PLATFORM64}}"\} + + \<^descr>[@{setting_def ISABELLE_APPLE_PLATFORM64}\\<^sup>*\] indicates the native Apple + Silicon platform (\<^verbatim>\arm64-darwin\ if available), instead of Intel emulation + via Rosetta (\<^verbatim>\ISABELLE_PLATFORM64=x86_64-darwin\). \<^descr>[@{setting ISABELLE_TOOL}\\<^sup>*\] is automatically set to the full path name of the @{executable isabelle} executable. diff -r 4121fc47432b -r 7404f2e1d092 src/Pure/Admin/build_history.scala --- 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) diff -r 4121fc47432b -r 7404f2e1d092 src/Pure/System/isabelle_platform.scala --- 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", diff -r 4121fc47432b -r 7404f2e1d092 src/Pure/System/platform.scala --- 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") }