author | wenzelm |
Sun, 04 Feb 2024 21:51:30 +0100 | |
changeset 79573 | 0e7dd3eaa6e8 |
parent 79563 | 76ad72736e9e |
child 79591 | 6e5f40cfa877 |
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 |
|
78773 | 36 |
x86_64-linux Ubuntu 18.04 LTS |
35610 | 37 |
|
78777
3b424f9cd5eb
update platforms: discontinue macOS 10.13 High Sierra, macOS 10.14 Mojave, macOS 10.15 Catalina;
wenzelm
parents:
78773
diff
changeset
|
38 |
x86_64-darwin macOS 11 Big Sur (mini1 Macmini8,1) |
3b424f9cd5eb
update platforms: discontinue macOS 10.13 High Sierra, macOS 10.14 Mojave, macOS 10.15 Catalina;
wenzelm
parents:
78773
diff
changeset
|
39 |
macOS 12 Monterey (???) |
78484 | 40 |
macOS 13 Ventura (mini3 Mac14,12 -- MacMini M2 Pro, 6+4 cores) |
78771
d7f4c5c7bebb
more platform tests: initial support for macOS 14 Sonoma;
wenzelm
parents:
78743
diff
changeset
|
41 |
macOS 14 Sonoma (mini2 Macmini8,1) |
72366 | 42 |
|
78484 | 43 |
arm64-darwin macOS 11 Big Sur (assur Macmini9,1 -- MacMini M1, 4+4 cores) |
76375
089e546f671f
more macOS platforms, without reference hardware;
wenzelm
parents:
76028
diff
changeset
|
44 |
macOS 12 Monterey (???) |
78484 | 45 |
macOS 13 Ventura (mini3 Mac14,12 -- MacMini M2 Pro, 6+4 cores) |
78771
d7f4c5c7bebb
more platform tests: initial support for macOS 14 Sonoma;
wenzelm
parents:
78743
diff
changeset
|
46 |
macOS 14 Sonoma (studio1 Mac13,2 M1 Ultra, 16+4 cores) |
73646 | 47 |
|
72526 | 48 |
x86_64-windows Windows 10 |
78304
e4b57eea7f86
update cygwin for Isabelle2023 -- somewhere after cygwin 3.4.0-1 (see https://cygwin.com/pipermail/cygwin-announce/2022-December/010821.html);
wenzelm
parents:
78144
diff
changeset
|
49 |
x86_64-cygwin Cygwin 3.4.x https://isabelle.sketis.net/cygwin_2023 (x86_64/release) |
72366 | 50 |
|
73646 | 51 |
Experimental platforms: |
72359 | 52 |
|
79563
76ad72736e9e
rebuild "verit" for arm64-linux for more robustness, e.g. relevant for theory "HOL-ex.BigO";
wenzelm
parents:
78777
diff
changeset
|
53 |
arm64-linux Ubuntu 18.04 LTS (e.g. via "docker run -it ubuntu:20.04 bash") |
36204 | 54 |
|
55 |
||
66911 | 56 |
64 bit vs. 32 bit platform personality |
57 |
-------------------------------------- |
|
36204 | 58 |
|
67235 | 59 |
Isabelle requires 64 bit hardware running a 64 bit operating |
72895 | 60 |
system. Only Windows still supports native x86 executables, but the |
61 |
POSIX emulation on Windows via Cygwin64 works exclusively for x86_64. |
|
65073 | 62 |
|
72895 | 63 |
The Isabelle settings environment provides variable |
64 |
ISABELLE_PLATFORM64 to refer to the standard platform personality. On |
|
65 |
Windows this is for Cygwin64, but the following native platform |
|
66 |
identifiers are available as well: |
|
65073 | 67 |
|
66732 | 68 |
ISABELLE_WINDOWS_PLATFORM64 |
65073 | 69 |
ISABELLE_WINDOWS_PLATFORM32 |
70 |
||
72894
bd2269b6cd99
updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents:
72526
diff
changeset
|
71 |
These are always empty on Linux and macOS, and non-empty on |
72895 | 72 |
Windows. For example, this is how to refer to native Windows and |
73 |
fall-back on Unix (always 64 bit): |
|
74 |
||
75 |
"${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}" |
|
65073 | 76 |
|
72895 | 77 |
And this is for old 32 bit executables on Windows, but still 64 bit on |
78 |
Unix: |
|
79 |
||
80 |
"${ISABELLE_WINDOWS_PLATFORM32:-$ISABELLE_PLATFORM64}" |
|
65073 | 81 |
|
73646 | 82 |
For Apple Silicon the native platform is "$ISABELLE_APPLE_PLATFORM64" |
83 |
(arm64-darwin), but thanks to Rosetta 2 "$ISABELLE_PLATFORM64" |
|
84 |
(x64_64-darwin) works routinely with fairly good performance. |
|
85 |
||
65073 | 86 |
|
35610 | 87 |
Dependable system tools |
88 |
----------------------- |
|
89 |
||
90 |
The following portable system tools can be taken for granted: |
|
91 |
||
73646 | 92 |
* Scala on top of Java. Isabelle/Scala irons out many fine points of |
93 |
the Java platform to make it fully portable as described above. |
|
64339 | 94 |
|
68002 | 95 |
* GNU bash as uniform shell on all platforms. The POSIX "standard" |
96 |
shell /bin/sh does *not* work portably -- there are too many |
|
97 |
non-standard implementations of it. On Debian and Ubuntu /bin/sh is |
|
98 |
actually /bin/dash and introduces many oddities. |
|
35610 | 99 |
|
100 |
||
101 |
Known problems |
|
102 |
-------------- |
|
103 |
||
73646 | 104 |
* macOS: If Homebrew or MacPorts is installed, there is some danger |
105 |
that accidental references to its shared libraries are created |
|
41668 | 106 |
(e.g. libgmp). Use otool -L to check if compiled binaries also work |
107 |
without MacPorts. |
|
108 |
||
55438 | 109 |
* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are |
64339 | 110 |
notoriously non-portable an should be avoided. |
66911 | 111 |
|
73646 | 112 |
* The traditional "uname" Unix tool only tells about its own |
113 |
executable format, not the underlying platform! |