--- a/Admin/components/PLATFORMS Mon Mar 25 19:27:53 2024 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-Multi-platform support of Isabelle
-==================================
-
-Preamble
---------
-
-The general programming model is that of a stylized ML + Scala + POSIX
-environment, with a minimum of system-specific code in user-space
-tools.
-
-The Isabelle system infrastructure provides some facilities to make
-this work, e.g. see the ML and Scala modules File and Path, or
-functions like Isabelle_System.bash. The settings environment also
-provides some means for portability, e.g. the bash function
-"platform_path" to keep the impression that Windows/Cygwin adheres to
-Isabelle/POSIX standards, although many executables are native on
-Windows (notably Poly/ML and Java).
-
-When producing add-on tools, it is important to stay within this clean
-room of Isabelle, and refrain from non-portable access to operating
-system functions. The Isabelle environment uses GNU bash and
-Isabelle/Scala as portable system infrastructure, using somewhat
-peculiar implementation techniques.
-
-
-Supported platforms
--------------------
-
-A broad range of hardware and operating system platforms are supported
-by building executables on base-line versions that are neither too old
-nor too new. Common OS families should work: Linux, macOS,
-Windows. More exotic platforms are unsupported: NixOS, BSD, Solaris.
-
-Official platforms:
-
- x86_64-linux Ubuntu 18.04 LTS
- arm64-linux Ubuntu 18.04 LTS (e.g. via "docker run -it ubuntu:18.04 bash")
-
- x86_64-darwin macOS 11 Big Sur (mini1 Macmini8,1)
- macOS 12 Monterey (???)
- macOS 13 Ventura (mini3 Mac14,12 -- MacMini M2 Pro, 6+4 cores)
- macOS 14 Sonoma (mini2 Macmini8,1)
-
- arm64-darwin macOS 11 Big Sur (assur Macmini9,1 -- MacMini M1, 4+4 cores)
- macOS 12 Monterey (???)
- macOS 13 Ventura (mini3 Mac14,12 -- MacMini M2 Pro, 6+4 cores)
- macOS 14 Sonoma (studio1 Mac13,2 M1 Ultra, 16+4 cores)
-
- x86_64-windows Windows 10
- x86_64-cygwin Cygwin 3.5.x https://isabelle.sketis.net/cygwin_2024 (x86_64/release)
-
-
-64 bit vs. 32 bit platform personality
---------------------------------------
-
-Isabelle requires 64 bit hardware running a 64 bit operating
-system. Only Windows still supports native x86 executables, but the
-POSIX emulation on Windows via Cygwin64 works exclusively for x86_64.
-
-The Isabelle settings environment provides variable
-ISABELLE_PLATFORM64 to refer to the standard platform personality. On
-Windows this is for Cygwin64, but the following native platform
-identifiers are available as well:
-
- ISABELLE_WINDOWS_PLATFORM64
- ISABELLE_WINDOWS_PLATFORM32
-
-These are always empty on Linux and macOS, and non-empty on
-Windows. For example, this is how to refer to native Windows and
-fall-back on Unix (always 64 bit):
-
- "${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}"
-
-And this is for old 32 bit executables on Windows, but still 64 bit on
-Unix:
-
- "${ISABELLE_WINDOWS_PLATFORM32:-$ISABELLE_PLATFORM64}"
-
-For Apple Silicon the native platform is "$ISABELLE_APPLE_PLATFORM64"
-(arm64-darwin), but thanks to Rosetta 2 "$ISABELLE_PLATFORM64"
-(x64_64-darwin) works routinely with fairly good performance.
-
-
-Dependable system tools
------------------------
-
-The following portable system tools can be taken for granted:
-
-* Scala on top of Java. Isabelle/Scala irons out many fine points of
- the Java platform to make it fully portable as described above.
-
-* GNU bash as uniform shell on all platforms. The POSIX "standard"
- shell /bin/sh does *not* work portably -- there are too many
- non-standard implementations of it. On Debian and Ubuntu /bin/sh is
- actually /bin/dash and introduces many oddities.
-
-
-Known problems
---------------
-
-* macOS: If Homebrew or MacPorts is installed, there is some danger
- that accidental references to its shared libraries are created
- (e.g. libgmp). Use otool -L to check if compiled binaries also work
- without MacPorts.
-
-* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are
- notoriously non-portable an should be avoided.
-
-* The traditional "uname" Unix tool only tells about its own
- executable format, not the underlying platform!
--- a/Admin/components/README Mon Mar 25 19:27:53 2024 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-Notes on maintaining the Isabelle component repository at TUM
-=============================================================
-
-Quick reference
----------------
-
- * local setup (and test) of component directory, e.g. in
-
- screwdriver-3.14/
-
- * packaging (with associated SHA1 digest), e.g.
-
- $ isabelle components_build screwdriver-3.14
-
- * publishing, e.g.
-
- $ isabelle components_build -P screwdriver-3.14.tar.gz
-
- * manual editing of Admin/components/main: screwdriver-3.14
-
-
-Unique names
-------------
-
-Component names are globally unique over time and space: names of
-published components are never re-used. If some component needs to be
-re-packaged, extra indices may be added to the official version number
-like this:
-
- screwdriver-3.14 #default packaging/publishing, no index
- screwdriver-3.14-1 #another refinement of the same
- screwdriver-3.14-2 #yet another refinement of the same
-
-There is no standard format for the structure of component names: they
-are compared for equality only, without any guess at an ordering.
-
-Components are registered in Admin/components/main (or similar) for
-use of that particular Isabelle repository version, subject to regular
-Mercurial history. This allows to bisect Isabelle versions with full
-record of the required components for testing.
-
-
-Authentic archives
-------------------
-
-Isabelle components are managed as authentic .tar.gz archives in
-/home/isabelle/components from where they are made publicly available
-on https://isabelle.in.tum.de/components/.
-
-Visibility on the HTTP server depends on local Unix file permission:
-nonfree components should omit "read" mode for the Unix group/other;
-regular components should be world-readable.
-
-The file `Admin/components/components.sha1` contains SHA1 identifiers
-within the Isabelle repository, for integrity checking of the archives
-that are exposed to the public file-system. The command-line tool
-`isabelle components_build` maintains these hash-keys automatically.
-
-
-Unpacked copy
--------------
-
-A second unpacked copy is provided in `/home/isabelle/contrib/`. This allows
-users and administrative services within the TUM network to activate arbitrary
-snapshots of the repository with all standard components being available,
-without extra copying or unpacking of the authentic archives. The
-isabelle_cronjob does this routinely: it will break if the unpacked version is
-omitted.
-
-The command-line tool `isabelle components_build -P` takes care of uploading
-the .tar.gz archive and unpacking it, unless it is a special component (e.g.
-for multiplatform application bundling).
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components/README.md Tue Mar 26 06:32:38 2024 +0100
@@ -0,0 +1,236 @@
+# Isabelle system components #
+
+## Multi-platform support of Isabelle ##
+
+### Preamble ###
+
+The general programming model is that of a stylized ML + Scala + POSIX
+environment, with a minimum of system-specific code in user-space tools.
+
+The Isabelle system infrastructure provides some facilities to make this work,
+e.g. see the ML and Scala modules `File` and `Path`, or functions like
+`Isabelle_System.bash`. The settings environment also provides some means for
+portability, e.g. the `bash` function `platform_path` to keep the impression
+that Windows/Cygwin adheres to Isabelle/POSIX standards, although most
+executables are running natively on Windows.
+
+When producing add-on tools, it is important to stay within this clean room of
+Isabelle, and refrain from non-portable access to operating system functions.
+The Isabelle environment uses Isabelle/Scala as portable system
+infrastructure, and Isabelle/ML refers to that for anything non-trivial.
+
+
+### Supported platforms ###
+
+A broad range of hardware and operating system platforms are supported by
+building executables on base-line versions that are neither too old nor too
+new. Common OS families should work: Linux, macOS, Windows. Exotic platforms
+are unsupported: NixOS, BSD, Solaris etc.
+
+The official platforms, with **base-line operating systems**, and reference
+machines are as follows:
+
+ * `x86_64-linux`
+ - **Ubuntu 18.04 LTS**
+ * `arm64-linux`
+ - **Ubuntu 18.04 LTS** (e.g. via `docker run -it ubuntu:18.04 bash`)
+
+ * `x86_64-darwin`
+ - **macOS 11 Big Sur** (`mini1` Macmini8,1)
+ - macOS 12 Monterey (untested)
+ - macOS 13 Ventura (`mini3` Mac14,12 -- MacMini M2 Pro, 6+4 cores)
+ - macOS 14 Sonoma (`mini2` Macmini8,1)
+ * `arm64-darwin`
+ - **macOS 11 Big Sur** (`assur` Macmini9,1 -- MacMini M1, 4+4 cores)
+ - macOS 12 Monterey (untested)
+ - macOS 13 Ventura (`mini3` Mac14,12 -- MacMini M2 Pro, 6+4 cores)
+ - macOS 14 Sonoma (`studio1` Mac13,2 M1 Ultra, 16+4 cores)
+
+ * `x86_64-windows`
+ - **Windows Server 2012 Rev 2** (`vmnipkow9`)
+ - **Windows 10**
+ - Windows 11
+ * `x86_64-cygwin`
+ - **Cygwin 3.5.x**
+ https://isabelle.sketis.net/cygwin_2024 (`x86_64/release`)
+
+
+### Multiple platform personalities ###
+
+Isabelle works with current 64 bit hardware and 64 bit operating systems,
+which usually means Intel (`x86_64`) and very often ARM (`arm64`). Windows and
+macOS provide `x86_64` emulation on their ARM versions, so that is in theory
+sufficient, but native `arm64` is more efficient. Linux lacks proper
+emulation, so tools should be provided for `x86_64-linux` and `arm64-linux`
+whenever possible. Also note that `arm64-linux` is the standard platform for
+Docker on ARM hardware (e.g. Apple Silicon).
+
+For extra performance on macOS, Isabelle tools are usually included in both
+variants: `x86_64-darwin` and `arm64-darwin` (or as hybrid executable that
+pretends to be `x86_64-darwin`, the default platform). Windows support is only
+for Intel so far: this could mean `x86_64-windows` or `x86_64-cygwin`, but
+also `x86-windows` for old binary-only tools.
+
+The Isabelle settings environment provides variable `ISABELLE_PLATFORM64` to
+refer to the standard POSIX platform personality (Linux/ARM, Linux/Intel,
+macOS/Intel, Windows/Cygwin64/Intel). Alternative settings are available for
+native platforms as show below. In summary, the symbolic platform names from
+the settings environment are as follows:
+
+ * Linux (Intel)
+ - `ISABELLE_PLATFORM64` is `x86_64-linux`
+
+ * Linux (ARM)
+ - `ISABELLE_PLATFORM64` is `arm64-linux`
+
+ * Windows
+ - `ISABELLE_PLATFORM64` is `x86_64-cygwin`
+ - `ISABELLE_WINDOWS_PLATFORM64` is `x86_64-windows`
+ - `ISABELLE_WINDOWS_PLATFORM32` is `x86-windows`
+
+ * macOS (Intel)
+ - `ISABELLE_PLATFORM64` is `x86_64-darwin`
+
+ * macOS (ARM)
+ - `ISABELLE_PLATFORM64` is `x86_64-darwin`
+ - `ISABELLE_APPLE_PLATFORM64` is `arm64-darwin`
+
+When used outside their proper system context, platform settings remain empty.
+This allows to refer symbolically to various combinations, using conditional
+expressions in GNU `bash` like this:
+
+ * `"${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}"`
+ -- native Windows, or default POSIX platform (always Intel on macOS)
+
+ * `"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}"`
+ -- native Windows platform, native Apple Silicon platform, or default/native Linux platform
+
+
+### Dependable system tools ###
+
+The following portable system tools can be taken for granted:
+
+* Scala on top of Java. Isabelle/Scala irons out many fine points of the Java
+ platform to make it fully portable as described above.
+
+* GNU `bash` as uniform shell on all platforms. The POSIX "standard" shell
+ `/bin/sh` does not work portably -- there are too many non-standard
+ implementations of it. On Debian and Ubuntu `/bin/sh` is actually
+ `/bin/dash` and causes many problems.
+
+
+### Common problems ###
+
+* The traditional `uname` Unix tool only tells about its own executable
+ format, not the underlying platform! There are special tricks to get
+ underlying platform details, depending on OS versions: Isabelle/Scala and
+ the Isabelle settings environment provide sanitized versions of that.
+ Isabelle tools should not attempt anything their own account.
+
+* Common Unix tools like `/bin/sh`, `/bin/kill`, `sed`, `ulimit` are
+ notoriously non-portable an should be avoided.
+
+* macOS: If Homebrew or MacPorts is installed, there is some danger that
+ accidental references to its shared libraries are created (e.g. `libgmp`).
+ Use `otool -L` to check if compiled binaries also work without MacPorts.
+
+* macOS as SSH server: The target user shell needs to be set to `/bin/bash`
+ instead of the default `/bin/zsh`, to make shell script escapes work
+ reliably.
+
+
+## The Isabelle component repository at TUM and sketis.net ##
+
+Isabelle repository versions and administrative tools download components via
+HTTPS from `ISABELLE_COMPONENT_REPOSITORY`, the default is
+`https://isabelle.sketis.net/components`, and alternative is
+`https://isabelle.in.tum.de/components`.
+
+Isabelle releases have all required components bundled, but additional
+components may be included via suitable manual configuration.
+
+
+### Quick reference ###
+
+The subsequent steps serve as a reminder of how to maintain components:
+
+ * local setup (and test) of component directory, e.g. in
+
+ - `screwdriver-3.14/`
+
+ * packaging (with associated SHA1 digest), e.g.
+
+ - `$ isabelle components_build screwdriver-3.14`
+
+ * publishing, e.g.
+
+ - `$ isabelle components_build -P screwdriver-3.14.tar.gz`
+
+ * manual editing of `Admin/components/main`: `screwdriver-3.14`
+
+
+### Unique names ###
+
+Component names are globally unique over time and space: names of published
+components are never re-used! If some component needs to be re-packaged, extra
+indices may be added to the official version number like this:
+
+ * `screwdriver-3.14` -- default packaging/publishing, no index
+ * `screwdriver-3.14-1` -- another refinement of the same
+ * `screwdriver-3.14-2` -- yet another refinement of the same
+
+There is no standard format for the structure of component names: they are
+compared for equality only, without any guess at an ordering (notions of
+"older", "newer", "better" etc. are irrelevant).
+
+Components are registered in `Admin/components/main` (or similar) for use of
+that particular Isabelle repository version, subject to regular Mercurial
+history. This allows to bisect Isabelle versions with full record of the
+required components for testing.
+
+
+### Authentic archives ###
+
+TUM provides the shared administrative directory `/p/home/isabelle/components`
+where the single source of all components is located as authentic `.tar.gz`
+archives. The file `Admin/components/components.sha1` contains SHA1
+identifiers within the Isabelle repository, for integrity checking of the
+archives that are exposed to the public file-system. The command-line tool
+`isabelle components_build` maintains these hash-keys automatically.
+
+Components are published on https://isabelle.sketis.net/components and
+https://isabelle.in.tum.de/components --- visibility on the web server depends
+on local Unix file permission: nonfree components should omit "read" mode for
+the Unix group/other; regular components should be world-readable.
+
+
+### Unpacked copy ###
+
+A second unpacked copy is provided in `/p/home/isabelle/contrib/`. This allows
+users and administrative services within the TUM network to activate arbitrary
+snapshots of the repository with all standard components being available,
+without extra copying or unpacking of the authentic archives.
+
+The command-line tool `isabelle components_build -P` takes care of uploading
+the `.tar.gz` archive and unpacking it, unless it is a special component (e.g.
+for multiplatform application bundling).
+
+
+### Repeatable component builds ###
+
+Historically, Isabelle components have often been assembled manually, packaged
+as `.tar.gz` and uploaded to the administrative directory. This model no
+longer fits the typical complexity of multi-platform tools.
+
+The current quality standard demands a separate tool in Isabelle/Scala, to
+build a component in a repeatable manner: e.g. see `isabelle component_jdk` or
+`isabelle component_e` with sources in `src/Pure/Admin`. Such tools often
+require a Unix platform (Linux or macOS), or the specific platform for which
+the target is built. In the latter case, the component build tool is run
+manually in each operating-system context, using the base-line versions
+specified above (e.g. via Docker); all results are assembled into one big
+`.tar.gz` archive.
+
+Multi-platform tools also require thorough testing on all platforms: base-line
+and latest versions. It "works for me on my system" is not sufficient for the
+general public.
--- a/Admin/components/components.sha1 Mon Mar 25 19:27:53 2024 +0100
+++ b/Admin/components/components.sha1 Tue Mar 26 06:32:38 2024 +0100
@@ -506,6 +506,7 @@
f969443705aa8619e93af5b34ea98d15cd7efaf1 stack-2.1.3.tar.gz
423df2c437f7cceac1d269da8e379507feb246ef stack-2.13.1.tar.gz
fdfea3b1c6b02612b1d50decb20b1a27ae741629 stack-2.15.1.tar.gz
+6fd65aac9147ba93fa3356fa629f6911d82d767b stack-2.15.3.tar.gz
ebd0221d038966aa8bde075f1b0189ff867b02ca stack-2.5.1.tar.gz
fa2d882ec45cbc8c7d2f3838b705a8316696dc66 stack-2.7.3.tar.gz
18437bc9abd5b95be31a96f7c15a85a3ebf466cf stack-2.9.3.tar.gz
--- a/Admin/components/main Mon Mar 25 19:27:53 2024 +0100
+++ b/Admin/components/main Tue Mar 26 06:32:38 2024 +0100
@@ -34,7 +34,7 @@
smbc-0.4.1
spass-3.8ds-2
sqlite-3.45.2.0
-stack-2.15.1
+stack-2.15.3
vampire-4.8
verit-2021.06.2-rmx-1
vscode_extension-20230206
--- a/NEWS Mon Mar 25 19:27:53 2024 +0100
+++ b/NEWS Tue Mar 26 06:32:38 2024 +0100
@@ -21,6 +21,7 @@
- Z3
- CVC4
+ - MLton
- Nunchaku + smbc (experimental)
--- a/etc/settings Mon Mar 25 19:27:53 2024 +0100
+++ b/etc/settings Tue Mar 26 06:32:38 2024 +0100
@@ -173,9 +173,9 @@
ISABELLE_STACK_ROOT="$USER_HOME/.stack"
-ISABELLE_STACK_RESOLVER="lts-22.6"
+ISABELLE_STACK_RESOLVER="lts-22.13"
-ISABELLE_GHC_VERSION="ghc-9.6.3"
+ISABELLE_GHC_VERSION="ghc-9.6.4"
###
--- a/lib/scripts/isabelle-platform Mon Mar 25 19:27:53 2024 +0100
+++ b/lib/scripts/isabelle-platform Tue Mar 26 06:32:38 2024 +0100
@@ -23,19 +23,12 @@
;;
Darwin)
ISABELLE_PLATFORM_FAMILY="macos"
- case $(sw_vers -productVersion) in
- 10.10*|10.11*|10.12*|10.13*|10.14*)
- ISABELLE_PLATFORM64=x86_64-darwin
+ ISABELLE_PLATFORM64=x86_64-darwin
+ case $(uname -a) in
+ *arm64*|*ARM64*)
+ ISABELLE_APPLE_PLATFORM64=arm64-darwin
;;
*)
- ISABELLE_PLATFORM64=x86_64-darwin
- case $(uname -a) in
- *arm64*|*ARM64*)
- ISABELLE_APPLE_PLATFORM64=arm64-darwin
- ;;
- *)
- ;;
- esac
;;
esac
;;
@@ -43,10 +36,6 @@
ISABELLE_PLATFORM_FAMILY="windows"
ISABELLE_WINDOWS_PLATFORM32="x86-windows"
ISABELLE_WINDOWS_PLATFORM64="x86_64-windows"
- case $(uname -m) in
- x86_64)
- ISABELLE_PLATFORM64=x86_64-cygwin
- ;;
- esac
+ ISABELLE_PLATFORM64=x86_64-cygwin
;;
esac
--- a/src/Pure/Admin/component_stack.scala Mon Mar 25 19:27:53 2024 +0100
+++ b/src/Pure/Admin/component_stack.scala Tue Mar 26 06:32:38 2024 +0100
@@ -29,7 +29,7 @@
/* build stack */
val default_url = "https://github.com/commercialhaskell/stack/releases/download"
- val default_version = "2.15.1"
+ val default_version = "2.15.3"
def build_stack(
base_url: String = default_url,
--- a/src/Pure/Admin/isabelle_cronjob.scala Mon Mar 25 19:27:53 2024 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Tue Mar 26 06:32:38 2024 +0100
@@ -335,14 +335,16 @@
" -e ISABELLE_SWIPL=/usr/local/bin/swipl",
args = "-a -d '~~/src/Benchmarks'")),
List(
- Remote_Build("macOS 14 Sonoma (ARM)", "studio1-sonoma",
+ Remote_Build("AFP (macOS 14 Sonoma, Apple Silicon)", "studio1-sonoma", history = 120,
history_base = "build_history_base_arm",
- options = "-m32 -B -M1x4,2x4,4x2,8 -p pide_session=false" +
+ java_heap = "8g",
+ options = "-m32 -M1x6 -p pide_session=false -t AFP" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
" -e ISABELLE_SWIPL=/opt/homebrew/bin/swipl",
- args = "-a -d '~~/src/Benchmarks'",
- count = () => 2)),
+ args = "-a -d '~~/src/Benchmarks' -X large -X slow",
+ afp = true,
+ detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"))),
List(
Remote_Build("macOS, quick_and_dirty", "mini2",
options = "-m32 -M4 -t quick_and_dirty -p pide_session=false",