wenzelm@36204: Some notes on multi-platform support of Isabelle wenzelm@36204: ================================================ wenzelm@35610: wenzelm@35610: Preamble wenzelm@35610: -------- wenzelm@35610: wenzelm@35610: The general programming model is that of a stylized ML + Scala + POSIX wenzelm@35610: environment, with hardly any system specific code in user-space tools wenzelm@35610: and packages. wenzelm@35610: wenzelm@35610: The basic Isabelle system infrastructure provides some facilities to wenzelm@35610: make this work, e.g. see the ML structures File and Path, or functions wenzelm@35610: like bash_output. The settings environment also provides some means wenzelm@36204: for portability, e.g. jvm_path to hold up the impression that Java on wenzelm@36204: Windows/Cygwin adheres to Isabelle/POSIX standards. wenzelm@35610: wenzelm@35610: When producing add-on tools, it is important to stay within this clean wenzelm@35610: room of Isabelle, and refrain from overly ambitious system hacking. wenzelm@36204: The existing Isabelle scripts follow a certain style that might look wenzelm@36204: odd at first sight, but reflects long years of experience in getting wenzelm@36204: system plumbing right (which is quite hard). wenzelm@35610: wenzelm@35610: wenzelm@35610: Supported platforms wenzelm@35610: ------------------- wenzelm@35610: wenzelm@35610: The following hardware and operating system platforms are officially wenzelm@36204: supported by the Isabelle distribution (and bundled tools), with the wenzelm@36204: following reference versions (which have been selected to be neither wenzelm@36204: too old nor too new): wenzelm@35610: wenzelm@36204: x86-linux Ubuntu 8.04 LTS Server wenzelm@36204: x86-darwin Mac OS Leopard wenzelm@36204: x86-cygwin Cygwin 1.7 wenzelm@35610: wenzelm@36204: x86_64-linux Ubuntu 8.04 LTS Server (64) wenzelm@36204: x86_64-darwin Mac OS Leopard wenzelm@36204: wenzelm@36204: All of the above platforms are 100% supported by Isabelle -- end-users wenzelm@36204: should not have to care about the differences at all. There are also wenzelm@36204: some secondary platforms where Poly/ML also happens to work: wenzelm@35610: wenzelm@35610: ppc-darwin wenzelm@35610: sparc-solaris wenzelm@35610: x86-solaris wenzelm@35610: x86-bsd wenzelm@35610: wenzelm@35610: There is no guarantee that Isabelle add-ons work on these fringe wenzelm@35610: platforms. Even Isabelle/Scala already fails on ppc-darwin due to wenzelm@36204: lack of JVM 1.6 support by Apple. wenzelm@36204: wenzelm@36204: wenzelm@36204: 32 bit vs. 64 bit platforms wenzelm@36204: --------------------------- wenzelm@36204: wenzelm@36204: 64 bit hardware becomes more and more important for power users. wenzelm@36204: Add-on tools need to work seamlessly without manual user wenzelm@36204: configuration, although it is often sufficient to fall back on 32 bit wenzelm@36204: executables. wenzelm@36204: wenzelm@36204: The ISABELLE_PLATFORM setting variable refers to the 32 bit version of wenzelm@36204: the platform, even on 64 bit hardware. Power-tools need to indicate wenzelm@36204: 64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64 wenzelm@36204: setting. The following bash expressions prefers the 64 bit platform, wenzelm@36204: if that is available: wenzelm@36204: wenzelm@36204: "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}" wenzelm@36204: wenzelm@36204: Note that ML and JVM may have a different idea of the platform, wenzelm@36204: depending the the respective binaries that are actually run. wenzelm@35610: wenzelm@35610: wenzelm@35610: Dependable system tools wenzelm@35610: ----------------------- wenzelm@35610: wenzelm@35610: The following portable system tools can be taken for granted: wenzelm@35610: wenzelm@36204: * GNU bash as uniform shell on all platforms. The POSIX "standard" wenzelm@36204: shell /bin/sh is *not* appropriate, because there are too many wenzelm@36204: different implementations of it. wenzelm@35610: wenzelm@36204: * Perl as largely portable system programming language. In some wenzelm@36204: situations Python may serve as an alternative, but it usually wenzelm@36204: performs not as well in addressing various delicate details of wenzelm@36204: operating system concepts (processes, signals, sockets etc.). wenzelm@35610: wenzelm@36204: * Scala with Java Runtime 1.6. The Isabelle/Pure.jar library irons wenzelm@36204: out many oddities and portability problems of the Java platform. wenzelm@35610: wenzelm@35610: wenzelm@35610: Known problems wenzelm@35610: -------------- wenzelm@35610: wenzelm@35610: * Mac OS: If MacPorts is installed and its version of Perl takes wenzelm@35610: precedence over /usr/bin/perl in the PATH, then the end-user needs wenzelm@36204: to take care of installing extra modules, e.g. for HTTP support. wenzelm@36204: Such add-ons are usually included in Apple's /usr/bin/perl by wenzelm@36204: default. wenzelm@35610: wenzelm@35610: * The Java runtime has its own idea about the underlying platform, wenzelm@36204: e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM wenzelm@35610: could be x86_64-linux. This affects Java native libraries in wenzelm@36204: particular -- which cause extra portability problems and can make wenzelm@36204: the JVM crash anyway. wenzelm@36204: wenzelm@36204: In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM wenzelm@36204: platform. Since there can be many different Java installations on wenzelm@36204: the same machine, which can also be run with different options, wenzelm@36204: reliable JVM platform identification works from inside the running wenzelm@36204: JVM only.