Admin/PLATFORMS
author wenzelm
Wed Mar 01 11:26:19 2017 +0100 (2017-03-01)
changeset 65073 b5bf76cf2b4e
parent 64406 492de9062cd2
child 65369 27c1b5e952bd
permissions -rw-r--r--
more uniform platform settings;
     1 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 native on
    17 Windows.
    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 bash scripts follow a peculiar style that
    22 reflects 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 base-line 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 MacBookPro6,2)
    37                     Mac OS X 10.9 Mavericks (macbroy2 MacPro4,1)
    38                     Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2)
    39                     Mac OS X 10.11 El Capitan (?)
    40                     macOS 10.12 Sierra (?)
    41 
    42   x86-windows       Windows 7
    43   x86_64-windows    Windows 7
    44   x86-cygwin        Cygwin 2.6 http://isabelle.in.tum.de/cygwin_2016-1 (x86/release)
    45 
    46 All of the above platforms are 100% supported by Isabelle -- end-users
    47 should not have to care about the differences (at least in theory).
    48 
    49 Fringe platforms like BSD or Solaris are not supported.
    50 
    51 
    52 32 bit vs. 64 bit platforms
    53 ---------------------------
    54 
    55 Most users have 64 bit hardware and are running a 64 bit operating
    56 system by default.  For Linux this usually means missing 32 bit shared
    57 libraries, so native x86_64-linux needs to be used by default, despite
    58 its doubled space requirements for Poly/ML heaps.  For Mac OS X, the
    59 x86-darwin personality usually works seamlessly for C/C++ programs,
    60 but the Java platform is always for x86_64-darwin.
    61 
    62 Add-on executables are expected to work without manual user
    63 configuration.  Each component settings script needs to determine the
    64 platform details appropriately.
    65 
    66 
    67 The Isabelle settings environment provides the following variables to
    68 help configuring platform-dependent tools:
    69 
    70   ISABELLE_PLATFORM64  (potentially empty)
    71   ISABELLE_PLATFORM32
    72   ISABELLE_PLATFORM
    73 
    74 The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
    75 the platform, even on 64 bit hardware.  Using regular bash notation,
    76 tools may express their preference for 64 bit with a fall-back for 32
    77 bit as follows:
    78 
    79   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
    80 
    81 
    82 There is a second set of settings for native Windows (instead of the
    83 POSIX emulation of Cygwin used before):
    84 
    85   ISABELLE_WINDOWS_PLATFORM64  (potentially empty)
    86   ISABELLE_WINDOWS_PLATFORM32
    87   ISABELLE_WINDOWS_PLATFORM
    88 
    89 It can be used like this:
    90 
    91   "${ISABELLE_WINDOWS_PLATFORM:-$ISABELLE_PLATFORM}"
    92 
    93   "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"
    94 
    95 
    96 Moreover note that ML and JVM usually have a different idea of the
    97 platform, depending on the respective binaries that are actually run.
    98 Poly/ML 5.6.x performs best in 32 bit mode, even for large
    99 applications, thanks to its sophisticated heap management.  The JVM
   100 usually works better in 64 bit mode, which allows its heap to grow
   101 beyond 2 GB.
   102 
   103 The traditional "uname" Unix tool only tells about its own executable
   104 format, not the underlying platform!
   105 
   106 
   107 Dependable system tools
   108 -----------------------
   109 
   110 The following portable system tools can be taken for granted:
   111 
   112 * Scala on top of Java 8.  Isabelle/Scala irons out many oddities and
   113   portability issues of the Java platform.
   114 
   115 * GNU bash as uniform shell on all platforms.  The POSIX "standard"
   116   shell /bin/sh does *not* work -- there are too many non-standard
   117   implementations of it.
   118 
   119 * Perl as largely portable system programming language, with its
   120   fairly robust support for processes, signals, sockets etc.
   121 
   122 
   123 Known problems
   124 --------------
   125 
   126 * Mac OS X: If MacPorts is installed there is some danger that
   127   accidental references to its shared libraries are created
   128   (e.g. libgmp).  Use otool -L to check if compiled binaries also work
   129   without MacPorts.
   130 
   131 * Mac OS X: If MacPorts is installed and its version of Perl takes
   132   precedence over /usr/bin/perl in the PATH, then the end-user needs
   133   to take care of installing extra modules, e.g. for HTTP support.
   134   Such add-ons are usually included in Apple's /usr/bin/perl by
   135   default.
   136 
   137 * The Java runtime has its own idea about the underlying platform,
   138   which affects Java native libraries in particular.  In
   139   Isabelle/Scala the function isabelle.Platform.jvm_platform
   140   identifies the JVM platform.  Since a particular Java version is
   141   always bundled with Isabelle, the resulting settings also provide
   142   some clues about its platform, without running it.
   143 
   144 * Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are
   145   notoriously non-portable an should be avoided.