Admin/PLATFORMS

generalized simproc

Multi-platform support of Isabelle
==================================

Preamble
--------

The general programming model is that of a stylized ML + Scala + POSIX
environment, with as little system-specific code in user-space tools
as possible.

The basic 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 overly ambitious system hacking.
The existing Isabelle bash scripts follow a peculiar style that
reflects long years of experience in getting system plumbing right.


Supported platforms
-------------------

The following hardware and operating system platforms are officially
supported by the Isabelle distribution (and bundled tools), with the
following base-line versions (which have been selected to be neither
too old nor too new):

  x86-linux         Ubuntu 12.04 LTS
  x86_64-linux      Ubuntu 12.04 LTS

  x86_64-darwin     Mac OS X 10.9 Mavericks (macbroy2 MacPro4,1)
                    Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2)
                    Mac OS X 10.11 El Capitan (?)
                    macOS 10.12 Sierra (macbroy30 MacBookPro6,2)

  x86-windows       Windows 7
  x86_64-windows    Windows 7
  x86_64-cygwin     Cygwin 2.8 http://isabelle.in.tum.de/cygwin_2017 (x86_64/release)

All of the above platforms are 100% supported by Isabelle -- end-users
should not have to care about the differences (at least in theory).

Fringe platforms like BSD or Solaris are not supported.


32 bit vs. 64 bit platforms
---------------------------

Most users have 64 bit hardware and are running a 64 bit operating
system by default.  For Linux this usually means missing 32 bit shared
libraries, so native x86_64-linux needs to be used by default, despite
its doubled space requirements for Poly/ML heaps.  For Mac OS X, the
x86-darwin personality usually works seamlessly for C/C++ programs,
but the Java platform is always for x86_64-darwin.

Add-on executables are expected to work without manual user
configuration.  Each component settings script needs to determine the
platform details appropriately.


The Isabelle settings environment provides the following variables to
help configuring platform-dependent tools:

  ISABELLE_PLATFORM64  (potentially empty)
  ISABELLE_PLATFORM32  (potentially empty)
  ISABELLE_PLATFORM

The ISABELLE_PLATFORM setting variable prefers the 32 bit version of the
platform, if possible. Using regular bash notation, tools may express their
preference for 64 bit with a fall-back for 32 bit as follows:

  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"


There is a second set of settings for native Windows (instead of the
POSIX emulation of Cygwin used before):

  ISABELLE_WINDOWS_PLATFORM64
  ISABELLE_WINDOWS_PLATFORM32
  ISABELLE_WINDOWS_PLATFORM

It can be used like this:

  "${ISABELLE_WINDOWS_PLATFORM:-$ISABELLE_PLATFORM}"

  "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"


Moreover note that ML and JVM usually have a different idea of the
platform, depending on the respective binaries that are actually run.
Poly/ML 5.6.x performs best in 32 bit mode, even for large
applications, thanks to its sophisticated heap management.  The JVM
usually works better in 64 bit mode, which allows its heap to grow
beyond 2 GB.

The traditional "uname" Unix tool only tells about its own executable
format, not the underlying platform!


Dependable system tools
-----------------------

The following portable system tools can be taken for granted:

* Scala on top of Java 8.  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 -- there are too many non-standard
  implementations of it.

* Perl as largely portable system programming language, with its
  fairly robust support for processes, signals, sockets etc.


Known problems
--------------

* Mac OS X: 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.

* Mac OS X: 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.

* The Java runtime has its own idea about the underlying platform,
  which affects Java native libraries in particular.  In
  Isabelle/Scala the function isabelle.Platform.jvm_platform
  identifies the JVM platform.  Since a particular Java version is
  always bundled with Isabelle, the resulting settings also provide
  some clues about its platform, without running it.

* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are
  notoriously non-portable an should be avoided.