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 hardly any 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 structures File and Path, or functions
13 like Isabelle_System.bash. The settings environment also provides
14 some means for portability, e.g. jvm_path to keep the impression that
15 Java on Windows/Cygwin adheres to Isabelle/POSIX standards (inside the
16 JVM itself there are many Windows-specific things, though).
18 When producing add-on tools, it is important to stay within this clean
19 room of Isabelle, and refrain from overly ambitious system hacking.
20 The existing Isabelle scripts follow a certain style that might look
21 odd at first sight, but it reflects long years of experience in
22 getting system plumbing right (which is quite hard).
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-darwin Mac OS Leopard (macbroy30)
35 Mac OS Snow Leopard (macbroy2)
36 Mac OS Lion (macbroy6)
37 x86-cygwin Cygwin 1.7 (vmbroy9)
39 x86_64-linux Ubuntu 10.04 LTS
40 x86_64-darwin Mac OS Leopard (macbroy30)
41 Mac OS Snow Leopard (macbroy2)
42 Mac OS Lion (macbroy6)
44 All of the above platforms are 100% supported by Isabelle -- end-users
45 should not have to care about the differences (at least in theory).
46 There are also some additional platforms where Poly/ML also happens to
47 work, but they are *not* covered by the official Isabelle
55 There are increasing problems to make contributing components of
56 Isabelle work on such fringe platforms. Note that x86-bsd is silently
57 treated like x86-linux -- this works if certain Linux compatibility
58 packages are installed on BSD.
61 32 bit vs. 64 bit platforms
62 ---------------------------
64 Most users already have 64 bit hardware, and many of them are running
65 a 64 bit operating system. Native 64 bit support for ML and Scala/JVM
66 is increasingly important for big Isabelle applications, but 32 bit is
67 often the default to get started. Add-on executables need to work
68 seamlessly without manual user configuration, either as native 64 bit
69 executables or in 32 bit mode on a 64 bit platform.
71 The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
72 the platform, even on 64 bit hardware. Tools need to indicate 64 bit
73 support explicitly via the (optional) ISABELLE_PLATFORM64 setting, if
74 this is really required. The following bash expression prefers the 64
75 bit platform, if that is available:
77 "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
79 Note that ML and JVM may have a different idea of the platform,
80 depending on the respective binaries that are actually run. The
81 "uname" Unix tool usually only tells about its own executable format,
82 not the underlying platform.
85 Dependable system tools
86 -----------------------
88 The following portable system tools can be taken for granted:
90 * GNU bash as uniform shell on all platforms. The POSIX "standard"
91 shell /bin/sh is *not* appropriate, because there are too many
92 non-standard implementations of it.
94 * Perl as largely portable system programming language. In some
95 situations Python may serve as an alternative, but it usually
96 performs not as well in addressing various delicate details of
97 operating system concepts (processes, signals, sockets etc.).
99 * Scala with Java Runtime 1.6. The Isabelle/Scala layer irons out
100 many oddities and portability issues of the Java platform.
106 * Mac OS: If MacPorts is installed there is some danger that
107 accidental references to its shared libraries are created
108 (e.g. libgmp). Use otool -L to check if compiled binaries also work
111 * Mac OS: If MacPorts is installed and its version of Perl takes
112 precedence over /usr/bin/perl in the PATH, then the end-user needs
113 to take care of installing extra modules, e.g. for HTTP support.
114 Such add-ons are usually included in Apple's /usr/bin/perl by
117 * The Java runtime has its own idea about the underlying platform,
118 e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM
119 could be x86_64-linux. This affects Java native libraries in
120 particular -- which cause extra portability problems and can make
121 the JVM crash anyway.
123 In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
124 platform. Since there can be many different Java installations on
125 the same machine, which can also be run with different options,
126 reliable JVM platform identification works from inside the running