diff -r 398dd97e49a5 -r 16c371c6ff86 Admin/PLATFORMS --- a/Admin/PLATFORMS Mon Apr 19 12:15:06 2010 +0200 +++ b/Admin/PLATFORMS Mon Apr 19 16:04:42 2010 +0200 @@ -1,5 +1,5 @@ -Some notes on platform support of Isabelle -========================================== +Some notes on multi-platform support of Isabelle +================================================ Preamble -------- @@ -11,32 +11,34 @@ 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. +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): - - x86-linux - x86-darwin - x86-cygwin - x86_64-linux - x86_64-darwin +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): -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. + x86-linux Ubuntu 8.04 LTS Server + x86-darwin Mac OS Leopard + x86-cygwin Cygwin 1.7 -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: + 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 @@ -45,7 +47,27 @@ 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. +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 @@ -53,17 +75,17 @@ 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. +* 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 as an alternative, but it usually performs - not as well in addressing various delicate details of basic - operating system concepts (processes, signals, sockets etc.). +* 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. +* Scala with Java Runtime 1.6. The Isabelle/Pure.jar library irons + out many oddities and portability problems of the Java platform. Known problems @@ -71,11 +93,18 @@ * 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. + 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 64 bit machine Isabelle/ML could be x86-linux, but the JVM + 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 are very hard to support in a platform - independent manner, and should be avoided in the first place. + 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.