|
1 Multi-platform support of Isabelle |
|
2 ================================== |
|
3 |
|
4 Preamble |
|
5 -------- |
|
6 |
|
7 The general programming model is that of a stylized ML + Scala + POSIX |
|
8 environment, with a minimum of system-specific code in user-space |
|
9 tools. |
|
10 |
|
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 |
|
13 functions like Isabelle_System.bash. The settings environment also |
|
14 provides some means for portability, e.g. the bash function |
|
15 "platform_path" to keep the impression that Windows/Cygwin adheres to |
|
16 Isabelle/POSIX standards, although Poly/ML and the JVM are native on |
|
17 Windows. |
|
18 |
|
19 When producing add-on tools, it is important to stay within this clean |
|
20 room of Isabelle, and refrain from non-portable access to operating |
|
21 system functions. The Isabelle environment uses peculiar scripts for |
|
22 GNU bash and perl as system glue: this style should be observed as far |
|
23 as possible. |
|
24 |
|
25 |
|
26 Supported platforms |
|
27 ------------------- |
|
28 |
|
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): |
|
35 |
|
36 x86_64-linux Ubuntu 16.04 LTS |
|
37 |
|
38 x86_64-darwin macOS 10.13 High Sierra (lapbroy68 MacBookPro11,2) |
|
39 macOS 10.14 Mojave (mini2 Macmini8,1) |
|
40 macOS 10.15 Catalina (laramac01 Macmini8,1) |
|
41 macOS 11.1 Big Sur (mini1 Macmini8,1) |
|
42 |
|
43 x86_64-windows Windows 10 |
|
44 x86_64-cygwin Cygwin 3.1.x https://isabelle.sketis.net/cygwin_2021 (x86_64/release) |
|
45 |
|
46 New (experimental): |
|
47 |
|
48 arm64-linux Raspberry Pi OS 64bit beta (Debian 10 / Buster) |
|
49 |
|
50 arm64-darwin macOS 11.1 Big Sur |
|
51 |
|
52 |
|
53 64 bit vs. 32 bit platform personality |
|
54 -------------------------------------- |
|
55 |
|
56 Isabelle requires 64 bit hardware running a 64 bit operating |
|
57 system. Only Windows still supports native x86 executables, but the |
|
58 POSIX emulation on Windows via Cygwin64 works exclusively for x86_64. |
|
59 |
|
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: |
|
64 |
|
65 ISABELLE_WINDOWS_PLATFORM64 |
|
66 ISABELLE_WINDOWS_PLATFORM32 |
|
67 |
|
68 These are always empty on Linux and macOS, and non-empty on |
|
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}" |
|
73 |
|
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}" |
|
78 |
|
79 |
|
80 Dependable system tools |
|
81 ----------------------- |
|
82 |
|
83 The following portable system tools can be taken for granted: |
|
84 |
|
85 * Scala on top of Java. Isabelle/Scala irons out many oddities and |
|
86 portability issues of the Java platform. |
|
87 |
|
88 * GNU bash as uniform shell on all platforms. The POSIX "standard" |
|
89 shell /bin/sh does *not* work portably -- there are too many |
|
90 non-standard implementations of it. On Debian and Ubuntu /bin/sh is |
|
91 actually /bin/dash and introduces many oddities. |
|
92 |
|
93 * Perl as largely portable system programming language, with its |
|
94 fairly robust support for processes, signals, sockets etc. |
|
95 |
|
96 |
|
97 Known problems |
|
98 -------------- |
|
99 |
|
100 * macOS: If MacPorts is installed there is some danger that |
|
101 accidental references to its shared libraries are created |
|
102 (e.g. libgmp). Use otool -L to check if compiled binaries also work |
|
103 without MacPorts. |
|
104 |
|
105 * macOS: If MacPorts is installed and its version of Perl takes |
|
106 precedence over /usr/bin/perl in the PATH, then the end-user needs |
|
107 to take care of installing extra modules, e.g. for HTTP support. |
|
108 Such add-ons are usually included in Apple's /usr/bin/perl by |
|
109 default. |
|
110 |
|
111 * Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are |
|
112 notoriously non-portable an should be avoided. |
|
113 |
|
114 * The traditional "uname" Unix tool only tells about its own executable |
|
115 format, not the underlying platform! |