some updates on multi-platform support;
authorwenzelm
Mon Apr 19 16:04:42 2010 +0200 (2010-04-19)
changeset 3620416c371c6ff86
parent 36203 398dd97e49a5
child 36205 e86d9a10e982
some updates on multi-platform support;
Admin/PLATFORMS
     1.1 --- a/Admin/PLATFORMS	Mon Apr 19 12:15:06 2010 +0200
     1.2 +++ b/Admin/PLATFORMS	Mon Apr 19 16:04:42 2010 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4 -Some notes on platform support of Isabelle
     1.5 -==========================================
     1.6 +Some notes on multi-platform support of Isabelle
     1.7 +================================================
     1.8  
     1.9  Preamble
    1.10  --------
    1.11 @@ -11,32 +11,34 @@
    1.12  The basic Isabelle system infrastructure provides some facilities to
    1.13  make this work, e.g. see the ML structures File and Path, or functions
    1.14  like bash_output.  The settings environment also provides some means
    1.15 -for portability, e.g. jvm_path to hold up the impression that even
    1.16 -Java on Windows/Cygwin adheres to Isabelle/POSIX standards.
    1.17 +for portability, e.g. jvm_path to hold up the impression that Java on
    1.18 +Windows/Cygwin adheres to Isabelle/POSIX standards.
    1.19  
    1.20  When producing add-on tools, it is important to stay within this clean
    1.21  room of Isabelle, and refrain from overly ambitious system hacking.
    1.22 +The existing Isabelle scripts follow a certain style that might look
    1.23 +odd at first sight, but reflects long years of experience in getting
    1.24 +system plumbing right (which is quite hard).
    1.25  
    1.26  
    1.27  Supported platforms
    1.28  -------------------
    1.29  
    1.30  The following hardware and operating system platforms are officially
    1.31 -supported by the Isabelle distribution (and bundled tools):
    1.32 -
    1.33 -  x86-linux
    1.34 -  x86-darwin
    1.35 -  x86-cygwin
    1.36 -  x86_64-linux
    1.37 -  x86_64-darwin
    1.38 +supported by the Isabelle distribution (and bundled tools), with the
    1.39 +following reference versions (which have been selected to be neither
    1.40 +too old nor too new):
    1.41  
    1.42 -As of Cygwin 1.7 there is only a 32 bit version of that platform.  The
    1.43 -other 64 bit platforms become more and more important for power users
    1.44 -and always need to be taken into account when testing tools.
    1.45 +  x86-linux         Ubuntu 8.04 LTS Server
    1.46 +  x86-darwin        Mac OS Leopard
    1.47 +  x86-cygwin        Cygwin 1.7
    1.48  
    1.49 -All of the above platforms are 100% supported -- end-users should not
    1.50 -have to care about the differences at all.  There are also some
    1.51 -secondary platforms where Poly/ML also happens to work:
    1.52 +  x86_64-linux      Ubuntu 8.04 LTS Server (64)
    1.53 +  x86_64-darwin     Mac OS Leopard
    1.54 +
    1.55 +All of the above platforms are 100% supported by Isabelle -- end-users
    1.56 +should not have to care about the differences at all.  There are also
    1.57 +some secondary platforms where Poly/ML also happens to work:
    1.58  
    1.59    ppc-darwin
    1.60    sparc-solaris
    1.61 @@ -45,7 +47,27 @@
    1.62  
    1.63  There is no guarantee that Isabelle add-ons work on these fringe
    1.64  platforms.  Even Isabelle/Scala already fails on ppc-darwin due to
    1.65 -lack of JVM 1.6 support on that platform.
    1.66 +lack of JVM 1.6 support by Apple.
    1.67 +
    1.68 +
    1.69 +32 bit vs. 64 bit platforms
    1.70 +---------------------------
    1.71 +
    1.72 +64 bit hardware becomes more and more important for power users.
    1.73 +Add-on tools need to work seamlessly without manual user
    1.74 +configuration, although it is often sufficient to fall back on 32 bit
    1.75 +executables.
    1.76 +
    1.77 +The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
    1.78 +the platform, even on 64 bit hardware.  Power-tools need to indicate
    1.79 +64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
    1.80 +setting.  The following bash expressions prefers the 64 bit platform,
    1.81 +if that is available:
    1.82 +
    1.83 +  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
    1.84 +
    1.85 +Note that ML and JVM may have a different idea of the platform,
    1.86 +depending the the respective binaries that are actually run.
    1.87  
    1.88  
    1.89  Dependable system tools
    1.90 @@ -53,17 +75,17 @@
    1.91  
    1.92  The following portable system tools can be taken for granted:
    1.93  
    1.94 -  * GNU bash as uniform shell on all platforms.  Note that the POSIX
    1.95 -    "standard" shell /bin/sh is *not* appropriate, because there are
    1.96 -    too many different implementations of it.
    1.97 +* GNU bash as uniform shell on all platforms.  The POSIX "standard"
    1.98 +  shell /bin/sh is *not* appropriate, because there are too many
    1.99 +  different implementations of it.
   1.100  
   1.101 -  * Perl as largely portable system programming language.  In some
   1.102 -    situations Python may as an alternative, but it usually performs
   1.103 -    not as well in addressing various delicate details of basic
   1.104 -    operating system concepts (processes, signals, sockets etc.).
   1.105 +* Perl as largely portable system programming language.  In some
   1.106 +  situations Python may serve as an alternative, but it usually
   1.107 +  performs not as well in addressing various delicate details of
   1.108 +  operating system concepts (processes, signals, sockets etc.).
   1.109  
   1.110 -  * Scala with Java Runtime 1.6.  The Isabelle/Pure.jar library irons
   1.111 -    out many oddities and portability problems of the Java platform.
   1.112 +* Scala with Java Runtime 1.6.  The Isabelle/Pure.jar library irons
   1.113 +  out many oddities and portability problems of the Java platform.
   1.114  
   1.115  
   1.116  Known problems
   1.117 @@ -71,11 +93,18 @@
   1.118  
   1.119  * Mac OS: If MacPorts is installed and its version of Perl takes
   1.120    precedence over /usr/bin/perl in the PATH, then the end-user needs
   1.121 -  to take care of installing add-on modules, e.g. HTTP support.  Such
   1.122 -  add-ons are usually included in Apple's /usr/bin/perl by default.
   1.123 +  to take care of installing extra modules, e.g. for HTTP support.
   1.124 +  Such add-ons are usually included in Apple's /usr/bin/perl by
   1.125 +  default.
   1.126  
   1.127  * The Java runtime has its own idea about the underlying platform,
   1.128 -  e.g. on 64 bit machine Isabelle/ML could be x86-linux, but the JVM
   1.129 +  e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM
   1.130    could be x86_64-linux.  This affects Java native libraries in
   1.131 -  particular -- which are very hard to support in a platform
   1.132 -  independent manner, and should be avoided in the first place.
   1.133 +  particular -- which cause extra portability problems and can make
   1.134 +  the JVM crash anyway.
   1.135 +
   1.136 +  In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
   1.137 +  platform.  Since there can be many different Java installations on
   1.138 +  the same machine, which can also be run with different options,
   1.139 +  reliable JVM platform identification works from inside the running
   1.140 +  JVM only.