author | wenzelm |
Sun, 13 Dec 2020 13:39:36 +0100 | |
changeset 72895 | dc9f43a9ad23 |
parent 72894 | bd2269b6cd99 |
child 73141 | 13bd167f4d97 |
child 73155 | d63c6fcccff2 |
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) |
72390 | 39 |
macOS 10.14 Mojave (mini2 Macmini8,1) |
72366 | 40 |
macOS 10.15 Catalina (laramac01 Macmini8,1) |
41 |
||
72526 | 42 |
x86_64-windows Windows 10 |
72366 | 43 |
x86_64-cygwin Cygwin 3.1.x https://isabelle.sketis.net/cygwin_2021 (x86_64/release) |
44 |
||
45 |
New (experimental): |
|
72359 | 46 |
|
72371
3e84f4e9651a
clarified arm64-linux base line: prefer Pi OS, which is based on slightly older Debian;
wenzelm
parents:
72366
diff
changeset
|
47 |
arm64-linux Raspberry Pi OS 64bit beta (Debian 10 / Buster) |
36204 | 48 |
|
72895 | 49 |
x86_64-darwin macOS 11 Big Sur |
50 |
||
36204 | 51 |
|
66911 | 52 |
64 bit vs. 32 bit platform personality |
53 |
-------------------------------------- |
|
36204 | 54 |
|
67235 | 55 |
Isabelle requires 64 bit hardware running a 64 bit operating |
72895 | 56 |
system. Only Windows still supports native x86 executables, but the |
57 |
POSIX emulation on Windows via Cygwin64 works exclusively for x86_64. |
|
65073 | 58 |
|
72895 | 59 |
The Isabelle settings environment provides variable |
60 |
ISABELLE_PLATFORM64 to refer to the standard platform personality. On |
|
61 |
Windows this is for Cygwin64, but the following native platform |
|
62 |
identifiers are available as well: |
|
65073 | 63 |
|
66732 | 64 |
ISABELLE_WINDOWS_PLATFORM64 |
65073 | 65 |
ISABELLE_WINDOWS_PLATFORM32 |
66 |
||
72894
bd2269b6cd99
updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents:
72526
diff
changeset
|
67 |
These are always empty on Linux and macOS, and non-empty on |
72895 | 68 |
Windows. For example, this is how to refer to native Windows and |
69 |
fall-back on Unix (always 64 bit): |
|
70 |
||
71 |
"${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}" |
|
65073 | 72 |
|
72895 | 73 |
And this is for old 32 bit executables on Windows, but still 64 bit on |
74 |
Unix: |
|
75 |
||
76 |
"${ISABELLE_WINDOWS_PLATFORM32:-$ISABELLE_PLATFORM64}" |
|
65073 | 77 |
|
78 |
||
35610 | 79 |
Dependable system tools |
80 |
----------------------- |
|
81 |
||
82 |
The following portable system tools can be taken for granted: |
|
83 |
||
68002 | 84 |
* Scala on top of Java. Isabelle/Scala irons out many oddities and |
64339 | 85 |
portability issues of the Java platform. |
86 |
||
68002 | 87 |
* GNU bash as uniform shell on all platforms. The POSIX "standard" |
88 |
shell /bin/sh does *not* work portably -- there are too many |
|
89 |
non-standard implementations of it. On Debian and Ubuntu /bin/sh is |
|
90 |
actually /bin/dash and introduces many oddities. |
|
35610 | 91 |
|
58780
1f8c0da85664
discontinued python from standard system environment;
wenzelm
parents:
55438
diff
changeset
|
92 |
* Perl as largely portable system programming language, with its |
1f8c0da85664
discontinued python from standard system environment;
wenzelm
parents:
55438
diff
changeset
|
93 |
fairly robust support for processes, signals, sockets etc. |
35610 | 94 |
|
95 |
||
96 |
Known problems |
|
97 |
-------------- |
|
98 |
||
72894
bd2269b6cd99
updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents:
72526
diff
changeset
|
99 |
* macOS: If MacPorts is installed there is some danger that |
41668 | 100 |
accidental references to its shared libraries are created |
101 |
(e.g. libgmp). Use otool -L to check if compiled binaries also work |
|
102 |
without MacPorts. |
|
103 |
||
72894
bd2269b6cd99
updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents:
72526
diff
changeset
|
104 |
* macOS: If MacPorts is installed and its version of Perl takes |
35610 | 105 |
precedence over /usr/bin/perl in the PATH, then the end-user needs |
36204 | 106 |
to take care of installing extra modules, e.g. for HTTP support. |
107 |
Such add-ons are usually included in Apple's /usr/bin/perl by |
|
108 |
default. |
|
35610 | 109 |
|
55438 | 110 |
* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are |
64339 | 111 |
notoriously non-portable an should be avoided. |
66911 | 112 |
|
113 |
* The traditional "uname" Unix tool only tells about its own executable |
|
114 |
format, not the underlying platform! |