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.