Admin/PLATFORMS
author wenzelm
Fri Aug 17 11:37:14 2012 +0200 (2012-08-17)
changeset 48836 90a0af19004c
parent 48833 10584ca5785f
child 49144 84699f37481d
permissions -rw-r--r--
tuned;
     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 as little system-specific code in user-space tools
     9 as possible.
    10 
    11 The basic Isabelle system infrastructure provides some facilities to
    12 make this work, e.g. see the ML and Scala modules File and Path, or
    13 functions like Isabelle_System.bash.  The settings environment also
    14 provides some means for portability, e.g. the bash function "jvmpath"
    15 to keep the impression that Java on Windows/Cygwin adheres to
    16 Isabelle/POSIX standards, although inside the JVM itself there are
    17 many Windows-specific things.
    18 
    19 When producing add-on tools, it is important to stay within this clean
    20 room of Isabelle, and refrain from overly ambitious system hacking.
    21 The existing Isabelle scripts follow a peculiar style that reflects
    22 long years of experience in getting system plumbing right.
    23 
    24 
    25 Supported platforms
    26 -------------------
    27 
    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):
    32 
    33   x86-linux         Ubuntu 10.04 LTS
    34   x86_64-linux      Ubuntu 10.04 LTS
    35 
    36   x86_64-darwin     Mac OS Snow Leopard (macbroy2)
    37                     Mac OS Lion (macbroy6)
    38                     Mac OS Mountain Lion (macbroy30)
    39 
    40   x86-cygwin        Cygwin 1.7 (vmbroy9)
    41 
    42 All of the above platforms are 100% supported by Isabelle -- end-users
    43 should not have to care about the differences (at least in theory).
    44 There are also some additional platforms where Poly/ML might also
    45 happen to work, but they are *not* covered by the official Isabelle
    46 distribution:
    47 
    48   ppc-darwin
    49   x86-darwin
    50   sparc-solaris
    51   x86-solaris
    52   x86-bsd
    53 
    54 There are increasing problems to make contributing components of
    55 Isabelle work on such fringe platforms.  Note that x86-bsd is silently
    56 treated like x86-linux -- this works if certain Linux compatibility
    57 packages are installed on BSD.  Old 32 bit Macintosh hardware is no
    58 longer supported due the its lack of Java 7.
    59 
    60 
    61 32 bit vs. 64 bit platforms
    62 ---------------------------
    63 
    64 Most users have 64 bit hardware and are running a 64 bit operating
    65 system by default.  For Linux this often means missing 32 bit shared
    66 libraries, so native x86_64-linux needs to be used by default, despite
    67 its doubled space requirements for Poly/ML heaps.  For Mac OS X, the
    68 x86-darwin personality usually works seamlessly for C/C++ programs,
    69 but the Java 7 platform is only available for x86_64-darwin.
    70 
    71 Add-on executables are expected to without manual user configuration,
    72 Each component settings script needs to work out the platform details
    73 appropriately.
    74 
    75 The Isabelle settings environment provides the following variables to
    76 help configuring platform-dependent tools:
    77 
    78   ISABELLE_PLATFORM64  (potentially empty)
    79   ISABELLE_PLATFORM32
    80   ISABELLE_PLATFORM
    81 
    82 The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
    83 the platform, even on 64 bit hardware.  Using regular bash notation,
    84 tools may express their preference for 64 bit with a fall-back for 32
    85 bit as follows:
    86 
    87   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
    88 
    89 Moreover note that ML and JVM usually have a different idea of the
    90 platform, depending on the respective binaries that are actually run.
    91 Poly/ML 5.5.x runs most efficiently on 32 bit, even for large
    92 applications.  The JVM usually performs better in 64 bit mode.
    93 
    94 The traditional "uname" Unix tool usually only tells about its own
    95 executable format, not the underlying platform!
    96 
    97 
    98 Dependable system tools
    99 -----------------------
   100 
   101 The following portable system tools can be taken for granted:
   102 
   103 * GNU bash as uniform shell on all platforms.  The POSIX "standard"
   104   shell /bin/sh is *not* appropriate, because there are too many
   105   non-standard implementations of it.
   106 
   107 * Perl as largely portable system programming language.  In some
   108   situations Python may serve as an alternative, but it usually
   109   performs not as well in addressing various delicate details of
   110   operating system concepts (processes, signals, sockets etc.).
   111 
   112 * Scala with Java 1.7.  The Isabelle/Scala layer irons out many
   113   oddities and portability issues of the Java platform.
   114 
   115 
   116 Known problems
   117 --------------
   118 
   119 * Mac OS: If MacPorts is installed there is some danger that
   120   accidental references to its shared libraries are created
   121   (e.g. libgmp).  Use otool -L to check if compiled binaries also work
   122   without MacPorts.
   123 
   124 * Mac OS: If MacPorts is installed and its version of Perl takes
   125   precedence over /usr/bin/perl in the PATH, then the end-user needs
   126   to take care of installing extra modules, e.g. for HTTP support.
   127   Such add-ons are usually included in Apple's /usr/bin/perl by
   128   default.
   129 
   130 * The Java runtime has its own idea about the underlying platform,
   131   which affects Java native libraries in particular.  In
   132   Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
   133   platform.  Since there can be many different Java installations on
   134   the same machine, which can also be run with different options,
   135   reliable JVM platform identification works from inside the running
   136   JVM only.