Admin/PLATFORMS

properly extract SPASS proof

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 bash_output.  The settings environment also provides some means
for portability, e.g. jvm_path to hold up the impression that Java on
Windows/Cygwin adheres to Isabelle/POSIX standards.

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 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 8.04 LTS Server
  x86-darwin        Mac OS Leopard
  x86-cygwin        Cygwin 1.7

  x86_64-linux      Ubuntu 8.04 LTS Server (64)
  x86_64-darwin     Mac OS Leopard

All of the above platforms are 100% supported by Isabelle -- end-users
should not have to care about the differences at all.  There are also
some secondary platforms where Poly/ML also happens to work:

  ppc-darwin
  sparc-solaris
  x86-solaris
  x86-bsd

There is no guarantee that Isabelle add-ons work on these fringe
platforms.  Even Isabelle/Scala already fails on ppc-darwin due to
lack of JVM 1.6 support by Apple.


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

64 bit hardware becomes more and more important for power users.
Add-on tools need to work seamlessly without manual user
configuration, although it is often sufficient to fall back on 32 bit
executables.

The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
the platform, even on 64 bit hardware.  Power-tools need to indicate
64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
setting.  The following bash expressions 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 the the respective binaries that are actually run.


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
  different 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/Pure.jar library irons
  out many oddities and portability problems of the Java platform.


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

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