Admin/PLATFORMS
author wenzelm
Wed Nov 07 14:06:43 2018 +0100 (8 months ago)
changeset 69254 9f8d26b8c731
parent 69244 264002272392
child 69309 283837b0b8b9
permissions -rw-r--r--
merged
     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 a minimum of system-specific code in user-space
     9 tools.
    10 
    11 The Isabelle system infrastructure provides some facilities to make
    12 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 non-portable access to operating
    21 system functions. The Isabelle environment uses peculiar scripts for
    22 GNU bash and perl as system glue: this style should be observed as far
    23 as 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.10 Yosemite (macbroy31 MacBookPro6,2)
    37                     Mac OS X 10.11 El Capitan (macbroy2 MacPro4,1)
    38                     macOS 10.12 Sierra (macbroy30 MacBookPro6,2)
    39                     macOS 10.13 High Sierra (!?)
    40                     macOS 10.14 Mojave (lapnipkow3 MacBookPro9,2)
    41 
    42   x86_64-windows    Windows 7
    43   x86_64-cygwin     Cygwin 2.10 https://isabelle.sketis.net/cygwin_2018 (x86_64/release)
    44 
    45 All of the above platforms are 100% supported by Isabelle -- end-users
    46 should not have to care about the differences (at least in theory).
    47 
    48 Exotic platforms like BSD, Solaris, NixOS are not supported.
    49 
    50 
    51 64 bit vs. 32 bit platform personality
    52 --------------------------------------
    53 
    54 Isabelle requires 64 bit hardware running a 64 bit operating
    55 system. Windows and Mac OS X allow x86 executables as well, but for
    56 Linux this requires separate installation of 32 bit shared
    57 libraries. The POSIX emulation on Windows via Cygwin64 works
    58 exclusively for x86_64.
    59 
    60 Poly/ML supports both for x86_64 and x86, and the latter is preferred
    61 for space and performance reasons. Java is always the x86_64 version
    62 on all platforms.
    63 
    64 Add-on executables are expected to work without manual user
    65 configuration. Each component settings script needs to determine the
    66 platform details appropriately.
    67 
    68 
    69 The Isabelle settings environment provides the following important
    70 variables to help configuring platform-dependent tools:
    71 
    72   ISABELLE_PLATFORM64  (potentially empty)
    73   ISABELLE_PLATFORM32  (potentially empty)
    74 
    75 Each can be empty, but not both at the same time. Using GNU bash
    76 notation, tools may express their platform preference, e.g. first 64
    77 bit and second 32 bit, or the opposite:
    78 
    79   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
    80   "${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}"
    81 
    82 
    83 There is a another set of settings for native Windows (instead of the
    84 POSIX emulation of Cygwin used before):
    85 
    86   ISABELLE_WINDOWS_PLATFORM64
    87   ISABELLE_WINDOWS_PLATFORM32
    88 
    89 These are always empty on Linux and Mac OS X, and non-empty on
    90 Windows. They can be used like this to prefer native Windows and then
    91 Unix (first 64 bit second 32 bit):
    92 
    93   "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"
    94 
    95 
    96 Dependable system tools
    97 -----------------------
    98 
    99 The following portable system tools can be taken for granted:
   100 
   101 * Scala on top of Java.  Isabelle/Scala irons out many oddities and
   102   portability issues of the Java platform.
   103 
   104 * GNU bash as uniform shell on all platforms. The POSIX "standard"
   105   shell /bin/sh does *not* work portably -- there are too many
   106   non-standard implementations of it. On Debian and Ubuntu /bin/sh is
   107   actually /bin/dash and introduces many oddities.
   108 
   109 * Perl as largely portable system programming language, with its
   110   fairly robust support for processes, signals, sockets etc.
   111 
   112 
   113 Known problems
   114 --------------
   115 
   116 * Mac OS X: If MacPorts is installed there is some danger that
   117   accidental references to its shared libraries are created
   118   (e.g. libgmp).  Use otool -L to check if compiled binaries also work
   119   without MacPorts.
   120 
   121 * Mac OS X: If MacPorts is installed and its version of Perl takes
   122   precedence over /usr/bin/perl in the PATH, then the end-user needs
   123   to take care of installing extra modules, e.g. for HTTP support.
   124   Such add-ons are usually included in Apple's /usr/bin/perl by
   125   default.
   126 
   127 * Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are
   128   notoriously non-portable an should be avoided.
   129 
   130 * The traditional "uname" Unix tool only tells about its own executable
   131   format, not the underlying platform!