1 Some notes on multi-platform support of Isabelle
2 ================================================
7 The general programming model is that of a stylized ML + Scala + POSIX
8 environment, with as little system-specific code in user-space tools
11 The basic Isabelle system infrastructure provides some facilities to
12 make this work, e.g. see the ML and Scala modules File and Path, or
13 functions like Isabelle_System.bash. The settings environment also
14 provides some means for portability, e.g. the bash function "jvmpath"
15 to keep the impression that Java on Windows/Cygwin adheres to
16 Isabelle/POSIX standards, although inside the JVM itself there are
17 many Windows-specific things.
19 When producing add-on tools, it is important to stay within this clean
20 room of Isabelle, and refrain from overly ambitious system hacking.
21 The existing Isabelle scripts follow a peculiar style that reflects
22 long years of experience in getting system plumbing right.
28 The following hardware and operating system platforms are officially
29 supported by the Isabelle distribution (and bundled tools), with the
30 following reference versions (which have been selected to be neither
33 x86-linux Ubuntu 10.04 LTS
34 x86_64-linux Ubuntu 10.04 LTS
36 x86_64-darwin Mac OS Snow Leopard (macbroy2)
37 Mac OS Lion (macbroy6)
38 Mac OS Mountain Lion (macbroy30)
40 x86-cygwin Cygwin 1.7 (vmbroy9)
42 All of the above platforms are 100% supported by Isabelle -- end-users
43 should not have to care about the differences (at least in theory).
44 There are also some additional platforms where Poly/ML might also
45 happen to work, but they are *not* covered by the official Isabelle
54 There are increasing problems to make contributing components of
55 Isabelle work on such fringe platforms. Note that x86-bsd is silently
56 treated like x86-linux -- this works if certain Linux compatibility
57 packages are installed on BSD. Old 32 bit Macintosh hardware is no
58 longer supported due the its lack of Java 7.
61 32 bit vs. 64 bit platforms
62 ---------------------------
64 Most users have 64 bit hardware and are running a 64 bit operating
65 system by default. For Linux this often means missing 32 bit shared
66 libraries, so native x86_64-linux needs to be used by default, despite
67 its doubled space requirements for Poly/ML heaps. For Mac OS X, the
68 x86-darwin personality usually works seamlessly for C/C++ programs,
69 but the Java 7 platform is only available for x86_64-darwin.
71 Add-on executables are expected to work without manual user
72 configuration. Each component settings script needs to determine the
73 platform details appropriately.
75 The Isabelle settings environment provides the following variables to
76 help configuring platform-dependent tools:
78 ISABELLE_PLATFORM64 (potentially empty)
82 The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
83 the platform, even on 64 bit hardware. Using regular bash notation,
84 tools may express their preference for 64 bit with a fall-back for 32
87 "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
89 Moreover note that ML and JVM usually have a different idea of the
90 platform, depending on the respective binaries that are actually run.
91 Poly/ML 5.5.x performs best in 32 bit mode, even for large
92 applications, thanks to its sophisticated heap management. The JVM
93 usually works better in 64 bit mode, which allows its heap to grow
96 The traditional "uname" Unix tool usually only tells about its own
97 executable format, not the underlying platform!
100 Dependable system tools
101 -----------------------
103 The following portable system tools can be taken for granted:
105 * GNU bash as uniform shell on all platforms. The POSIX "standard"
106 shell /bin/sh is *not* appropriate, because there are too many
107 non-standard implementations of it.
109 * Perl as largely portable system programming language. In some
110 situations Python may serve as an alternative, but it usually
111 performs not as well in addressing various delicate details of
112 operating system concepts (processes, signals, sockets etc.).
114 * Scala with Java 1.7. Isabelle/Scala irons out many oddities and
115 portability issues of the Java platform.
121 * Mac OS: If MacPorts is installed there is some danger that
122 accidental references to its shared libraries are created
123 (e.g. libgmp). Use otool -L to check if compiled binaries also work
126 * Mac OS: If MacPorts is installed and its version of Perl takes
127 precedence over /usr/bin/perl in the PATH, then the end-user needs
128 to take care of installing extra modules, e.g. for HTTP support.
129 Such add-ons are usually included in Apple's /usr/bin/perl by
132 * The Java runtime has its own idea about the underlying platform,
133 which affects Java native libraries in particular. In
134 Isabelle/Scala the function isabelle.Platform.jvm_platform
135 identifies the JVM platform. Since a particular Java version is
136 always bundled with Isabelle, the resulting settings also provide
137 some clues about its platform, without running it.