more uniform directory layout for macOS;
uniform Isabelle_app executable + lib/scripts/Isabelle_app for Linux and macOS;
proper support for Apple "Files and Folders" security via x86_64-darwin executable (which is still able to launch arm64-darwin Java);
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
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!