diff --git a/Admin/PLATFORMS b/Admin/PLATFORMS --- a/Admin/PLATFORMS +++ b/Admin/PLATFORMS @@ -1,115 +1,115 @@ 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 Poly/ML and the JVM are native 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 peculiar scripts for GNU bash and perl as system glue: this style should be observed as far as possible. 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 work: Linux, Windows, macOS, but exotic ones are unsupported: BSD, Solaris, NixOS. Official (full support): x86_64-linux Ubuntu 14.04 LTS x86_64-darwin macOS 10.13 High Sierra (lapbroy68 MacBookPro11,2) macOS 10.14 Mojave (mini2 Macmini8,1) macOS 10.15 Catalina (laramac01 Macmini8,1) - macOS 11.1 Big Sur (mini2 Macmini8,1) + macOS 11.1 Big Sur (mini1 Macmini8,1) x86_64-windows Windows 10 x86_64-cygwin Cygwin 3.1.x https://isabelle.sketis.net/cygwin_2021 (x86_64/release) New (experimental): arm64-linux Raspberry Pi OS 64bit beta (Debian 10 / Buster) arm64-darwin macOS 11.1 Big Sur 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}" Dependable system tools ----------------------- The following portable system tools can be taken for granted: * Scala on top of Java. Isabelle/Scala irons out many oddities and portability issues of the Java platform. * 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. * Perl as largely portable system programming language, with its fairly robust support for processes, signals, sockets etc. Known problems -------------- * macOS: If 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: If MacPorts is installed and its version of Perl takes precedence over /usr/bin/perl in the PATH, then the end-user needs to take care of installing extra modules, e.g. for HTTP support. Such add-ons are usually included in Apple's /usr/bin/perl by default. * 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!