author | wenzelm |
Mon, 28 Aug 2017 19:06:00 +0200 | |
changeset 66529 | f39e01e9c489 |
parent 65369 | 27c1b5e952bd |
child 66691 | a8703e8ee1d3 |
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 |
|
48833 | 8 |
environment, with as little system-specific code in user-space tools |
9 |
as possible. |
|
35610 | 10 |
|
11 |
The basic Isabelle system infrastructure provides some facilities to |
|
48833 | 12 |
make this work, e.g. see the ML and Scala modules File and Path, or |
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 |
|
20 |
room of Isabelle, and refrain from overly ambitious system hacking. |
|
64339 | 21 |
The existing Isabelle bash scripts follow a peculiar style that |
22 |
reflects long years of experience in getting system plumbing right. |
|
35610 | 23 |
|
24 |
||
25 |
Supported platforms |
|
26 |
------------------- |
|
27 |
||
28 |
The following hardware and operating system platforms are officially |
|
36204 | 29 |
supported by the Isabelle distribution (and bundled tools), with the |
64339 | 30 |
following base-line versions (which have been selected to be neither |
36204 | 31 |
too old nor too new): |
35610 | 32 |
|
63520 | 33 |
x86-linux Ubuntu 12.04 LTS |
34 |
x86_64-linux Ubuntu 12.04 LTS |
|
35610 | 35 |
|
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
|
36 |
x86_64-darwin Mac OS X 10.9 Mavericks (macbroy2 MacPro4,1) |
64406
492de9062cd2
more specific hardware information: relevant for ultimate Mac OS X version;
wenzelm
parents:
64402
diff
changeset
|
37 |
Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2) |
64402
4f0acbd97491
latest Mac OS X versions *are* still supported, but presently without formal reference systems;
wenzelm
parents:
64387
diff
changeset
|
38 |
Mac OS X 10.11 El Capitan (?) |
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
|
39 |
macOS 10.12 Sierra (macbroy30 MacBookPro6,2) |
48833 | 40 |
|
64339 | 41 |
x86-windows Windows 7 |
42 |
x86_64-windows Windows 7 |
|
66529
f39e01e9c489
updated to cygwin-20170828, which is close to Cygwin 2.8.2-1;
wenzelm
parents:
65369
diff
changeset
|
43 |
x86-cygwin Cygwin 2.8 http://isabelle.in.tum.de/cygwin_2017 (x86/release) |
36204 | 44 |
|
45 |
All of the above platforms are 100% supported by Isabelle -- end-users |
|
44876 | 46 |
should not have to care about the differences (at least in theory). |
35610 | 47 |
|
64339 | 48 |
Fringe platforms like BSD or Solaris are not supported. |
36204 | 49 |
|
50 |
||
51 |
32 bit vs. 64 bit platforms |
|
52 |
--------------------------- |
|
53 |
||
48833 | 54 |
Most users have 64 bit hardware and are running a 64 bit operating |
55391
eae296b5ef33
Mac OS X Lion (macbroy6) is baseline for portable executables;
wenzelm
parents:
49144
diff
changeset
|
55 |
system by default. For Linux this usually means missing 32 bit shared |
48833 | 56 |
libraries, so native x86_64-linux needs to be used by default, despite |
57 |
its doubled space requirements for Poly/ML heaps. For Mac OS X, the |
|
58 |
x86-darwin personality usually works seamlessly for C/C++ programs, |
|
65073 | 59 |
but the Java platform is always for x86_64-darwin. |
48833 | 60 |
|
49144 | 61 |
Add-on executables are expected to work without manual user |
62 |
configuration. Each component settings script needs to determine the |
|
63 |
platform details appropriately. |
|
48833 | 64 |
|
65073 | 65 |
|
48833 | 66 |
The Isabelle settings environment provides the following variables to |
67 |
help configuring platform-dependent tools: |
|
68 |
||
69 |
ISABELLE_PLATFORM64 (potentially empty) |
|
70 |
ISABELLE_PLATFORM32 |
|
71 |
ISABELLE_PLATFORM |
|
36204 | 72 |
|
73 |
The ISABELLE_PLATFORM setting variable refers to the 32 bit version of |
|
48833 | 74 |
the platform, even on 64 bit hardware. Using regular bash notation, |
75 |
tools may express their preference for 64 bit with a fall-back for 32 |
|
76 |
bit as follows: |
|
77 |
||
78 |
"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}" |
|
36204 | 79 |
|
65073 | 80 |
|
81 |
There is a second set of settings for native Windows (instead of the |
|
82 |
POSIX emulation of Cygwin used before): |
|
83 |
||
84 |
ISABELLE_WINDOWS_PLATFORM64 (potentially empty) |
|
85 |
ISABELLE_WINDOWS_PLATFORM32 |
|
86 |
ISABELLE_WINDOWS_PLATFORM |
|
87 |
||
88 |
It can be used like this: |
|
89 |
||
90 |
"${ISABELLE_WINDOWS_PLATFORM:-$ISABELLE_PLATFORM}" |
|
91 |
||
92 |
"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}" |
|
93 |
||
94 |
||
48833 | 95 |
Moreover note that ML and JVM usually have a different idea of the |
96 |
platform, depending on the respective binaries that are actually run. |
|
64339 | 97 |
Poly/ML 5.6.x performs best in 32 bit mode, even for large |
49144 | 98 |
applications, thanks to its sophisticated heap management. The JVM |
99 |
usually works better in 64 bit mode, which allows its heap to grow |
|
100 |
beyond 2 GB. |
|
36204 | 101 |
|
64339 | 102 |
The traditional "uname" Unix tool only tells about its own executable |
103 |
format, not the underlying platform! |
|
35610 | 104 |
|
105 |
||
106 |
Dependable system tools |
|
107 |
----------------------- |
|
108 |
||
109 |
The following portable system tools can be taken for granted: |
|
110 |
||
64339 | 111 |
* Scala on top of Java 8. Isabelle/Scala irons out many oddities and |
112 |
portability issues of the Java platform. |
|
113 |
||
36204 | 114 |
* GNU bash as uniform shell on all platforms. The POSIX "standard" |
64339 | 115 |
shell /bin/sh does *not* work -- there are too many non-standard |
116 |
implementations of it. |
|
35610 | 117 |
|
58780
1f8c0da85664
discontinued python from standard system environment;
wenzelm
parents:
55438
diff
changeset
|
118 |
* Perl as largely portable system programming language, with its |
1f8c0da85664
discontinued python from standard system environment;
wenzelm
parents:
55438
diff
changeset
|
119 |
fairly robust support for processes, signals, sockets etc. |
35610 | 120 |
|
121 |
||
122 |
Known problems |
|
123 |
-------------- |
|
124 |
||
55391
eae296b5ef33
Mac OS X Lion (macbroy6) is baseline for portable executables;
wenzelm
parents:
49144
diff
changeset
|
125 |
* Mac OS X: If MacPorts is installed there is some danger that |
41668 | 126 |
accidental references to its shared libraries are created |
127 |
(e.g. libgmp). Use otool -L to check if compiled binaries also work |
|
128 |
without MacPorts. |
|
129 |
||
55391
eae296b5ef33
Mac OS X Lion (macbroy6) is baseline for portable executables;
wenzelm
parents:
49144
diff
changeset
|
130 |
* Mac OS X: If MacPorts is installed and its version of Perl takes |
35610 | 131 |
precedence over /usr/bin/perl in the PATH, then the end-user needs |
36204 | 132 |
to take care of installing extra modules, e.g. for HTTP support. |
133 |
Such add-ons are usually included in Apple's /usr/bin/perl by |
|
134 |
default. |
|
35610 | 135 |
|
136 |
* The Java runtime has its own idea about the underlying platform, |
|
48833 | 137 |
which affects Java native libraries in particular. In |
49144 | 138 |
Isabelle/Scala the function isabelle.Platform.jvm_platform |
139 |
identifies the JVM platform. Since a particular Java version is |
|
140 |
always bundled with Isabelle, the resulting settings also provide |
|
141 |
some clues about its platform, without running it. |
|
55438 | 142 |
|
143 |
* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are |
|
64339 | 144 |
notoriously non-portable an should be avoided. |