# HG changeset patch # User desharna # Date 1711431158 -3600 # Node ID 9df291750cc06fe11905e6f6b99db4784d837b11 # Parent d8320c3a43ec2788cfae1108eb2e0ce9411d14c3# Parent e94a36467f4ee4be5da1eeabc206c7543903ca48 merged diff -r d8320c3a43ec -r 9df291750cc0 Admin/components/PLATFORMS --- 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! diff -r d8320c3a43ec -r 9df291750cc0 Admin/components/README --- 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). diff -r d8320c3a43ec -r 9df291750cc0 Admin/components/README.md --- /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. diff -r d8320c3a43ec -r 9df291750cc0 Admin/components/components.sha1 --- 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 diff -r d8320c3a43ec -r 9df291750cc0 Admin/components/main --- 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 diff -r d8320c3a43ec -r 9df291750cc0 NEWS --- 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) diff -r d8320c3a43ec -r 9df291750cc0 etc/settings --- 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" ### diff -r d8320c3a43ec -r 9df291750cc0 lib/scripts/isabelle-platform --- 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 diff -r d8320c3a43ec -r 9df291750cc0 src/Pure/Admin/component_stack.scala --- 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, diff -r d8320c3a43ec -r 9df291750cc0 src/Pure/Admin/isabelle_cronjob.scala --- 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",