|
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. |