--- a/Admin/components/README.md Mon Mar 25 17:46:16 2024 +0100
+++ b/Admin/components/README.md Mon Mar 25 19:56:12 2024 +0100
@@ -11,72 +11,99 @@
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).
+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 GNU `bash` and Isabelle/Scala as portable system
-infrastructure, using somewhat peculiar implementation techniques.
+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. More exotic
-platforms are unsupported: NixOS, BSD, Solaris.
+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.
-Official platforms:
+The official platforms, with base-line operating systems, and reference
+machines are as follows:
* `x86_64-linux`
- - Ubuntu 18.04 LTS
+ - **Ubuntu 18.04 LTS**
* `arm64-linux`
- - Ubuntu 18.04 LTS (e.g. via `docker run -it ubuntu:18.04 bash`)
+ - **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 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 (???)
+ - **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 10
+ - **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`)
+ - **Cygwin 3.5.x**
+ https://isabelle.sketis.net/cygwin_2024 (`x86_64/release`)
-### 64 bit vs. 32 bit platform personality ###
+### Multiple platform personalities ###
-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`.
+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 platform personality. On Windows this is for Cygwin64,
-but the following native platform identifiers are available as well:
+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`
- * `ISABELLE_WINDOWS_PLATFORM64`
- * `ISABELLE_WINDOWS_PLATFORM32`
+ * 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`
-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):
+ * 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}"`
-
-And this is for old 32 bit executables on Windows, but still 64 bit on Unix:
+ -- native Windows, or default POSIX platform (always Intel on macOS)
- * `"${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.
+ * `"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}"`
+ -- native Windows platform, native Apple Silicon platform, or default/native Linux platform
### Dependable system tools ###
@@ -89,26 +116,43 @@
* 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.
+ `/bin/dash` and causes many problems.
-### Known 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.
-* 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!
+* 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.
-## Notes on maintaining the Isabelle component repository at TUM ##
+## 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
@@ -128,7 +172,7 @@
### 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
+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
@@ -136,9 +180,10 @@
* `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.
+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
+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.
@@ -146,29 +191,46 @@
### 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/.
+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.
-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.
+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 `/home/isabelle/contrib/`. This allows
+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
-`isabelle_cronjob` does this routinely: it will break if the unpacked version
-is omitted.
+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.