Admin/PLATFORMS
author wenzelm
Sat Mar 06 14:28:31 2010 +0100 (2010-03-06)
changeset 35610 a5b7a0903441
child 36204 16c371c6ff86
permissions -rw-r--r--
Some notes on platform support of Isabelle.
     1 Some notes on platform support of Isabelle
     2 ==========================================
     3 
     4 Preamble
     5 --------
     6 
     7 The general programming model is that of a stylized ML + Scala + POSIX
     8 environment, with hardly any system specific code in user-space tools
     9 and packages.
    10 
    11 The basic Isabelle system infrastructure provides some facilities to
    12 make this work, e.g. see the ML structures File and Path, or functions
    13 like bash_output.  The settings environment also provides some means
    14 for portability, e.g. jvm_path to hold up the impression that even
    15 Java on Windows/Cygwin adheres to Isabelle/POSIX standards.
    16 
    17 When producing add-on tools, it is important to stay within this clean
    18 room of Isabelle, and refrain from overly ambitious system hacking.
    19 
    20 
    21 Supported platforms
    22 -------------------
    23 
    24 The following hardware and operating system platforms are officially
    25 supported by the Isabelle distribution (and bundled tools):
    26 
    27   x86-linux
    28   x86-darwin
    29   x86-cygwin
    30   x86_64-linux
    31   x86_64-darwin
    32 
    33 As of Cygwin 1.7 there is only a 32 bit version of that platform.  The
    34 other 64 bit platforms become more and more important for power users
    35 and always need to be taken into account when testing tools.
    36 
    37 All of the above platforms are 100% supported -- end-users should not
    38 have to care about the differences at all.  There are also some
    39 secondary platforms where Poly/ML also happens to work:
    40 
    41   ppc-darwin
    42   sparc-solaris
    43   x86-solaris
    44   x86-bsd
    45 
    46 There is no guarantee that Isabelle add-ons work on these fringe
    47 platforms.  Even Isabelle/Scala already fails on ppc-darwin due to
    48 lack of JVM 1.6 support on that platform.
    49 
    50 
    51 Dependable system tools
    52 -----------------------
    53 
    54 The following portable system tools can be taken for granted:
    55 
    56   * GNU bash as uniform shell on all platforms.  Note that the POSIX
    57     "standard" shell /bin/sh is *not* appropriate, because there are
    58     too many different implementations of it.
    59 
    60   * Perl as largely portable system programming language.  In some
    61     situations Python may as an alternative, but it usually performs
    62     not as well in addressing various delicate details of basic
    63     operating system concepts (processes, signals, sockets etc.).
    64 
    65   * Scala with Java Runtime 1.6.  The Isabelle/Pure.jar library irons
    66     out many oddities and portability problems of the Java platform.
    67 
    68 
    69 Known problems
    70 --------------
    71 
    72 * Mac OS: If MacPorts is installed and its version of Perl takes
    73   precedence over /usr/bin/perl in the PATH, then the end-user needs
    74   to take care of installing add-on modules, e.g. HTTP support.  Such
    75   add-ons are usually included in Apple's /usr/bin/perl by default.
    76 
    77 * The Java runtime has its own idea about the underlying platform,
    78   e.g. on 64 bit machine Isabelle/ML could be x86-linux, but the JVM
    79   could be x86_64-linux.  This affects Java native libraries in
    80   particular -- which are very hard to support in a platform
    81   independent manner, and should be avoided in the first place.