author wenzelm
Sat, 06 Mar 2010 14:28:31 +0100
changeset 35610 a5b7a0903441
child 36204 16c371c6ff86
permissions -rw-r--r--
Some notes on platform support of Isabelle.

Some notes on platform support of Isabelle


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

Supported platforms

The following hardware and operating system platforms are officially
supported by the Isabelle distribution (and bundled tools):


As of Cygwin 1.7 there is only a 32 bit version of that platform.  The
other 64 bit platforms become more and more important for power users
and always need to be taken into account when testing tools.

All of the above platforms are 100% supported -- 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:


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 on that platform.

Dependable system tools

The following portable system tools can be taken for granted:

  * GNU bash as uniform shell on all platforms.  Note that 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 as an alternative, but it usually performs
    not as well in addressing various delicate details of basic
    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 add-on modules, e.g. 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 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 are very hard to support in a platform
  independent manner, and should be avoided in the first place.