Some notes on multi-platform support of Isabelle ================================================ Preamble -------- The general programming model is that of a stylized ML + Scala + POSIX environment, with as little system-specific code in user-space tools as possible. The basic Isabelle system infrastructure provides some facilities to make this work, e.g. see the ML and Scala modules File and Path, or functions like Isabelle_System.bash. The settings environment also provides some means for portability, e.g. the bash function "jvmpath" to keep the impression that Java on Windows/Cygwin adheres to Isabelle/POSIX standards, although inside the JVM itself there are many Windows-specific things. When producing add-on tools, it is important to stay within this clean room of Isabelle, and refrain from overly ambitious system hacking. The existing Isabelle scripts follow a peculiar style that reflects long years of experience in getting system plumbing right. Supported platforms ------------------- The following hardware and operating system platforms are officially supported by the Isabelle distribution (and bundled tools), with the following reference versions (which have been selected to be neither too old nor too new): x86-linux Ubuntu 10.04 LTS x86_64-linux Ubuntu 10.04 LTS x86_64-darwin Mac OS X 10.7 Lion (macbroy6) Mac OS X 10.8 Mountain Lion (macbroy30) Mac OS X 10.9 Mavericks (macbroy2) Mac OS X 10.10 Yosemite (macbroy31) x86-cygwin Cygwin 1.7 (vmbroy9) All of the above platforms are 100% supported by Isabelle -- end-users should not have to care about the differences (at least in theory). Fringe platforms like BSD or Solaris are unsupported. 32 bit vs. 64 bit platforms --------------------------- Most users have 64 bit hardware and are running a 64 bit operating system by default. For Linux this usually means missing 32 bit shared libraries, so native x86_64-linux needs to be used by default, despite its doubled space requirements for Poly/ML heaps. For Mac OS X, the x86-darwin personality usually works seamlessly for C/C++ programs, but the Java 7 platform is only available for x86_64-darwin. Add-on executables are expected to work without manual user configuration. Each component settings script needs to determine the platform details appropriately. The Isabelle settings environment provides the following variables to help configuring platform-dependent tools: ISABELLE_PLATFORM64 (potentially empty) ISABELLE_PLATFORM32 ISABELLE_PLATFORM The ISABELLE_PLATFORM setting variable refers to the 32 bit version of the platform, even on 64 bit hardware. Using regular bash notation, tools may express their preference for 64 bit with a fall-back for 32 bit as follows: "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}" Moreover note that ML and JVM usually have a different idea of the platform, depending on the respective binaries that are actually run. Poly/ML 5.5.x performs best in 32 bit mode, even for large applications, thanks to its sophisticated heap management. The JVM usually works better in 64 bit mode, which allows its heap to grow beyond 2 GB. The traditional "uname" Unix tool usually only tells about its own executable format, not the underlying platform! Dependable system tools ----------------------- The following portable system tools can be taken for granted: * GNU bash as uniform shell on all platforms. The POSIX "standard" shell /bin/sh is *not* appropriate, because there are too many non-standard implementations of it. * Perl as largely portable system programming language, with its fairly robust support for processes, signals, sockets etc. * Scala with Java 1.7. Isabelle/Scala irons out many oddities and portability issues of the Java platform. Known problems -------------- * Mac OS X: If MacPorts is installed there is some danger that accidental references to its shared libraries are created (e.g. libgmp). Use otool -L to check if compiled binaries also work without MacPorts. * Mac OS X: 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 extra modules, e.g. for 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, which affects Java native libraries in particular. In Isabelle/Scala the function isabelle.Platform.jvm_platform identifies the JVM platform. Since a particular Java version is always bundled with Isabelle, the resulting settings also provide some clues about its platform, without running it. * Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are notoriously non-portable an should be avoided.