Some notes on platform support of Isabelle.
Sat, 06 Mar 2010 14:28:31 +0100
changeset 35610 a5b7a0903441
parent 35609 0f2c634c8ab7
child 35611 07a8904f8fcd
Some notes on platform support of Isabelle.
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/PLATFORMS	Sat Mar 06 14:28:31 2010 +0100
@@ -0,0 +1,81 @@
+Some notes on platform support of Isabelle
+The general programming model is that of a stylized ML + Scala + POSIX
+environment, with hardly any system specific code in user-space tools
+and packages.
+The basic Isabelle system infrastructure provides some facilities to
+make this work, e.g. see the ML structures File and Path, or functions
+like bash_output.  The settings environment also provides some means
+for portability, e.g. jvm_path to hold up the impression that even
+Java on Windows/Cygwin adheres to Isabelle/POSIX standards.
+When producing add-on tools, it is important to stay within this clean
+room of Isabelle, and refrain from overly ambitious system hacking.
+Supported platforms
+The following hardware and operating system platforms are officially
+supported by the Isabelle distribution (and bundled tools):
+  x86-linux
+  x86-darwin
+  x86-cygwin
+  x86_64-linux
+  x86_64-darwin
+As of Cygwin 1.7 there is only a 32 bit version of that platform.  The
+other 64 bit platforms become more and more important for power users
+and always need to be taken into account when testing tools.
+All of the above platforms are 100% supported -- end-users should not
+have to care about the differences at all.  There are also some
+secondary platforms where Poly/ML also happens to work:
+  ppc-darwin
+  sparc-solaris
+  x86-solaris
+  x86-bsd
+There is no guarantee that Isabelle add-ons work on these fringe
+platforms.  Even Isabelle/Scala already fails on ppc-darwin due to
+lack of JVM 1.6 support on that platform.
+Dependable system tools
+The following portable system tools can be taken for granted:
+  * GNU bash as uniform shell on all platforms.  Note that the POSIX
+    "standard" shell /bin/sh is *not* appropriate, because there are
+    too many different implementations of it.
+  * Perl as largely portable system programming language.  In some
+    situations Python may as an alternative, but it usually performs
+    not as well in addressing various delicate details of basic
+    operating system concepts (processes, signals, sockets etc.).
+  * Scala with Java Runtime 1.6.  The Isabelle/Pure.jar library irons
+    out many oddities and portability problems of the Java platform.
+Known problems
+* Mac OS: If MacPorts is installed and its version of Perl takes
+  precedence over /usr/bin/perl in the PATH, then the end-user needs
+  to take care of installing add-on modules, e.g. HTTP support.  Such
+  add-ons are usually included in Apple's /usr/bin/perl by default.
+* The Java runtime has its own idea about the underlying platform,
+  e.g. on 64 bit machine Isabelle/ML could be x86-linux, but the JVM
+  could be x86_64-linux.  This affects Java native libraries in
+  particular -- which are very hard to support in a platform
+  independent manner, and should be avoided in the first place.