11 The basic Isabelle system infrastructure provides some facilities to |
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 |
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 |
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 |
16 Isabelle/POSIX standards, although Poly/ML and the JVM are native on |
17 Windows-specific things. |
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 overly ambitious system hacking. |
20 room of Isabelle, and refrain from overly ambitious system hacking. |
21 The existing Isabelle scripts follow a peculiar style that reflects |
21 The existing Isabelle bash scripts follow a peculiar style that |
22 long years of experience in getting system plumbing right. |
22 reflects long years of experience in getting system plumbing right. |
23 |
23 |
24 |
24 |
25 Supported platforms |
25 Supported platforms |
26 ------------------- |
26 ------------------- |
27 |
27 |
28 The following hardware and operating system platforms are officially |
28 The following hardware and operating system platforms are officially |
29 supported by the Isabelle distribution (and bundled tools), with the |
29 supported by the Isabelle distribution (and bundled tools), with the |
30 following reference versions (which have been selected to be neither |
30 following base-line versions (which have been selected to be neither |
31 too old nor too new): |
31 too old nor too new): |
32 |
32 |
33 x86-linux Ubuntu 12.04 LTS |
33 x86-linux Ubuntu 12.04 LTS |
34 x86_64-linux Ubuntu 12.04 LTS |
34 x86_64-linux Ubuntu 12.04 LTS |
35 |
35 |
37 Mac OS X 10.9 Mavericks (macbroy2) |
37 Mac OS X 10.9 Mavericks (macbroy2) |
38 Mac OS X 10.10 Yosemite (macbroy31) |
38 Mac OS X 10.10 Yosemite (macbroy31) |
39 Mac OS X 10.11 El Capitan (??) |
39 Mac OS X 10.11 El Capitan (??) |
40 macOS 10.12 Sierra (???) |
40 macOS 10.12 Sierra (???) |
41 |
41 |
42 x86-cygwin http://isabelle.in.tum.de/cygwin_2015 (x86/release) |
42 x86-windows Windows 7 |
|
43 x86_64-windows Windows 7 |
|
44 x86-cygwin http://isabelle.in.tum.de/cygwin_2016 (x86/release) |
43 |
45 |
44 All of the above platforms are 100% supported by Isabelle -- end-users |
46 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). |
47 should not have to care about the differences (at least in theory). |
46 |
48 |
47 Fringe platforms like BSD or Solaris are unsupported. |
49 Fringe platforms like BSD or Solaris are not supported. |
48 |
50 |
49 |
51 |
50 32 bit vs. 64 bit platforms |
52 32 bit vs. 64 bit platforms |
51 --------------------------- |
53 --------------------------- |
52 |
54 |
53 Most users have 64 bit hardware and are running a 64 bit operating |
55 Most users have 64 bit hardware and are running a 64 bit operating |
54 system by default. For Linux this usually means missing 32 bit shared |
56 system by default. For Linux this usually means missing 32 bit shared |
55 libraries, so native x86_64-linux needs to be used by default, despite |
57 libraries, so native x86_64-linux needs to be used by default, despite |
56 its doubled space requirements for Poly/ML heaps. For Mac OS X, the |
58 its doubled space requirements for Poly/ML heaps. For Mac OS X, the |
57 x86-darwin personality usually works seamlessly for C/C++ programs, |
59 x86-darwin personality usually works seamlessly for C/C++ programs, |
58 but the Java 7 platform is only available for x86_64-darwin. |
60 but the Java platform is only available for x86_64-darwin. |
59 |
61 |
60 Add-on executables are expected to work without manual user |
62 Add-on executables are expected to work without manual user |
61 configuration. Each component settings script needs to determine the |
63 configuration. Each component settings script needs to determine the |
62 platform details appropriately. |
64 platform details appropriately. |
63 |
65 |
75 |
77 |
76 "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}" |
78 "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}" |
77 |
79 |
78 Moreover note that ML and JVM usually have a different idea of the |
80 Moreover note that ML and JVM usually have a different idea of the |
79 platform, depending on the respective binaries that are actually run. |
81 platform, depending on the respective binaries that are actually run. |
80 Poly/ML 5.5.x performs best in 32 bit mode, even for large |
82 Poly/ML 5.6.x performs best in 32 bit mode, even for large |
81 applications, thanks to its sophisticated heap management. The JVM |
83 applications, thanks to its sophisticated heap management. The JVM |
82 usually works better in 64 bit mode, which allows its heap to grow |
84 usually works better in 64 bit mode, which allows its heap to grow |
83 beyond 2 GB. |
85 beyond 2 GB. |
84 |
86 |
85 The traditional "uname" Unix tool usually only tells about its own |
87 The traditional "uname" Unix tool only tells about its own executable |
86 executable format, not the underlying platform! |
88 format, not the underlying platform! |
87 |
89 |
88 |
90 |
89 Dependable system tools |
91 Dependable system tools |
90 ----------------------- |
92 ----------------------- |
91 |
93 |
92 The following portable system tools can be taken for granted: |
94 The following portable system tools can be taken for granted: |
93 |
95 |
|
96 * Scala on top of Java 8. Isabelle/Scala irons out many oddities and |
|
97 portability issues of the Java platform. |
|
98 |
94 * GNU bash as uniform shell on all platforms. The POSIX "standard" |
99 * GNU bash as uniform shell on all platforms. The POSIX "standard" |
95 shell /bin/sh is *not* appropriate, because there are too many |
100 shell /bin/sh does *not* work -- there are too many non-standard |
96 non-standard implementations of it. |
101 implementations of it. |
97 |
102 |
98 * Perl as largely portable system programming language, with its |
103 * Perl as largely portable system programming language, with its |
99 fairly robust support for processes, signals, sockets etc. |
104 fairly robust support for processes, signals, sockets etc. |
100 |
|
101 * Scala with Java 1.8. Isabelle/Scala irons out many oddities and |
|
102 portability issues of the Java platform. |
|
103 |
105 |
104 |
106 |
105 Known problems |
107 Known problems |
106 -------------- |
108 -------------- |
107 |
109 |