wneuper@59180
|
1 |
Some notes on multi-platform support of Isabelle
|
wneuper@59180
|
2 |
================================================
|
wneuper@59180
|
3 |
|
wneuper@59180
|
4 |
Preamble
|
wneuper@59180
|
5 |
--------
|
wneuper@59180
|
6 |
|
wneuper@59180
|
7 |
The general programming model is that of a stylized ML + Scala + POSIX
|
wneuper@59180
|
8 |
environment, with as little system-specific code in user-space tools
|
wneuper@59180
|
9 |
as possible.
|
wneuper@59180
|
10 |
|
wneuper@59180
|
11 |
The basic Isabelle system infrastructure provides some facilities to
|
wneuper@59180
|
12 |
make this work, e.g. see the ML and Scala modules File and Path, or
|
wneuper@59180
|
13 |
functions like Isabelle_System.bash. The settings environment also
|
wneuper@59180
|
14 |
provides some means for portability, e.g. the bash function "jvmpath"
|
wneuper@59180
|
15 |
to keep the impression that Java on Windows/Cygwin adheres to
|
wneuper@59180
|
16 |
Isabelle/POSIX standards, although inside the JVM itself there are
|
wneuper@59180
|
17 |
many Windows-specific things.
|
wneuper@59180
|
18 |
|
wneuper@59180
|
19 |
When producing add-on tools, it is important to stay within this clean
|
wneuper@59180
|
20 |
room of Isabelle, and refrain from overly ambitious system hacking.
|
wneuper@59180
|
21 |
The existing Isabelle scripts follow a peculiar style that reflects
|
wneuper@59180
|
22 |
long years of experience in getting system plumbing right.
|
wneuper@59180
|
23 |
|
wneuper@59180
|
24 |
|
wneuper@59180
|
25 |
Supported platforms
|
wneuper@59180
|
26 |
-------------------
|
wneuper@59180
|
27 |
|
wneuper@59180
|
28 |
The following hardware and operating system platforms are officially
|
wneuper@59180
|
29 |
supported by the Isabelle distribution (and bundled tools), with the
|
wneuper@59180
|
30 |
following reference versions (which have been selected to be neither
|
wneuper@59180
|
31 |
too old nor too new):
|
wneuper@59180
|
32 |
|
wneuper@59180
|
33 |
x86-linux Ubuntu 10.04 LTS
|
wneuper@59180
|
34 |
x86_64-linux Ubuntu 10.04 LTS
|
wneuper@59180
|
35 |
|
wneuper@59180
|
36 |
x86_64-darwin Mac OS X 10.7 Lion (macbroy6)
|
wneuper@59180
|
37 |
Mac OS X 10.8 Mountain Lion (macbroy30)
|
wneuper@59180
|
38 |
Mac OS X 10.9 Mavericks (macbroy2)
|
wneuper@59180
|
39 |
Mac OS X 10.10 Yosemite (macbroy31)
|
wneuper@59180
|
40 |
|
wneuper@59180
|
41 |
x86-cygwin Cygwin 1.7 (vmbroy9)
|
wneuper@59180
|
42 |
|
wneuper@59180
|
43 |
All of the above platforms are 100% supported by Isabelle -- end-users
|
wneuper@59180
|
44 |
should not have to care about the differences (at least in theory).
|
wneuper@59180
|
45 |
|
wneuper@59180
|
46 |
Fringe platforms like BSD or Solaris are unsupported.
|
wneuper@59180
|
47 |
|
wneuper@59180
|
48 |
|
wneuper@59180
|
49 |
32 bit vs. 64 bit platforms
|
wneuper@59180
|
50 |
---------------------------
|
wneuper@59180
|
51 |
|
wneuper@59180
|
52 |
Most users have 64 bit hardware and are running a 64 bit operating
|
wneuper@59180
|
53 |
system by default. For Linux this usually means missing 32 bit shared
|
wneuper@59180
|
54 |
libraries, so native x86_64-linux needs to be used by default, despite
|
wneuper@59180
|
55 |
its doubled space requirements for Poly/ML heaps. For Mac OS X, the
|
wneuper@59180
|
56 |
x86-darwin personality usually works seamlessly for C/C++ programs,
|
wneuper@59180
|
57 |
but the Java 7 platform is only available for x86_64-darwin.
|
wneuper@59180
|
58 |
|
wneuper@59180
|
59 |
Add-on executables are expected to work without manual user
|
wneuper@59180
|
60 |
configuration. Each component settings script needs to determine the
|
wneuper@59180
|
61 |
platform details appropriately.
|
wneuper@59180
|
62 |
|
wneuper@59180
|
63 |
The Isabelle settings environment provides the following variables to
|
wneuper@59180
|
64 |
help configuring platform-dependent tools:
|
wneuper@59180
|
65 |
|
wneuper@59180
|
66 |
ISABELLE_PLATFORM64 (potentially empty)
|
wneuper@59180
|
67 |
ISABELLE_PLATFORM32
|
wneuper@59180
|
68 |
ISABELLE_PLATFORM
|
wneuper@59180
|
69 |
|
wneuper@59180
|
70 |
The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
|
wneuper@59180
|
71 |
the platform, even on 64 bit hardware. Using regular bash notation,
|
wneuper@59180
|
72 |
tools may express their preference for 64 bit with a fall-back for 32
|
wneuper@59180
|
73 |
bit as follows:
|
wneuper@59180
|
74 |
|
wneuper@59180
|
75 |
"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
|
wneuper@59180
|
76 |
|
wneuper@59180
|
77 |
Moreover note that ML and JVM usually have a different idea of the
|
wneuper@59180
|
78 |
platform, depending on the respective binaries that are actually run.
|
wneuper@59180
|
79 |
Poly/ML 5.5.x performs best in 32 bit mode, even for large
|
wneuper@59180
|
80 |
applications, thanks to its sophisticated heap management. The JVM
|
wneuper@59180
|
81 |
usually works better in 64 bit mode, which allows its heap to grow
|
wneuper@59180
|
82 |
beyond 2 GB.
|
wneuper@59180
|
83 |
|
wneuper@59180
|
84 |
The traditional "uname" Unix tool usually only tells about its own
|
wneuper@59180
|
85 |
executable format, not the underlying platform!
|
wneuper@59180
|
86 |
|
wneuper@59180
|
87 |
|
wneuper@59180
|
88 |
Dependable system tools
|
wneuper@59180
|
89 |
-----------------------
|
wneuper@59180
|
90 |
|
wneuper@59180
|
91 |
The following portable system tools can be taken for granted:
|
wneuper@59180
|
92 |
|
wneuper@59180
|
93 |
* GNU bash as uniform shell on all platforms. The POSIX "standard"
|
wneuper@59180
|
94 |
shell /bin/sh is *not* appropriate, because there are too many
|
wneuper@59180
|
95 |
non-standard implementations of it.
|
wneuper@59180
|
96 |
|
wneuper@59180
|
97 |
* Perl as largely portable system programming language, with its
|
wneuper@59180
|
98 |
fairly robust support for processes, signals, sockets etc.
|
wneuper@59180
|
99 |
|
wneuper@59180
|
100 |
* Scala with Java 1.7. Isabelle/Scala irons out many oddities and
|
wneuper@59180
|
101 |
portability issues of the Java platform.
|
wneuper@59180
|
102 |
|
wneuper@59180
|
103 |
|
wneuper@59180
|
104 |
Known problems
|
wneuper@59180
|
105 |
--------------
|
wneuper@59180
|
106 |
|
wneuper@59180
|
107 |
* Mac OS X: If MacPorts is installed there is some danger that
|
wneuper@59180
|
108 |
accidental references to its shared libraries are created
|
wneuper@59180
|
109 |
(e.g. libgmp). Use otool -L to check if compiled binaries also work
|
wneuper@59180
|
110 |
without MacPorts.
|
wneuper@59180
|
111 |
|
wneuper@59180
|
112 |
* Mac OS X: If MacPorts is installed and its version of Perl takes
|
wneuper@59180
|
113 |
precedence over /usr/bin/perl in the PATH, then the end-user needs
|
wneuper@59180
|
114 |
to take care of installing extra modules, e.g. for HTTP support.
|
wneuper@59180
|
115 |
Such add-ons are usually included in Apple's /usr/bin/perl by
|
wneuper@59180
|
116 |
default.
|
wneuper@59180
|
117 |
|
wneuper@59180
|
118 |
* The Java runtime has its own idea about the underlying platform,
|
wneuper@59180
|
119 |
which affects Java native libraries in particular. In
|
wneuper@59180
|
120 |
Isabelle/Scala the function isabelle.Platform.jvm_platform
|
wneuper@59180
|
121 |
identifies the JVM platform. Since a particular Java version is
|
wneuper@59180
|
122 |
always bundled with Isabelle, the resulting settings also provide
|
wneuper@59180
|
123 |
some clues about its platform, without running it.
|
wneuper@59180
|
124 |
|
wneuper@59180
|
125 |
* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are
|
wneuper@59180
|
126 |
notoriously non-portable an should be avoided. |