Some notes on multi-platform support of Isabelle

================================================

Preamble

--------

The general programming model is that of a stylized ML + Scala + POSIX

environment, with hardly any system specific code in user-space tools

and packages.

The basic Isabelle system infrastructure provides some facilities to

make this work, e.g. see the ML structures 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 (inside the

JVM itself there are many Windows-specific things, though).

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 certain style that might look

odd at first sight, but it reflects long years of experience in

getting system plumbing right (which is quite hard).

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-darwin        Mac OS Leopard (macbroy30)

                    Mac OS Snow Leopard (macbroy2)

                    Mac OS Lion (macbroy6)

  x86-cygwin        Cygwin 1.7 (vmbroy9)

  x86_64-linux      Ubuntu 10.04 LTS

  x86_64-darwin     Mac OS Leopard (macbroy30)

                    Mac OS Snow Leopard (macbroy2)

                    Mac OS Lion (macbroy6)

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 also happens to

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

distribution:

  ppc-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.

32 bit vs. 64 bit platforms

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

Most users already have 64 bit hardware, and many of them are running

a 64 bit operating system.  Native 64 bit support for ML and Scala/JVM

is increasingly important for big Isabelle applications, but 32 bit is

often the default to get started.  Add-on executables need to work

seamlessly without manual user configuration, either as native 64 bit

executables or in 32 bit mode on a 64 bit platform.

The ISABELLE_PLATFORM setting variable refers to the 32 bit version of

the platform, even on 64 bit hardware.  Tools need to indicate 64 bit

support explicitly via the (optional) ISABELLE_PLATFORM64 setting, if

this is really required.  The following bash expression prefers the 64

bit platform, if that is available:

  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"

Note that ML and JVM may have a different idea of the platform,

depending on the respective binaries that are actually run.  The

"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 Runtime 1.6.  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,

  e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM

  could be x86_64-linux.  This affects Java native libraries in

  particular -- which cause extra portability problems and can make

  the JVM crash anyway.

  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.