Some notes on 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. jvm_path to keep the

impression that Java on Windows/Cygwin adheres to Isabelle/POSIX

standards, although inside the JVM itself there are many

Windows-specific things.

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 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 reference versions (which have been selected to be neither

too old nor too new):

  x86-linux         Ubuntu 10.04 LTS

  x86_64-linux      Ubuntu 10.04 LTS

  x86_64-darwin     Mac OS Snow Leopard (macbroy2)

                    Mac OS Lion (macbroy6)

                    Mac OS Mountain Lion (macbroy30)

  x86-cygwin        Cygwin 1.7 (vmbroy9)

All of the above platforms are 100% supported by Isabelle -- end-users

should not have to care about the differences (at least in theory).

There are also some additional platforms where Poly/ML might also

happen to work, but they are *not* covered by the official Isabelle

distribution:

  ppc-darwin

  x86-darwin

  sparc-solaris

  x86-solaris

  x86-bsd

There are increasing problems to make contributing components of

Isabelle work on such fringe platforms.  Note that x86-bsd is silently

treated like x86-linux -- this works if certain Linux compatibility

packages are installed on BSD.  Old 32 bit Macintosh hardware is no

longer supported due the its lack of Java 7.

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 often 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 7 platform is only available for x86_64-darwin.

Add-on executables are expected to without manual user configuration,

Each component settings script needs to work out the platform details

appropriately.

The Isabelle settings environment provides the following variables to

help configuring platform-dependent tools:

  ISABELLE_PLATFORM64  (potentially empty)

  ISABELLE_PLATFORM32

  ISABELLE_PLATFORM

The ISABELLE_PLATFORM setting variable refers to the 32 bit version of

the platform, even on 64 bit hardware.  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}"

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.5.x runs most efficiently on 32 bit, even for large

applications.  The JVM usually performs better in 64 bit mode.

The traditional "uname" Unix tool usually only tells about its own

executable format, not the underlying platform!

Dependable system tools

-----------------------

The following portable system tools can be taken for granted:

* GNU bash as uniform shell on all platforms.  The POSIX "standard"

  shell /bin/sh is *not* appropriate, because there are too many

  non-standard implementations of it.

* Perl as largely portable system programming language.  In some

  situations Python may serve as an alternative, but it usually

  performs not as well in addressing various delicate details of

  operating system concepts (processes, signals, sockets etc.).

* Scala with Java 1.7.  The Isabelle/Scala layer irons out many

  oddities and portability issues of the Java platform.

Known problems

--------------

* Mac OS: 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: 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 isabelle.Platform.jvm_platform identifies the JVM

  platform.  Since there can be many different Java installations on

  the same machine, which can also be run with different options,

  reliable JVM platform identification works from inside the running

  JVM only.