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 +supported by the Isabelle distribution (and bundled tools), with the
1.33 +following reference versions (which have been selected to be neither
1.34 +too old nor too new):
1.35
1.36 - x86-linux
1.37 - x86-darwin
1.38 - x86-cygwin
1.39 - x86_64-linux
1.40 - x86_64-darwin
1.41 + x86-linux Ubuntu 8.04 LTS Server
1.42 + x86-darwin Mac OS Leopard
1.43 + x86-cygwin Cygwin 1.7
1.44
1.45 -As of Cygwin 1.7 there is only a 32 bit version of that platform. The
1.46 -other 64 bit platforms become more and more important for power users
1.47 -and always need to be taken into account when testing tools.
1.48 + x86_64-linux Ubuntu 8.04 LTS Server (64)
1.49 + x86_64-darwin Mac OS Leopard
1.50
1.51 -All of the above platforms are 100% supported -- end-users should not
1.52 -have to care about the differences at all. There are also some
1.53 -secondary platforms where Poly/ML also happens to work:
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 all. There are also
1.56 +some secondary platforms where Poly/ML also happens to work:
1.57
1.58 ppc-darwin
1.59 sparc-solaris
1.60 @@ -45,7 +47,27 @@
1.61
1.62 There is no guarantee that Isabelle add-ons work on these fringe
1.63 platforms. Even Isabelle/Scala already fails on ppc-darwin due to
1.64 -lack of JVM 1.6 support on that platform.
1.65 +lack of JVM 1.6 support by Apple.
1.66 +
1.67 +
1.68 +32 bit vs. 64 bit platforms
1.69 +---------------------------
1.70 +
1.71 +64 bit hardware becomes more and more important for power users.
1.72 +Add-on tools need to work seamlessly without manual user
1.73 +configuration, although it is often sufficient to fall back on 32 bit
1.74 +executables.
1.75 +
1.76 +The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
1.77 +the platform, even on 64 bit hardware. Power-tools need to indicate
1.78 +64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
1.79 +setting. The following bash expressions prefers the 64 bit platform,
1.80 +if that is available:
1.81 +
1.82 + "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
1.83 +
1.84 +Note that ML and JVM may have a different idea of the platform,
1.85 +depending the the respective binaries that are actually run.
1.86
1.87
1.88 Dependable system tools
1.89 @@ -53,17 +75,17 @@
1.90
1.91 The following portable system tools can be taken for granted:
1.92
1.93 - * GNU bash as uniform shell on all platforms. Note that the POSIX
1.94 - "standard" shell /bin/sh is *not* appropriate, because there are
1.95 - too many different implementations of it.
1.96 +* GNU bash as uniform shell on all platforms. The POSIX "standard"
1.97 + shell /bin/sh is *not* appropriate, because there are too many
1.98 + different implementations of it.
1.99
1.100 - * Perl as largely portable system programming language. In some
1.101 - situations Python may as an alternative, but it usually performs
1.102 - not as well in addressing various delicate details of basic
1.103 - operating system concepts (processes, signals, sockets etc.).
1.104 +* Perl as largely portable system programming language. In some
1.105 + situations Python may serve as an alternative, but it usually
1.106 + performs not as well in addressing various delicate details of
1.107 + operating system concepts (processes, signals, sockets etc.).
1.108
1.109 - * Scala with Java Runtime 1.6. The Isabelle/Pure.jar library irons
1.110 - out many oddities and portability problems of the Java platform.
1.111 +* Scala with Java Runtime 1.6. The Isabelle/Pure.jar library irons
1.112 + out many oddities and portability problems of the Java platform.
1.113
1.114
1.115 Known problems
1.116 @@ -71,11 +93,18 @@
1.117
1.118 * Mac OS: If MacPorts is installed and its version of Perl takes
1.119 precedence over /usr/bin/perl in the PATH, then the end-user needs
1.120 - to take care of installing add-on modules, e.g. HTTP support. Such
1.121 - add-ons are usually included in Apple's /usr/bin/perl by default.
1.122 + to take care of installing extra modules, e.g. for HTTP support.
1.123 + Such add-ons are usually included in Apple's /usr/bin/perl by
1.124 + default.
1.125
1.126 * The Java runtime has its own idea about the underlying platform,
1.127 - e.g. on 64 bit machine Isabelle/ML could be x86-linux, but the JVM
1.128 + e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM
1.129 could be x86_64-linux. This affects Java native libraries in
1.130 - particular -- which are very hard to support in a platform
1.131 - independent manner, and should be avoided in the first place.
1.132 + particular -- which cause extra portability problems and can make
1.133 + the JVM crash anyway.
1.134 +
1.135 + In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
1.136 + platform. Since there can be many different Java installations on
1.137 + the same machine, which can also be run with different options,
1.138 + reliable JVM platform identification works from inside the running
1.139 + JVM only.