Admin/PLATFORMS
author wenzelm
Wed Apr 20 13:17:25 2011 +0200 (2011-04-20)
changeset 42424 e94350a2ed20
parent 41668 62ed9f31ea90
child 44876 243e2a413787
permissions -rw-r--r--
updated reference machines;
     1 Some notes on multi-platform support of Isabelle
     2 ================================================
     3 
     4 Preamble
     5 --------
     6 
     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.
    10 
    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 bash_output.  The settings environment also provides some means
    14 for portability, e.g. jvm_path to hold up the impression that Java on
    15 Windows/Cygwin adheres to Isabelle/POSIX standards.
    16 
    17 When producing add-on tools, it is important to stay within this clean
    18 room of Isabelle, and refrain from overly ambitious system hacking.
    19 The existing Isabelle scripts follow a certain style that might look
    20 odd at first sight, but reflects long years of experience in getting
    21 system plumbing right (which is quite hard).
    22 
    23 
    24 Supported platforms
    25 -------------------
    26 
    27 The following hardware and operating system platforms are officially
    28 supported by the Isabelle distribution (and bundled tools), with the
    29 following reference versions (which have been selected to be neither
    30 too old nor too new):
    31 
    32   x86-linux         SuSE 11.0 (atbroy51) (??)
    33   x86-darwin        Mac OS Leopard (macbroy30)
    34   x86-cygwin        Cygwin 1.7 (atbroy102)
    35 
    36   x86_64-linux      SuSE 11.0 (atbroy100)
    37   x86_64-darwin     Mac OS Leopard (macbroy30)
    38 
    39 All of the above platforms are 100% supported by Isabelle -- end-users
    40 should not have to care about the differences at all.  There are also
    41 some secondary platforms where Poly/ML also happens to work:
    42 
    43   ppc-darwin
    44   sparc-solaris
    45   x86-solaris
    46   x86-bsd
    47 
    48 There is no guarantee that Isabelle add-ons work on these fringe
    49 platforms.  Even Isabelle/Scala already fails on ppc-darwin due to
    50 lack of JVM 1.6 support by Apple.
    51 
    52 
    53 32 bit vs. 64 bit platforms
    54 ---------------------------
    55 
    56 64 bit hardware becomes more and more important for power users.
    57 Add-on tools need to work seamlessly without manual user
    58 configuration, although it is often sufficient to fall back on 32 bit
    59 executables.
    60 
    61 The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
    62 the platform, even on 64 bit hardware.  Power-tools need to indicate
    63 64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
    64 setting.  The following bash expression prefers the 64 bit platform,
    65 if that is available:
    66 
    67   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
    68 
    69 Note that ML and JVM may have a different idea of the platform,
    70 depending on the respective binaries that are actually run.
    71 
    72 
    73 Dependable system tools
    74 -----------------------
    75 
    76 The following portable system tools can be taken for granted:
    77 
    78 * GNU bash as uniform shell on all platforms.  The POSIX "standard"
    79   shell /bin/sh is *not* appropriate, because there are too many
    80   different implementations of it.
    81 
    82 * Perl as largely portable system programming language.  In some
    83   situations Python may serve as an alternative, but it usually
    84   performs not as well in addressing various delicate details of
    85   operating system concepts (processes, signals, sockets etc.).
    86 
    87 * Scala with Java Runtime 1.6.  The Isabelle/Pure.jar library irons
    88   out many oddities and portability problems of the Java platform.
    89 
    90 
    91 Known problems
    92 --------------
    93 
    94 * Mac OS: If MacPorts is installed there is some danger that
    95   accidental references to its shared libraries are created
    96   (e.g. libgmp).  Use otool -L to check if compiled binaries also work
    97   without MacPorts.
    98 
    99 * Mac OS: If MacPorts is installed and its version of Perl takes
   100   precedence over /usr/bin/perl in the PATH, then the end-user needs
   101   to take care of installing extra modules, e.g. for HTTP support.
   102   Such add-ons are usually included in Apple's /usr/bin/perl by
   103   default.
   104 
   105 * The Java runtime has its own idea about the underlying platform,
   106   e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM
   107   could be x86_64-linux.  This affects Java native libraries in
   108   particular -- which cause extra portability problems and can make
   109   the JVM crash anyway.
   110 
   111   In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
   112   platform.  Since there can be many different Java installations on
   113   the same machine, which can also be run with different options,
   114   reliable JVM platform identification works from inside the running
   115   JVM only.