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

 environment, with as little system-specific code in user-space tools

 and packages.

 as possible.

 make this work, e.g. see the ML structures File and Path, or functions

 make this work, e.g. see the ML and Scala modules File and Path, or

 like Isabelle_System.bash.  The settings environment also provides

 functions like Isabelle_System.bash.  The settings environment also

 some means for portability, e.g. jvm_path to keep the impression that

 provides some means for portability, e.g. jvm_path to keep the

 Java on Windows/Cygwin adheres to Isabelle/POSIX standards (inside the

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

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

 standards, although inside the JVM itself there are many

 Windows-specific things.

 The existing Isabelle scripts follow a certain style that might look

 The existing Isabelle scripts follow a peculiar style that reflects

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

 long years of experience in getting system plumbing right.

 getting system plumbing right (which is quite hard).

   x86-darwin        Mac OS Leopard (macbroy30)

   x86_64-linux      Ubuntu 10.04 LTS

                     Mac OS Snow Leopard (macbroy2)

   x86_64-darwin     Mac OS Snow Leopard (macbroy2)

 There are also some additional platforms where Poly/ML also happens to

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

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

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

 packages are installed on BSD.

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

 longer supported due the its lack of Java 7.

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

 Most users have 64 bit hardware and are running a 64 bit operating

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

 system by default.  For Linux this often means missing 32 bit shared

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

 libraries, so native x86_64-linux needs to be used by default, despite

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

 its doubled space requirements for Poly/ML heaps.  For Mac OS X, the

 seamlessly without manual user configuration, either as native 64 bit

 x86-darwin personality usually works seamlessly for C/C++ programs,

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

 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 platform, even on 64 bit hardware.  Tools need to indicate 64 bit

 the platform, even on 64 bit hardware.  Using regular bash notation,

 support explicitly via the (optional) ISABELLE_PLATFORM64 setting, if

 tools may express their preference for 64 bit with a fall-back for 32

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

 bit as follows:

 bit platform, if that is available:

   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"

   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"

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

 Moreover note that ML and JVM usually have a different idea of the

 depending on the respective binaries that are actually run.  The

 platform, depending on the respective binaries that are actually run.

 "uname" Unix tool usually only tells about its own executable format,

 Poly/ML 5.5.x runs most efficiently on 32 bit, even for large

 not the underlying platform.

 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!

 * Scala with Java Runtime 1.6.  The Isabelle/Scala layer irons out

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

   many oddities and portability issues of the Java platform.

   oddities and portability issues of the Java platform.

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

   which affects Java native libraries in particular.  In

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

   Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM

   particular -- which cause extra portability problems and can make

   the JVM crash anyway.

   In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM