Admin/components/PLATFORMS

prefer system option;

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 16.04 LTS

  x86_64-darwin     macOS 10.13 High Sierra (lapbroy68 MacBookPro11,2)
                    macOS 10.14 Mojave (mini2 Macmini8,1)
                    macOS 10.15 Catalina (???)
                    macOS 11 Big Sur (mini1 Macmini8,1)
                    macOS 12 Monterey (laramac01 Macmini8,1)
                    macOS 13 Ventura (mini3 Mac14,12 -- MacMini M2)

  arm64-darwin      macOS 11 Big Sur (assur Macmini9,1 -- MacMini M1)
                    macOS 12 Monterey (???)
                    macOS 13 Ventura (mini3 Mac14,12 -- MacMini M2)

  x86_64-windows    Windows 10
  x86_64-cygwin     Cygwin 3.3.x https://isabelle.sketis.net/cygwin_2022 (x86_64/release)

Experimental platforms:

  arm64-linux       Raspberry Pi OS 64bit beta (Debian 10 / Buster)


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!