1Multi-platform support of Isabelle 2================================== 3 4Preamble 5-------- 6 7The general programming model is that of a stylized ML + Scala + POSIX 8environment, with a minimum of system-specific code in user-space 9tools. 10 11The Isabelle system infrastructure provides some facilities to make 12this work, e.g. see the ML and Scala modules File and Path, or 13functions like Isabelle_System.bash. The settings environment also 14provides some means for portability, e.g. the bash function 15"platform_path" to keep the impression that Windows/Cygwin adheres to 16Isabelle/POSIX standards, although Poly/ML and the JVM are native on 17Windows. 18 19When producing add-on tools, it is important to stay within this clean 20room of Isabelle, and refrain from non-portable access to operating 21system functions. The Isabelle environment uses peculiar scripts for 22GNU bash and perl as system glue: this style should be observed as far 23as possible. 24 25 26Supported platforms 27------------------- 28 29The following hardware and operating system platforms are officially 30supported by the Isabelle distribution (and bundled tools), with the 31following base-line versions (which have been selected to be neither 32too 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 41 x86_64-windows Windows 7 42 x86_64-cygwin Cygwin 2.10 https://isabelle.sketis.net/cygwin_2018 (x86_64/release) 43 44All of the above platforms are 100% supported by Isabelle -- end-users 45should not have to care about the differences (at least in theory). 46 47Exotic platforms like BSD, Solaris, NixOS are not supported. 48 49 5064 bit vs. 32 bit platform personality 51-------------------------------------- 52 53Isabelle requires 64 bit hardware running a 64 bit operating 54system. Windows and Mac OS X allow x86 executables as well, but for 55Linux this requires separate installation of 32 bit shared 56libraries. The POSIX emulation on Windows via Cygwin64 works 57exclusively for x86_64. 58 59Poly/ML supports both for x86_64 and x86, and the latter is preferred 60for space and performance reasons. Java is always the x86_64 version 61on all platforms. 62 63Add-on executables are expected to work without manual user 64configuration. Each component settings script needs to determine the 65platform details appropriately. 66 67 68The Isabelle settings environment provides the following important 69variables to help configuring platform-dependent tools: 70 71 ISABELLE_PLATFORM64 (potentially empty) 72 ISABELLE_PLATFORM32 (potentially empty) 73 74Each can be empty, but not both at the same time. Using GNU bash 75notation, tools may express their platform preference, e.g. first 64 76bit and second 32 bit, or the opposite: 77 78 "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}" 79 "${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}" 80 81 82There is a another set of settings for native Windows (instead of the 83POSIX emulation of Cygwin used before): 84 85 ISABELLE_WINDOWS_PLATFORM64 86 ISABELLE_WINDOWS_PLATFORM32 87 88These are always empty on Linux and Mac OS X, and non-empty on 89Windows. They can be used like this to prefer native Windows and then 90Unix (first 64 bit second 32 bit): 91 92 "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}" 93 94 95Dependable system tools 96----------------------- 97 98The following portable system tools can be taken for granted: 99 100* Scala on top of Java. 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" 104 shell /bin/sh does *not* work portably -- there are too many 105 non-standard implementations of it. On Debian and Ubuntu /bin/sh is 106 actually /bin/dash and 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 112Known 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* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are 127 notoriously non-portable an should be avoided. 128 129* The traditional "uname" Unix tool only tells about its own executable 130 format, not the underlying platform! 131