Admin/PLATFORMS

killed dead data

+
−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 Lion (macbroy6)
+
−                    Mac OS X Mountain Lion (macbroy30)
+
−                    Mac OS X Mavericks (macbroy2)
+
−
+
−  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.  In some
+
−  situations Python may serve as an alternative, but it usually
+
−  performs not as well in addressing various delicate details of
+
−  operating system concepts (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.