|
35610
|
1 |
Some notes on 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 hardly any system specific code in user-space tools
|
|
|
9 |
and packages.
|
|
|
10 |
|
|
|
11 |
The basic Isabelle system infrastructure provides some facilities to
|
|
|
12 |
make this work, e.g. see the ML structures File and Path, or functions
|
|
|
13 |
like bash_output. The settings environment also provides some means
|
|
|
14 |
for portability, e.g. jvm_path to hold up the impression that even
|
|
|
15 |
Java on Windows/Cygwin adheres to Isabelle/POSIX standards.
|
|
|
16 |
|
|
|
17 |
When producing add-on tools, it is important to stay within this clean
|
|
|
18 |
room of Isabelle, and refrain from overly ambitious system hacking.
|
|
|
19 |
|
|
|
20 |
|
|
|
21 |
Supported platforms
|
|
|
22 |
-------------------
|
|
|
23 |
|
|
|
24 |
The following hardware and operating system platforms are officially
|
|
|
25 |
supported by the Isabelle distribution (and bundled tools):
|
|
|
26 |
|
|
|
27 |
x86-linux
|
|
|
28 |
x86-darwin
|
|
|
29 |
x86-cygwin
|
|
|
30 |
x86_64-linux
|
|
|
31 |
x86_64-darwin
|
|
|
32 |
|
|
|
33 |
As of Cygwin 1.7 there is only a 32 bit version of that platform. The
|
|
|
34 |
other 64 bit platforms become more and more important for power users
|
|
|
35 |
and always need to be taken into account when testing tools.
|
|
|
36 |
|
|
|
37 |
All of the above platforms are 100% supported -- end-users should not
|
|
|
38 |
have to care about the differences at all. There are also some
|
|
|
39 |
secondary platforms where Poly/ML also happens to work:
|
|
|
40 |
|
|
|
41 |
ppc-darwin
|
|
|
42 |
sparc-solaris
|
|
|
43 |
x86-solaris
|
|
|
44 |
x86-bsd
|
|
|
45 |
|
|
|
46 |
There is no guarantee that Isabelle add-ons work on these fringe
|
|
|
47 |
platforms. Even Isabelle/Scala already fails on ppc-darwin due to
|
|
|
48 |
lack of JVM 1.6 support on that platform.
|
|
|
49 |
|
|
|
50 |
|
|
|
51 |
Dependable system tools
|
|
|
52 |
-----------------------
|
|
|
53 |
|
|
|
54 |
The following portable system tools can be taken for granted:
|
|
|
55 |
|
|
|
56 |
* GNU bash as uniform shell on all platforms. Note that the POSIX
|
|
|
57 |
"standard" shell /bin/sh is *not* appropriate, because there are
|
|
|
58 |
too many different implementations of it.
|
|
|
59 |
|
|
|
60 |
* Perl as largely portable system programming language. In some
|
|
|
61 |
situations Python may as an alternative, but it usually performs
|
|
|
62 |
not as well in addressing various delicate details of basic
|
|
|
63 |
operating system concepts (processes, signals, sockets etc.).
|
|
|
64 |
|
|
|
65 |
* Scala with Java Runtime 1.6. The Isabelle/Pure.jar library irons
|
|
|
66 |
out many oddities and portability problems of the Java platform.
|
|
|
67 |
|
|
|
68 |
|
|
|
69 |
Known problems
|
|
|
70 |
--------------
|
|
|
71 |
|
|
|
72 |
* Mac OS: If MacPorts is installed and its version of Perl takes
|
|
|
73 |
precedence over /usr/bin/perl in the PATH, then the end-user needs
|
|
|
74 |
to take care of installing add-on modules, e.g. HTTP support. Such
|
|
|
75 |
add-ons are usually included in Apple's /usr/bin/perl by default.
|
|
|
76 |
|
|
|
77 |
* The Java runtime has its own idea about the underlying platform,
|
|
|
78 |
e.g. on 64 bit machine Isabelle/ML could be x86-linux, but the JVM
|
|
|
79 |
could be x86_64-linux. This affects Java native libraries in
|
|
|
80 |
particular -- which are very hard to support in a platform
|
|
|
81 |
independent manner, and should be avoided in the first place.
|