# HG changeset patch # User wenzelm # Date 1267882111 -3600 # Node ID a5b7a09034411aa768bb11d015d8312cf565ad24 # Parent 0f2c634c8ab7395c1854810282a6116ecca660f0 Some notes on platform support of Isabelle. diff -r 0f2c634c8ab7 -r a5b7a0903441 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.