author wenzelm
Sun Sep 18 16:24:26 2011 +0200 (2011-09-18)
changeset 44977 1b2ce8d0f8e3
parent 44876 243e2a413787
child 46006 36cd232b18bb
permissions -rw-r--r--
more Mac OS reference hardware;
     1 Some notes on multi-platform support of Isabelle
     2 ================================================
     4 Preamble
     5 --------
     7 The general programming model is that of a stylized ML + Scala + POSIX
     8 environment, with hardly any system specific code in user-space tools
     9 and packages.
    11 The basic Isabelle system infrastructure provides some facilities to
    12 make this work, e.g. see the ML structures File and Path, or functions
    13 like Isabelle_System.bash.  The settings environment also provides
    14 some means for portability, e.g. jvm_path to keep the impression that
    15 Java on Windows/Cygwin adheres to Isabelle/POSIX standards (inside the
    16 JVM itself there are many Windows-specific things, though).
    18 When producing add-on tools, it is important to stay within this clean
    19 room of Isabelle, and refrain from overly ambitious system hacking.
    20 The existing Isabelle scripts follow a certain style that might look
    21 odd at first sight, but it reflects long years of experience in
    22 getting system plumbing right (which is quite hard).
    25 Supported platforms
    26 -------------------
    28 The following hardware and operating system platforms are officially
    29 supported by the Isabelle distribution (and bundled tools), with the
    30 following reference versions (which have been selected to be neither
    31 too old nor too new):
    33   x86-linux         Ubuntu 10.04 LTS
    34   x86-darwin        Mac OS Leopard (macbroy30)
    35                     Mac OS Snow Leopard (macbroy2)
    36                     Mac OS Lion (macbroy6)
    37   x86-cygwin        Cygwin 1.7 (vmbroy9)
    39   x86_64-linux      Ubuntu 10.04 LTS
    40   x86_64-darwin     Mac OS Leopard (macbroy30)
    41                     Mac OS Snow Leopard (macbroy2)
    42                     Mac OS Lion (macbroy6)
    44 All of the above platforms are 100% supported by Isabelle -- end-users
    45 should not have to care about the differences (at least in theory).
    46 There are also some additional platforms where Poly/ML also happens to
    47 work, but they are *not* covered by the official Isabelle
    48 distribution:
    50   ppc-darwin
    51   sparc-solaris
    52   x86-solaris
    53   x86-bsd
    55 There are increasing problems to make contributing components of
    56 Isabelle work on such fringe platforms.  Note that x86-bsd is silently
    57 treated like x86-linux -- this works if certain Linux compatibility
    58 packages are installed on BSD.
    61 32 bit vs. 64 bit platforms
    62 ---------------------------
    64 64 bit hardware becomes more and more important for many users.
    65 Add-on tools need to work seamlessly without manual user
    66 configuration, although it is often sufficient to fall back on 32 bit
    67 executables.
    69 The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
    70 the platform, even on 64 bit hardware.  Power-tools need to indicate
    71 64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
    72 setting.  The following bash expression prefers the 64 bit platform,
    73 if that is available:
    77 Note that ML and JVM may have a different idea of the platform,
    78 depending on the respective binaries that are actually run.
    81 Dependable system tools
    82 -----------------------
    84 The following portable system tools can be taken for granted:
    86 * GNU bash as uniform shell on all platforms.  The POSIX "standard"
    87   shell /bin/sh is *not* appropriate, because there are too many
    88   non-standard implementations of it.
    90 * Perl as largely portable system programming language.  In some
    91   situations Python may serve as an alternative, but it usually
    92   performs not as well in addressing various delicate details of
    93   operating system concepts (processes, signals, sockets etc.).
    95 * Scala with Java Runtime 1.6.  The Isabelle/Scala layer irons out
    96   many oddities and portability issues of the Java platform.
    99 Known problems
   100 --------------
   102 * Mac OS: If MacPorts is installed there is some danger that
   103   accidental references to its shared libraries are created
   104   (e.g. libgmp).  Use otool -L to check if compiled binaries also work
   105   without MacPorts.
   107 * Mac OS: If MacPorts is installed and its version of Perl takes
   108   precedence over /usr/bin/perl in the PATH, then the end-user needs
   109   to take care of installing extra modules, e.g. for HTTP support.
   110   Such add-ons are usually included in Apple's /usr/bin/perl by
   111   default.
   113 * The Java runtime has its own idea about the underlying platform,
   114   e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM
   115   could be x86_64-linux.  This affects Java native libraries in
   116   particular -- which cause extra portability problems and can make
   117   the JVM crash anyway.
   119   In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
   120   platform.  Since there can be many different Java installations on
   121   the same machine, which can also be run with different options,
   122   reliable JVM platform identification works from inside the running
   123   JVM only.