Admin/PLATFORMS
changeset 35610 a5b7a0903441
child 36204 16c371c6ff86
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/PLATFORMS	Sat Mar 06 14:28:31 2010 +0100
     1.3 @@ -0,0 +1,81 @@
     1.4 +Some notes on platform support of Isabelle
     1.5 +==========================================
     1.6 +
     1.7 +Preamble
     1.8 +--------
     1.9 +
    1.10 +The general programming model is that of a stylized ML + Scala + POSIX
    1.11 +environment, with hardly any system specific code in user-space tools
    1.12 +and packages.
    1.13 +
    1.14 +The basic Isabelle system infrastructure provides some facilities to
    1.15 +make this work, e.g. see the ML structures File and Path, or functions
    1.16 +like bash_output.  The settings environment also provides some means
    1.17 +for portability, e.g. jvm_path to hold up the impression that even
    1.18 +Java on Windows/Cygwin adheres to Isabelle/POSIX standards.
    1.19 +
    1.20 +When producing add-on tools, it is important to stay within this clean
    1.21 +room of Isabelle, and refrain from overly ambitious system hacking.
    1.22 +
    1.23 +
    1.24 +Supported platforms
    1.25 +-------------------
    1.26 +
    1.27 +The following hardware and operating system platforms are officially
    1.28 +supported by the Isabelle distribution (and bundled tools):
    1.29 +
    1.30 +  x86-linux
    1.31 +  x86-darwin
    1.32 +  x86-cygwin
    1.33 +  x86_64-linux
    1.34 +  x86_64-darwin
    1.35 +
    1.36 +As of Cygwin 1.7 there is only a 32 bit version of that platform.  The
    1.37 +other 64 bit platforms become more and more important for power users
    1.38 +and always need to be taken into account when testing tools.
    1.39 +
    1.40 +All of the above platforms are 100% supported -- end-users should not
    1.41 +have to care about the differences at all.  There are also some
    1.42 +secondary platforms where Poly/ML also happens to work:
    1.43 +
    1.44 +  ppc-darwin
    1.45 +  sparc-solaris
    1.46 +  x86-solaris
    1.47 +  x86-bsd
    1.48 +
    1.49 +There is no guarantee that Isabelle add-ons work on these fringe
    1.50 +platforms.  Even Isabelle/Scala already fails on ppc-darwin due to
    1.51 +lack of JVM 1.6 support on that platform.
    1.52 +
    1.53 +
    1.54 +Dependable system tools
    1.55 +-----------------------
    1.56 +
    1.57 +The following portable system tools can be taken for granted:
    1.58 +
    1.59 +  * GNU bash as uniform shell on all platforms.  Note that the POSIX
    1.60 +    "standard" shell /bin/sh is *not* appropriate, because there are
    1.61 +    too many different implementations of it.
    1.62 +
    1.63 +  * Perl as largely portable system programming language.  In some
    1.64 +    situations Python may as an alternative, but it usually performs
    1.65 +    not as well in addressing various delicate details of basic
    1.66 +    operating system concepts (processes, signals, sockets etc.).
    1.67 +
    1.68 +  * Scala with Java Runtime 1.6.  The Isabelle/Pure.jar library irons
    1.69 +    out many oddities and portability problems of the Java platform.
    1.70 +
    1.71 +
    1.72 +Known problems
    1.73 +--------------
    1.74 +
    1.75 +* Mac OS: If MacPorts is installed and its version of Perl takes
    1.76 +  precedence over /usr/bin/perl in the PATH, then the end-user needs
    1.77 +  to take care of installing add-on modules, e.g. HTTP support.  Such
    1.78 +  add-ons are usually included in Apple's /usr/bin/perl by default.
    1.79 +
    1.80 +* The Java runtime has its own idea about the underlying platform,
    1.81 +  e.g. on 64 bit machine Isabelle/ML could be x86-linux, but the JVM
    1.82 +  could be x86_64-linux.  This affects Java native libraries in
    1.83 +  particular -- which are very hard to support in a platform
    1.84 +  independent manner, and should be avoided in the first place.