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