wenzelm@36204
|
1 |
Some notes on multi-platform support of Isabelle
|
wenzelm@36204
|
2 |
================================================
|
wenzelm@35610
|
3 |
|
wenzelm@35610
|
4 |
Preamble
|
wenzelm@35610
|
5 |
--------
|
wenzelm@35610
|
6 |
|
wenzelm@35610
|
7 |
The general programming model is that of a stylized ML + Scala + POSIX
|
wenzelm@35610
|
8 |
environment, with hardly any system specific code in user-space tools
|
wenzelm@35610
|
9 |
and packages.
|
wenzelm@35610
|
10 |
|
wenzelm@35610
|
11 |
The basic Isabelle system infrastructure provides some facilities to
|
wenzelm@35610
|
12 |
make this work, e.g. see the ML structures File and Path, or functions
|
wenzelm@35610
|
13 |
like bash_output. The settings environment also provides some means
|
wenzelm@36204
|
14 |
for portability, e.g. jvm_path to hold up the impression that Java on
|
wenzelm@36204
|
15 |
Windows/Cygwin adheres to Isabelle/POSIX standards.
|
wenzelm@35610
|
16 |
|
wenzelm@35610
|
17 |
When producing add-on tools, it is important to stay within this clean
|
wenzelm@35610
|
18 |
room of Isabelle, and refrain from overly ambitious system hacking.
|
wenzelm@36204
|
19 |
The existing Isabelle scripts follow a certain style that might look
|
wenzelm@36204
|
20 |
odd at first sight, but reflects long years of experience in getting
|
wenzelm@36204
|
21 |
system plumbing right (which is quite hard).
|
wenzelm@35610
|
22 |
|
wenzelm@35610
|
23 |
|
wenzelm@35610
|
24 |
Supported platforms
|
wenzelm@35610
|
25 |
-------------------
|
wenzelm@35610
|
26 |
|
wenzelm@35610
|
27 |
The following hardware and operating system platforms are officially
|
wenzelm@36204
|
28 |
supported by the Isabelle distribution (and bundled tools), with the
|
wenzelm@36204
|
29 |
following reference versions (which have been selected to be neither
|
wenzelm@36204
|
30 |
too old nor too new):
|
wenzelm@35610
|
31 |
|
wenzelm@36204
|
32 |
x86-linux Ubuntu 8.04 LTS Server
|
wenzelm@36204
|
33 |
x86-darwin Mac OS Leopard
|
wenzelm@36204
|
34 |
x86-cygwin Cygwin 1.7
|
wenzelm@35610
|
35 |
|
wenzelm@36204
|
36 |
x86_64-linux Ubuntu 8.04 LTS Server (64)
|
wenzelm@36204
|
37 |
x86_64-darwin Mac OS Leopard
|
wenzelm@35610
|
38 |
|
wenzelm@36204
|
39 |
All of the above platforms are 100% supported by Isabelle -- end-users
|
wenzelm@36204
|
40 |
should not have to care about the differences at all. There are also
|
wenzelm@36204
|
41 |
some secondary platforms where Poly/ML also happens to work:
|
wenzelm@35610
|
42 |
|
wenzelm@35610
|
43 |
ppc-darwin
|
wenzelm@35610
|
44 |
sparc-solaris
|
wenzelm@35610
|
45 |
x86-solaris
|
wenzelm@35610
|
46 |
x86-bsd
|
wenzelm@35610
|
47 |
|
wenzelm@35610
|
48 |
There is no guarantee that Isabelle add-ons work on these fringe
|
wenzelm@35610
|
49 |
platforms. Even Isabelle/Scala already fails on ppc-darwin due to
|
wenzelm@36204
|
50 |
lack of JVM 1.6 support by Apple.
|
wenzelm@36204
|
51 |
|
wenzelm@36204
|
52 |
|
wenzelm@36204
|
53 |
32 bit vs. 64 bit platforms
|
wenzelm@36204
|
54 |
---------------------------
|
wenzelm@36204
|
55 |
|
wenzelm@36204
|
56 |
64 bit hardware becomes more and more important for power users.
|
wenzelm@36204
|
57 |
Add-on tools need to work seamlessly without manual user
|
wenzelm@36204
|
58 |
configuration, although it is often sufficient to fall back on 32 bit
|
wenzelm@36204
|
59 |
executables.
|
wenzelm@36204
|
60 |
|
wenzelm@36204
|
61 |
The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
|
wenzelm@36204
|
62 |
the platform, even on 64 bit hardware. Power-tools need to indicate
|
wenzelm@36204
|
63 |
64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
|
wenzelm@36204
|
64 |
setting. The following bash expressions prefers the 64 bit platform,
|
wenzelm@36204
|
65 |
if that is available:
|
wenzelm@36204
|
66 |
|
wenzelm@36204
|
67 |
"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
|
wenzelm@36204
|
68 |
|
wenzelm@36204
|
69 |
Note that ML and JVM may have a different idea of the platform,
|
wenzelm@36204
|
70 |
depending the the respective binaries that are actually run.
|
wenzelm@35610
|
71 |
|
wenzelm@35610
|
72 |
|
wenzelm@35610
|
73 |
Dependable system tools
|
wenzelm@35610
|
74 |
-----------------------
|
wenzelm@35610
|
75 |
|
wenzelm@35610
|
76 |
The following portable system tools can be taken for granted:
|
wenzelm@35610
|
77 |
|
wenzelm@36204
|
78 |
* GNU bash as uniform shell on all platforms. The POSIX "standard"
|
wenzelm@36204
|
79 |
shell /bin/sh is *not* appropriate, because there are too many
|
wenzelm@36204
|
80 |
different implementations of it.
|
wenzelm@35610
|
81 |
|
wenzelm@36204
|
82 |
* Perl as largely portable system programming language. In some
|
wenzelm@36204
|
83 |
situations Python may serve as an alternative, but it usually
|
wenzelm@36204
|
84 |
performs not as well in addressing various delicate details of
|
wenzelm@36204
|
85 |
operating system concepts (processes, signals, sockets etc.).
|
wenzelm@35610
|
86 |
|
wenzelm@36204
|
87 |
* Scala with Java Runtime 1.6. The Isabelle/Pure.jar library irons
|
wenzelm@36204
|
88 |
out many oddities and portability problems of the Java platform.
|
wenzelm@35610
|
89 |
|
wenzelm@35610
|
90 |
|
wenzelm@35610
|
91 |
Known problems
|
wenzelm@35610
|
92 |
--------------
|
wenzelm@35610
|
93 |
|
wenzelm@35610
|
94 |
* Mac OS: If MacPorts is installed and its version of Perl takes
|
wenzelm@35610
|
95 |
precedence over /usr/bin/perl in the PATH, then the end-user needs
|
wenzelm@36204
|
96 |
to take care of installing extra modules, e.g. for HTTP support.
|
wenzelm@36204
|
97 |
Such add-ons are usually included in Apple's /usr/bin/perl by
|
wenzelm@36204
|
98 |
default.
|
wenzelm@35610
|
99 |
|
wenzelm@35610
|
100 |
* The Java runtime has its own idea about the underlying platform,
|
wenzelm@36204
|
101 |
e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM
|
wenzelm@35610
|
102 |
could be x86_64-linux. This affects Java native libraries in
|
wenzelm@36204
|
103 |
particular -- which cause extra portability problems and can make
|
wenzelm@36204
|
104 |
the JVM crash anyway.
|
wenzelm@36204
|
105 |
|
wenzelm@36204
|
106 |
In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
|
wenzelm@36204
|
107 |
platform. Since there can be many different Java installations on
|
wenzelm@36204
|
108 |
the same machine, which can also be run with different options,
|
wenzelm@36204
|
109 |
reliable JVM platform identification works from inside the running
|
wenzelm@36204
|
110 |
JVM only.
|