author | wenzelm |
Sat, 03 Oct 2020 13:59:56 +0200 | |
changeset 72366 | ed99d0f9b536 |
parent 72359 | 9af8124f7f0d |
child 72371 | 3e84f4e9651a |
permissions | -rw-r--r-- |
64339 | 1 |
Multi-platform support of Isabelle |
2 |
================================== |
|
35610 | 3 |
|
4 |
Preamble |
|
5 |
-------- |
|
6 |
||
7 |
The general programming model is that of a stylized ML + Scala + POSIX |
|
68002 | 8 |
environment, with a minimum of system-specific code in user-space |
9 |
tools. |
|
35610 | 10 |
|
67235 | 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 |
|
48833 | 13 |
functions like Isabelle_System.bash. The settings environment also |
61294 | 14 |
provides some means for portability, e.g. the bash function |
15 |
"platform_path" to keep the impression that Windows/Cygwin adheres to |
|
64339 | 16 |
Isabelle/POSIX standards, although Poly/ML and the JVM are native on |
17 |
Windows. |
|
35610 | 18 |
|
19 |
When producing add-on tools, it is important to stay within this clean |
|
67235 | 20 |
room of Isabelle, and refrain from non-portable access to operating |
21 |
system functions. The Isabelle environment uses peculiar scripts for |
|
68002 | 22 |
GNU bash and perl as system glue: this style should be observed as far |
23 |
as possible. |
|
35610 | 24 |
|
25 |
||
26 |
Supported platforms |
|
27 |
------------------- |
|
28 |
||
72366 | 29 |
A broad range of hardware and operating system platforms are supported |
30 |
by building executables on base-line versions that are neither too old |
|
31 |
nor too new. Common OS families work: Linux, Windows, macOS, but |
|
32 |
exotic ones are unsupported: BSD, Solaris, NixOS. |
|
33 |
||
34 |
Official (full support): |
|
35610 | 35 |
|
69725 | 36 |
x86_64-linux Ubuntu 14.04 LTS |
35610 | 37 |
|
72366 | 38 |
x86_64-darwin macOS 10.13 High Sierra (lapbroy68 MacBookPro11,2) |
39 |
macOS 10.14 Mojave (lapnipkow3 MacBookPro9,2) |
|
40 |
macOS 10.15 Catalina (laramac01 Macmini8,1) |
|
41 |
||
42 |
x86_64-windows Windows 7 |
|
43 |
x86_64-cygwin Cygwin 3.1.x https://isabelle.sketis.net/cygwin_2021 (x86_64/release) |
|
44 |
||
45 |
Old (partial support): |
|
46 |
||
67088 | 47 |
x86_64-darwin Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2) |
48 |
Mac OS X 10.11 El Capitan (macbroy2 MacPro4,1) |
|
65369
27c1b5e952bd
macbroy30 is on 10.12 Sierra (already since 04-Mar-2017) -- discontinued support for 10.8 Mountain Lion;
wenzelm
parents:
65073
diff
changeset
|
49 |
macOS 10.12 Sierra (macbroy30 MacBookPro6,2) |
48833 | 50 |
|
72366 | 51 |
New (experimental): |
72359 | 52 |
|
53 |
arm64-linux Ubuntu 20.04 LTS |
|
54 |
||
36204 | 55 |
|
56 |
||
66911 | 57 |
64 bit vs. 32 bit platform personality |
58 |
-------------------------------------- |
|
36204 | 59 |
|
67235 | 60 |
Isabelle requires 64 bit hardware running a 64 bit operating |
61 |
system. Windows and Mac OS X allow x86 executables as well, but for |
|
62 |
Linux this requires separate installation of 32 bit shared |
|
68002 | 63 |
libraries. The POSIX emulation on Windows via Cygwin64 works |
64 |
exclusively for x86_64. |
|
66911 | 65 |
|
68002 | 66 |
Poly/ML supports both for x86_64 and x86, and the latter is preferred |
67 |
for space and performance reasons. Java is always the x86_64 version |
|
68 |
on all platforms. |
|
48833 | 69 |
|
49144 | 70 |
Add-on executables are expected to work without manual user |
66911 | 71 |
configuration. Each component settings script needs to determine the |
49144 | 72 |
platform details appropriately. |
48833 | 73 |
|
65073 | 74 |
|
68002 | 75 |
The Isabelle settings environment provides the following important |
76 |
variables to help configuring platform-dependent tools: |
|
48833 | 77 |
|
78 |
ISABELLE_PLATFORM64 (potentially empty) |
|
66691 | 79 |
ISABELLE_PLATFORM32 (potentially empty) |
36204 | 80 |
|
68002 | 81 |
Each can be empty, but not both at the same time. Using GNU bash |
82 |
notation, tools may express their platform preference, e.g. first 64 |
|
83 |
bit and second 32 bit, or the opposite: |
|
48833 | 84 |
|
85 |
"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}" |
|
68002 | 86 |
"${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}" |
36204 | 87 |
|
65073 | 88 |
|
68002 | 89 |
There is a another set of settings for native Windows (instead of the |
65073 | 90 |
POSIX emulation of Cygwin used before): |
91 |
||
66732 | 92 |
ISABELLE_WINDOWS_PLATFORM64 |
65073 | 93 |
ISABELLE_WINDOWS_PLATFORM32 |
94 |
||
68002 | 95 |
These are always empty on Linux and Mac OS X, and non-empty on |
96 |
Windows. They can be used like this to prefer native Windows and then |
|
97 |
Unix (first 64 bit second 32 bit): |
|
65073 | 98 |
|
99 |
"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}" |
|
100 |
||
101 |
||
35610 | 102 |
Dependable system tools |
103 |
----------------------- |
|
104 |
||
105 |
The following portable system tools can be taken for granted: |
|
106 |
||
68002 | 107 |
* Scala on top of Java. Isabelle/Scala irons out many oddities and |
64339 | 108 |
portability issues of the Java platform. |
109 |
||
68002 | 110 |
* GNU bash as uniform shell on all platforms. The POSIX "standard" |
111 |
shell /bin/sh does *not* work portably -- there are too many |
|
112 |
non-standard implementations of it. On Debian and Ubuntu /bin/sh is |
|
113 |
actually /bin/dash and introduces many oddities. |
|
35610 | 114 |
|
58780
1f8c0da85664
discontinued python from standard system environment;
wenzelm
parents:
55438
diff
changeset
|
115 |
* Perl as largely portable system programming language, with its |
1f8c0da85664
discontinued python from standard system environment;
wenzelm
parents:
55438
diff
changeset
|
116 |
fairly robust support for processes, signals, sockets etc. |
35610 | 117 |
|
118 |
||
119 |
Known problems |
|
120 |
-------------- |
|
121 |
||
55391
eae296b5ef33
Mac OS X Lion (macbroy6) is baseline for portable executables;
wenzelm
parents:
49144
diff
changeset
|
122 |
* Mac OS X: If MacPorts is installed there is some danger that |
41668 | 123 |
accidental references to its shared libraries are created |
124 |
(e.g. libgmp). Use otool -L to check if compiled binaries also work |
|
125 |
without MacPorts. |
|
126 |
||
55391
eae296b5ef33
Mac OS X Lion (macbroy6) is baseline for portable executables;
wenzelm
parents:
49144
diff
changeset
|
127 |
* Mac OS X: If MacPorts is installed and its version of Perl takes |
35610 | 128 |
precedence over /usr/bin/perl in the PATH, then the end-user needs |
36204 | 129 |
to take care of installing extra modules, e.g. for HTTP support. |
130 |
Such add-ons are usually included in Apple's /usr/bin/perl by |
|
131 |
default. |
|
35610 | 132 |
|
55438 | 133 |
* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are |
64339 | 134 |
notoriously non-portable an should be avoided. |
66911 | 135 |
|
136 |
* The traditional "uname" Unix tool only tells about its own executable |
|
137 |
format, not the underlying platform! |