author | wenzelm |
Fri, 07 May 2021 16:45:49 +0200 | |
changeset 73646 | 078ad17eb934 |
parent 73645 | dea7f6a2485e |
child 74063 | ff466b272267 |
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 |
|
73646 | 16 |
Isabelle/POSIX standards, although many executables are native on |
17 |
Windows (notably Poly/ML and Java). |
|
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 |
73646 | 21 |
system functions. The Isabelle environment uses GNU bash and |
22 |
Isabelle/Scala as portable system infrastructure, using somewhat |
|
23 |
peculiar implementation techniques. |
|
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 |
|
73646 | 31 |
nor too new. Common OS families should work: Linux, macOS, |
32 |
Windows. More exotic platforms are unsupported: NixOS, BSD, Solaris. |
|
72366 | 33 |
|
73646 | 34 |
Official platforms: |
35610 | 35 |
|
73598 | 36 |
x86_64-linux Ubuntu 16.04 LTS |
35610 | 37 |
|
72366 | 38 |
x86_64-darwin macOS 10.13 High Sierra (lapbroy68 MacBookPro11,2) |
72390 | 39 |
macOS 10.14 Mojave (mini2 Macmini8,1) |
72366 | 40 |
macOS 10.15 Catalina (laramac01 Macmini8,1) |
73142 | 41 |
macOS 11.1 Big Sur (mini1 Macmini8,1) |
72366 | 42 |
|
73646 | 43 |
arm64-darwin macOS 11.1 Big Sur |
44 |
||
72526 | 45 |
x86_64-windows Windows 10 |
72366 | 46 |
x86_64-cygwin Cygwin 3.1.x https://isabelle.sketis.net/cygwin_2021 (x86_64/release) |
47 |
||
73646 | 48 |
Experimental platforms: |
72359 | 49 |
|
72371
3e84f4e9651a
clarified arm64-linux base line: prefer Pi OS, which is based on slightly older Debian;
wenzelm
parents:
72366
diff
changeset
|
50 |
arm64-linux Raspberry Pi OS 64bit beta (Debian 10 / Buster) |
36204 | 51 |
|
52 |
||
66911 | 53 |
64 bit vs. 32 bit platform personality |
54 |
-------------------------------------- |
|
36204 | 55 |
|
67235 | 56 |
Isabelle requires 64 bit hardware running a 64 bit operating |
72895 | 57 |
system. Only Windows still supports native x86 executables, but the |
58 |
POSIX emulation on Windows via Cygwin64 works exclusively for x86_64. |
|
65073 | 59 |
|
72895 | 60 |
The Isabelle settings environment provides variable |
61 |
ISABELLE_PLATFORM64 to refer to the standard platform personality. On |
|
62 |
Windows this is for Cygwin64, but the following native platform |
|
63 |
identifiers are available as well: |
|
65073 | 64 |
|
66732 | 65 |
ISABELLE_WINDOWS_PLATFORM64 |
65073 | 66 |
ISABELLE_WINDOWS_PLATFORM32 |
67 |
||
72894
bd2269b6cd99
updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents:
72526
diff
changeset
|
68 |
These are always empty on Linux and macOS, and non-empty on |
72895 | 69 |
Windows. For example, this is how to refer to native Windows and |
70 |
fall-back on Unix (always 64 bit): |
|
71 |
||
72 |
"${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}" |
|
65073 | 73 |
|
72895 | 74 |
And this is for old 32 bit executables on Windows, but still 64 bit on |
75 |
Unix: |
|
76 |
||
77 |
"${ISABELLE_WINDOWS_PLATFORM32:-$ISABELLE_PLATFORM64}" |
|
65073 | 78 |
|
73646 | 79 |
For Apple Silicon the native platform is "$ISABELLE_APPLE_PLATFORM64" |
80 |
(arm64-darwin), but thanks to Rosetta 2 "$ISABELLE_PLATFORM64" |
|
81 |
(x64_64-darwin) works routinely with fairly good performance. |
|
82 |
||
65073 | 83 |
|
35610 | 84 |
Dependable system tools |
85 |
----------------------- |
|
86 |
||
87 |
The following portable system tools can be taken for granted: |
|
88 |
||
73646 | 89 |
* Scala on top of Java. Isabelle/Scala irons out many fine points of |
90 |
the Java platform to make it fully portable as described above. |
|
64339 | 91 |
|
68002 | 92 |
* GNU bash as uniform shell on all platforms. The POSIX "standard" |
93 |
shell /bin/sh does *not* work portably -- there are too many |
|
94 |
non-standard implementations of it. On Debian and Ubuntu /bin/sh is |
|
95 |
actually /bin/dash and introduces many oddities. |
|
35610 | 96 |
|
97 |
||
98 |
Known problems |
|
99 |
-------------- |
|
100 |
||
73646 | 101 |
* macOS: If Homebrew or MacPorts is installed, there is some danger |
102 |
that accidental references to its shared libraries are created |
|
41668 | 103 |
(e.g. libgmp). Use otool -L to check if compiled binaries also work |
104 |
without MacPorts. |
|
105 |
||
55438 | 106 |
* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are |
64339 | 107 |
notoriously non-portable an should be avoided. |
66911 | 108 |
|
73646 | 109 |
* The traditional "uname" Unix tool only tells about its own |
110 |
executable format, not the underlying platform! |