Admin/PLATFORMS
author wenzelm
Tue Jul 19 09:55:03 2016 +0200 (2016-07-19)
changeset 63520 2803d2b8f85d
parent 62011 03e69b1bf359
child 64337 e3b57c8046cb
permissions -rw-r--r--
Linux platform base-line is Ubuntu 12.04 LTS;
     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
    15 "platform_path" to keep the impression that Windows/Cygwin adheres to
    16 Isabelle/POSIX standards, although Poly/ML and the JVM are
    17 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 12.04 LTS
    34   x86_64-linux      Ubuntu 12.04 LTS
    35 
    36   x86_64-darwin     Mac OS X 10.8 Mountain Lion (macbroy30)
    37                     Mac OS X 10.9 Mavericks (macbroy2)
    38                     Mac OS X 10.10 Yosemite (macbroy31)
    39                     Mac OS X 10.11 El Capitan
    40 
    41   x86-cygwin        http://isabelle.in.tum.de/cygwin_2015 (x86/release)
    42 
    43 All of the above platforms are 100% supported by Isabelle -- end-users
    44 should not have to care about the differences (at least in theory).
    45 
    46 Fringe platforms like BSD or Solaris are unsupported.
    47 
    48 
    49 32 bit vs. 64 bit platforms
    50 ---------------------------
    51 
    52 Most users have 64 bit hardware and are running a 64 bit operating
    53 system by default.  For Linux this usually means missing 32 bit shared
    54 libraries, so native x86_64-linux needs to be used by default, despite
    55 its doubled space requirements for Poly/ML heaps.  For Mac OS X, the
    56 x86-darwin personality usually works seamlessly for C/C++ programs,
    57 but the Java 7 platform is only available for x86_64-darwin.
    58 
    59 Add-on executables are expected to work without manual user
    60 configuration.  Each component settings script needs to determine the
    61 platform details appropriately.
    62 
    63 The Isabelle settings environment provides the following variables to
    64 help configuring platform-dependent tools:
    65 
    66   ISABELLE_PLATFORM64  (potentially empty)
    67   ISABELLE_PLATFORM32
    68   ISABELLE_PLATFORM
    69 
    70 The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
    71 the platform, even on 64 bit hardware.  Using regular bash notation,
    72 tools may express their preference for 64 bit with a fall-back for 32
    73 bit as follows:
    74 
    75   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
    76 
    77 Moreover note that ML and JVM usually have a different idea of the
    78 platform, depending on the respective binaries that are actually run.
    79 Poly/ML 5.5.x performs best in 32 bit mode, even for large
    80 applications, thanks to its sophisticated heap management.  The JVM
    81 usually works better in 64 bit mode, which allows its heap to grow
    82 beyond 2 GB.
    83 
    84 The traditional "uname" Unix tool usually only tells about its own
    85 executable format, not the underlying platform!
    86 
    87 
    88 Dependable system tools
    89 -----------------------
    90 
    91 The following portable system tools can be taken for granted:
    92 
    93 * GNU bash as uniform shell on all platforms.  The POSIX "standard"
    94   shell /bin/sh is *not* appropriate, because there are too many
    95   non-standard implementations of it.
    96 
    97 * Perl as largely portable system programming language, with its
    98   fairly robust support for processes, signals, sockets etc.
    99 
   100 * Scala with Java 1.8.  Isabelle/Scala irons out many oddities and
   101   portability issues of the Java platform.
   102 
   103 
   104 Known problems
   105 --------------
   106 
   107 * Mac OS X: If MacPorts is installed there is some danger that
   108   accidental references to its shared libraries are created
   109   (e.g. libgmp).  Use otool -L to check if compiled binaries also work
   110   without MacPorts.
   111 
   112 * Mac OS X: If MacPorts is installed and its version of Perl takes
   113   precedence over /usr/bin/perl in the PATH, then the end-user needs
   114   to take care of installing extra modules, e.g. for HTTP support.
   115   Such add-ons are usually included in Apple's /usr/bin/perl by
   116   default.
   117 
   118 * The Java runtime has its own idea about the underlying platform,
   119   which affects Java native libraries in particular.  In
   120   Isabelle/Scala the function isabelle.Platform.jvm_platform
   121   identifies the JVM platform.  Since a particular Java version is
   122   always bundled with Isabelle, the resulting settings also provide
   123   some clues about its platform, without running it.
   124 
   125 * Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are
   126   notoriously non-portable an should be avoided.