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