6 |
6 |
7 The general programming model is that of a stylized ML + Scala + POSIX |
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 |
8 environment, with as little system-specific code in user-space tools |
9 as possible. |
9 as possible. |
10 |
10 |
11 The basic Isabelle system infrastructure provides some facilities to |
11 The Isabelle system infrastructure provides some facilities to make |
12 make this work, e.g. see the ML and Scala modules File and Path, or |
12 this work, e.g. see the ML and Scala modules File and Path, or |
13 functions like Isabelle_System.bash. The settings environment also |
13 functions like Isabelle_System.bash. The settings environment also |
14 provides some means for portability, e.g. the bash function |
14 provides some means for portability, e.g. the bash function |
15 "platform_path" to keep the impression that Windows/Cygwin adheres to |
15 "platform_path" to keep the impression that Windows/Cygwin adheres to |
16 Isabelle/POSIX standards, although Poly/ML and the JVM are native on |
16 Isabelle/POSIX standards, although Poly/ML and the JVM are native on |
17 Windows. |
17 Windows. |
18 |
18 |
19 When producing add-on tools, it is important to stay within this clean |
19 When producing add-on tools, it is important to stay within this clean |
20 room of Isabelle, and refrain from low-level access to the operating |
20 room of Isabelle, and refrain from non-portable access to operating |
21 system. The Isabelle environment uses peculiar scripts for GNU bash and |
21 system functions. The Isabelle environment uses peculiar scripts for |
22 perl to get the plumbing right. This style should be imitated as far as |
22 GNU bash and perl to get the plumbing right. This style should be |
23 possible. |
23 imitated as far as possible. |
24 |
24 |
25 |
25 |
26 Supported platforms |
26 Supported platforms |
27 ------------------- |
27 ------------------- |
28 |
28 |
47 |
47 |
48 |
48 |
49 64 bit vs. 32 bit platform personality |
49 64 bit vs. 32 bit platform personality |
50 -------------------------------------- |
50 -------------------------------------- |
51 |
51 |
52 Isabelle requires 64 bit hardware running a 64 bit operating. Windows |
52 Isabelle requires 64 bit hardware running a 64 bit operating |
53 and Mac OS X allow x86 executables as well, but for Linux this requires |
53 system. Windows and Mac OS X allow x86 executables as well, but for |
54 separate installation of 32 bit shared libraries. The POSIX emulation on |
54 Linux this requires separate installation of 32 bit shared |
55 Windows via Cygwin64 is exclusively for x86_64. |
55 libraries. The POSIX emulation on Windows via Cygwin64 is exclusively |
|
56 for x86_64. |
56 |
57 |
57 ML works both for x86_64 and x86, and the latter is preferred for space |
58 ML works both for x86_64 and x86, and the latter is preferred for space |
58 and performance reasons. Java is always for x86_64 on all platforms. |
59 and performance reasons. Java is always for x86_64 on all platforms. |
59 |
60 |
60 Add-on executables are expected to work without manual user |
61 Add-on executables are expected to work without manual user |