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