Admin/components/PLATFORMS

added lemmas reflclp_(less|greater)_eq[simp], rtranclp_(less|greater)_eq[simp], and tranclp_(less|greater|less_eq|greater_eq)[simp]

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!