updates on 32 bit vs. 64 bit platforms;
authorwenzelm
Fri Aug 17 11:18:26 2012 +0200 (2012-08-17)
changeset 4883310584ca5785f
parent 48832 ab9663b8734b
child 48834 94bb87ef7127
updates on 32 bit vs. 64 bit platforms;
added Mountain Lion;
dropped Leopard;
tuned;
Admin/PLATFORMS
     1.1 --- a/Admin/PLATFORMS	Fri Aug 17 10:46:42 2012 +0200
     1.2 +++ b/Admin/PLATFORMS	Fri Aug 17 11:18:26 2012 +0200
     1.3 @@ -5,21 +5,21 @@
     1.4  --------
     1.5  
     1.6  The general programming model is that of a stylized ML + Scala + POSIX
     1.7 -environment, with hardly any system specific code in user-space tools
     1.8 -and packages.
     1.9 +environment, with as little system-specific code in user-space tools
    1.10 +as possible.
    1.11  
    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 Isabelle_System.bash.  The settings environment also provides
    1.15 -some means for portability, e.g. jvm_path to keep the impression that
    1.16 -Java on Windows/Cygwin adheres to Isabelle/POSIX standards (inside the
    1.17 -JVM itself there are many Windows-specific things, though).
    1.18 +make this work, e.g. see the ML and Scala modules File and Path, or
    1.19 +functions like Isabelle_System.bash.  The settings environment also
    1.20 +provides some means for portability, e.g. jvm_path to keep the
    1.21 +impression that Java on Windows/Cygwin adheres to Isabelle/POSIX
    1.22 +standards, although inside the JVM itself there are many
    1.23 +Windows-specific things.
    1.24  
    1.25  When producing add-on tools, it is important to stay within this clean
    1.26  room of Isabelle, and refrain from overly ambitious system hacking.
    1.27 -The existing Isabelle scripts follow a certain style that might look
    1.28 -odd at first sight, but it reflects long years of experience in
    1.29 -getting system plumbing right (which is quite hard).
    1.30 +The existing Isabelle scripts follow a peculiar style that reflects
    1.31 +long years of experience in getting system plumbing right.
    1.32  
    1.33  
    1.34  Supported platforms
    1.35 @@ -31,23 +31,22 @@
    1.36  too old nor too new):
    1.37  
    1.38    x86-linux         Ubuntu 10.04 LTS
    1.39 -  x86-darwin        Mac OS Leopard (macbroy30)
    1.40 -                    Mac OS Snow Leopard (macbroy2)
    1.41 -                    Mac OS Lion (macbroy6)
    1.42 -  x86-cygwin        Cygwin 1.7 (vmbroy9)
    1.43 +  x86_64-linux      Ubuntu 10.04 LTS
    1.44  
    1.45 -  x86_64-linux      Ubuntu 10.04 LTS
    1.46 -  x86_64-darwin     Mac OS Leopard (macbroy30)
    1.47 -                    Mac OS Snow Leopard (macbroy2)
    1.48 +  x86_64-darwin     Mac OS Snow Leopard (macbroy2)
    1.49                      Mac OS Lion (macbroy6)
    1.50 +                    Mac OS Mountain Lion (macbroy30)
    1.51 +
    1.52 +  x86-cygwin        Cygwin 1.7 (vmbroy9)
    1.53  
    1.54  All of the above platforms are 100% supported by Isabelle -- end-users
    1.55  should not have to care about the differences (at least in theory).
    1.56 -There are also some additional platforms where Poly/ML also happens to
    1.57 -work, but they are *not* covered by the official Isabelle
    1.58 +There are also some additional platforms where Poly/ML might also
    1.59 +happen to work, but they are *not* covered by the official Isabelle
    1.60  distribution:
    1.61  
    1.62    ppc-darwin
    1.63 +  x86-darwin
    1.64    sparc-solaris
    1.65    x86-solaris
    1.66    x86-bsd
    1.67 @@ -55,31 +54,45 @@
    1.68  There are increasing problems to make contributing components of
    1.69  Isabelle work on such fringe platforms.  Note that x86-bsd is silently
    1.70  treated like x86-linux -- this works if certain Linux compatibility
    1.71 -packages are installed on BSD.
    1.72 +packages are installed on BSD.  Old 32 bit Macintosh hardware is no
    1.73 +longer supported due the its lack of Java 7.
    1.74  
    1.75  
    1.76  32 bit vs. 64 bit platforms
    1.77  ---------------------------
    1.78  
    1.79 -Most users already have 64 bit hardware, and many of them are running
    1.80 -a 64 bit operating system.  Native 64 bit support for ML and Scala/JVM
    1.81 -is increasingly important for big Isabelle applications, but 32 bit is
    1.82 -often the default to get started.  Add-on executables need to work
    1.83 -seamlessly without manual user configuration, either as native 64 bit
    1.84 -executables or in 32 bit mode on a 64 bit platform.
    1.85 +Most users have 64 bit hardware and are running a 64 bit operating
    1.86 +system by default.  For Linux this often means missing 32 bit shared
    1.87 +libraries, so native x86_64-linux needs to be used by default, despite
    1.88 +its doubled space requirements for Poly/ML heaps.  For Mac OS X, the
    1.89 +x86-darwin personality usually works seamlessly for C/C++ programs,
    1.90 +but the Java 7 platform is only available for x86_64-darwin.
    1.91 +
    1.92 +Add-on executables are expected to without manual user configuration,
    1.93 +Each component settings script needs to work out the platform details
    1.94 +appropriately.
    1.95 +
    1.96 +The Isabelle settings environment provides the following variables to
    1.97 +help configuring platform-dependent tools:
    1.98 +
    1.99 +  ISABELLE_PLATFORM64  (potentially empty)
   1.100 +  ISABELLE_PLATFORM32
   1.101 +  ISABELLE_PLATFORM
   1.102  
   1.103  The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
   1.104 -the platform, even on 64 bit hardware.  Tools need to indicate 64 bit
   1.105 -support explicitly via the (optional) ISABELLE_PLATFORM64 setting, if
   1.106 -this is really required.  The following bash expression prefers the 64
   1.107 -bit platform, if that is available:
   1.108 +the platform, even on 64 bit hardware.  Using regular bash notation,
   1.109 +tools may express their preference for 64 bit with a fall-back for 32
   1.110 +bit as follows:
   1.111 +
   1.112 +  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
   1.113  
   1.114 -  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
   1.115 +Moreover note that ML and JVM usually have a different idea of the
   1.116 +platform, depending on the respective binaries that are actually run.
   1.117 +Poly/ML 5.5.x runs most efficiently on 32 bit, even for large
   1.118 +applications.  The JVM usually performs better in 64 bit mode.
   1.119  
   1.120 -Note that ML and JVM may have a different idea of the platform,
   1.121 -depending on the respective binaries that are actually run.  The
   1.122 -"uname" Unix tool usually only tells about its own executable format,
   1.123 -not the underlying platform.
   1.124 +The traditional "uname" Unix tool usually only tells about its own
   1.125 +executable format, not the underlying platform!
   1.126  
   1.127  
   1.128  Dependable system tools
   1.129 @@ -96,8 +109,8 @@
   1.130    performs not as well in addressing various delicate details of
   1.131    operating system concepts (processes, signals, sockets etc.).
   1.132  
   1.133 -* Scala with Java Runtime 1.6.  The Isabelle/Scala layer irons out
   1.134 -  many oddities and portability issues of the Java platform.
   1.135 +* Scala with Java 1.7.  The Isabelle/Scala layer irons out many
   1.136 +  oddities and portability issues of the Java platform.
   1.137  
   1.138  
   1.139  Known problems
   1.140 @@ -115,12 +128,8 @@
   1.141    default.
   1.142  
   1.143  * The Java runtime has its own idea about the underlying platform,
   1.144 -  e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM
   1.145 -  could be x86_64-linux.  This affects Java native libraries in
   1.146 -  particular -- which cause extra portability problems and can make
   1.147 -  the JVM crash anyway.
   1.148 -
   1.149 -  In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
   1.150 +  which affects Java native libraries in particular.  In
   1.151 +  Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
   1.152    platform.  Since there can be many different Java installations on
   1.153    the same machine, which can also be run with different options,
   1.154    reliable JVM platform identification works from inside the running