Admin/PLATFORMS

--- /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
+==========================================
+
+Preamble
+--------
+
+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.