Admin/PLATFORMS
author blanchet
Tue Nov 07 15:16:41 2017 +0100 (19 months ago)
changeset 67021 41f1f8c4259b
parent 66911 d122c24a93d6
child 67088 89e82aed7813
permissions -rw-r--r--
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
     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 low-level access to the operating
    21 system. The Isabelle environment uses peculiar scripts for GNU bash and
    22 perl to get the plumbing right. This style should be imitated as far as
    23 possible.
    24 
    25 
    26 Supported platforms
    27 -------------------
    28 
    29 The following hardware and operating system platforms are officially
    30 supported by the Isabelle distribution (and bundled tools), with the
    31 following base-line versions (which have been selected to be neither
    32 too old nor too new):
    33 
    34   x86_64-linux      Ubuntu 12.04 LTS
    35 
    36   x86_64-darwin     Mac OS X 10.9 Mavericks (macbroy2 MacPro4,1)
    37                     Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2)
    38                     Mac OS X 10.11 El Capitan (?)
    39                     macOS 10.12 Sierra (macbroy30 MacBookPro6,2)
    40 
    41   x86_64-windows    Windows 7
    42   x86_64-cygwin     Cygwin 2.8 http://isabelle.in.tum.de/cygwin_2017 (x86_64/release)
    43 
    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 
    47 Fringe platforms like BSD or Solaris are not supported.
    48 
    49 
    50 64 bit vs. 32 bit platform personality
    51 --------------------------------------
    52 
    53 Isabelle requires 64 bit hardware running a 64 bit operating. Windows
    54 and Mac OS X allow x86 executables as well, but for Linux this requires
    55 separate installation of 32 bit shared libraries. The POSIX emulation on
    56 Windows via Cygwin64 is exclusively for x86_64.
    57 
    58 ML works both for x86_64 and x86, and the latter is preferred for space
    59 and performance reasons. Java is always for x86_64 on all platforms.
    60 
    61 Add-on executables are expected to work without manual user
    62 configuration. Each component settings script needs to determine the
    63 platform details appropriately.
    64 
    65 
    66 The Isabelle settings environment provides the following variables to
    67 help configuring platform-dependent tools:
    68 
    69   ISABELLE_PLATFORM64  (potentially empty)
    70   ISABELLE_PLATFORM32  (potentially empty)
    71   ISABELLE_PLATFORM
    72 
    73 The ISABELLE_PLATFORM setting variable prefers the 32 bit personality of
    74 the platform, if possible. Using regular bash notation, tools may
    75 express their preference for 64 bit with a fall-back for 32 bit as
    76 follows:
    77 
    78   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
    79 
    80 
    81 There is a second set of settings for native Windows (instead of the
    82 POSIX emulation of Cygwin used before):
    83 
    84   ISABELLE_WINDOWS_PLATFORM64
    85   ISABELLE_WINDOWS_PLATFORM32
    86   ISABELLE_WINDOWS_PLATFORM
    87 
    88 It can be used like this:
    89 
    90   "${ISABELLE_WINDOWS_PLATFORM:-$ISABELLE_PLATFORM}"
    91 
    92   "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"
    93 
    94 
    95 Dependable system tools
    96 -----------------------
    97 
    98 The following portable system tools can be taken for granted:
    99 
   100 * Scala on top of Java 8.  Isabelle/Scala irons out many oddities and
   101   portability issues of the Java platform.
   102 
   103 * GNU bash as uniform shell on all platforms. The POSIX "standard" shell
   104   /bin/sh does *not* work -- there are too many non-standard
   105   implementations of it. On Debian and Ubuntu /bin/sh is actually
   106   /bin/dash and thus introduces many oddities.
   107 
   108 * Perl as largely portable system programming language, with its
   109   fairly robust support for processes, signals, sockets etc.
   110 
   111 
   112 Known problems
   113 --------------
   114 
   115 * Mac OS X: If MacPorts is installed there is some danger that
   116   accidental references to its shared libraries are created
   117   (e.g. libgmp).  Use otool -L to check if compiled binaries also work
   118   without MacPorts.
   119 
   120 * Mac OS X: If MacPorts is installed and its version of Perl takes
   121   precedence over /usr/bin/perl in the PATH, then the end-user needs
   122   to take care of installing extra modules, e.g. for HTTP support.
   123   Such add-ons are usually included in Apple's /usr/bin/perl by
   124   default.
   125 
   126 * The Java runtime has its own idea about the underlying platform, which
   127   affects Java native libraries in particular. In Isabelle/Scala the
   128   function isabelle.Platform.jvm_platform identifies the JVM platform.
   129   In the settings environment, ISABELLE_JAVA_PLATFORM provides the same
   130   information without running the JVM.
   131 
   132 * Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are
   133   notoriously non-portable an should be avoided.
   134 
   135 * The traditional "uname" Unix tool only tells about its own executable
   136   format, not the underlying platform!