Admin/PLATFORMS
author wenzelm
Sun Nov 28 17:58:38 2010 +0100 (2010-11-28)
changeset 40789 301e91df039d
parent 36204 16c371c6ff86
child 41458 5eca258324ca
permissions -rw-r--r--
updated reference platforms;
wenzelm@36204
     1
Some notes on multi-platform support of Isabelle
wenzelm@36204
     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@36204
    14
for portability, e.g. jvm_path to hold up the impression that Java on
wenzelm@36204
    15
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@36204
    19
The existing Isabelle scripts follow a certain style that might look
wenzelm@36204
    20
odd at first sight, but reflects long years of experience in getting
wenzelm@36204
    21
system plumbing right (which is quite hard).
wenzelm@35610
    22
wenzelm@35610
    23
wenzelm@35610
    24
Supported platforms
wenzelm@35610
    25
-------------------
wenzelm@35610
    26
wenzelm@35610
    27
The following hardware and operating system platforms are officially
wenzelm@36204
    28
supported by the Isabelle distribution (and bundled tools), with the
wenzelm@36204
    29
following reference versions (which have been selected to be neither
wenzelm@36204
    30
too old nor too new):
wenzelm@35610
    31
wenzelm@40789
    32
  x86-linux         SuSE 11.0 (atbroy51)
wenzelm@40789
    33
  x86-darwin        Mac OS Leopard (macbroy6)
wenzelm@40789
    34
  x86-cygwin        Cygwin 1.7 (atbroy102)
wenzelm@35610
    35
wenzelm@40789
    36
  x86_64-linux      SuSE 11.0 (atbroy100)
wenzelm@40789
    37
  x86_64-darwin     Mac OS Leopard (macbroy6)
wenzelm@36204
    38
wenzelm@36204
    39
All of the above platforms are 100% supported by Isabelle -- end-users
wenzelm@36204
    40
should not have to care about the differences at all.  There are also
wenzelm@36204
    41
some secondary platforms where Poly/ML also happens to work:
wenzelm@35610
    42
wenzelm@35610
    43
  ppc-darwin
wenzelm@35610
    44
  sparc-solaris
wenzelm@35610
    45
  x86-solaris
wenzelm@35610
    46
  x86-bsd
wenzelm@35610
    47
wenzelm@35610
    48
There is no guarantee that Isabelle add-ons work on these fringe
wenzelm@35610
    49
platforms.  Even Isabelle/Scala already fails on ppc-darwin due to
wenzelm@36204
    50
lack of JVM 1.6 support by Apple.
wenzelm@36204
    51
wenzelm@36204
    52
wenzelm@36204
    53
32 bit vs. 64 bit platforms
wenzelm@36204
    54
---------------------------
wenzelm@36204
    55
wenzelm@36204
    56
64 bit hardware becomes more and more important for power users.
wenzelm@36204
    57
Add-on tools need to work seamlessly without manual user
wenzelm@36204
    58
configuration, although it is often sufficient to fall back on 32 bit
wenzelm@36204
    59
executables.
wenzelm@36204
    60
wenzelm@36204
    61
The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
wenzelm@36204
    62
the platform, even on 64 bit hardware.  Power-tools need to indicate
wenzelm@36204
    63
64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
wenzelm@36204
    64
setting.  The following bash expressions prefers the 64 bit platform,
wenzelm@36204
    65
if that is available:
wenzelm@36204
    66
wenzelm@36204
    67
  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
wenzelm@36204
    68
wenzelm@36204
    69
Note that ML and JVM may have a different idea of the platform,
wenzelm@36204
    70
depending the the respective binaries that are actually run.
wenzelm@35610
    71
wenzelm@35610
    72
wenzelm@35610
    73
Dependable system tools
wenzelm@35610
    74
-----------------------
wenzelm@35610
    75
wenzelm@35610
    76
The following portable system tools can be taken for granted:
wenzelm@35610
    77
wenzelm@36204
    78
* GNU bash as uniform shell on all platforms.  The POSIX "standard"
wenzelm@36204
    79
  shell /bin/sh is *not* appropriate, because there are too many
wenzelm@36204
    80
  different implementations of it.
wenzelm@35610
    81
wenzelm@36204
    82
* Perl as largely portable system programming language.  In some
wenzelm@36204
    83
  situations Python may serve as an alternative, but it usually
wenzelm@36204
    84
  performs not as well in addressing various delicate details of
wenzelm@36204
    85
  operating system concepts (processes, signals, sockets etc.).
wenzelm@35610
    86
wenzelm@36204
    87
* Scala with Java Runtime 1.6.  The Isabelle/Pure.jar library irons
wenzelm@36204
    88
  out many oddities and portability problems of the Java platform.
wenzelm@35610
    89
wenzelm@35610
    90
wenzelm@35610
    91
Known problems
wenzelm@35610
    92
--------------
wenzelm@35610
    93
wenzelm@35610
    94
* Mac OS: If MacPorts is installed and its version of Perl takes
wenzelm@35610
    95
  precedence over /usr/bin/perl in the PATH, then the end-user needs
wenzelm@36204
    96
  to take care of installing extra modules, e.g. for HTTP support.
wenzelm@36204
    97
  Such add-ons are usually included in Apple's /usr/bin/perl by
wenzelm@36204
    98
  default.
wenzelm@35610
    99
wenzelm@35610
   100
* The Java runtime has its own idea about the underlying platform,
wenzelm@36204
   101
  e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM
wenzelm@35610
   102
  could be x86_64-linux.  This affects Java native libraries in
wenzelm@36204
   103
  particular -- which cause extra portability problems and can make
wenzelm@36204
   104
  the JVM crash anyway.
wenzelm@36204
   105
wenzelm@36204
   106
  In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
wenzelm@36204
   107
  platform.  Since there can be many different Java installations on
wenzelm@36204
   108
  the same machine, which can also be run with different options,
wenzelm@36204
   109
  reliable JVM platform identification works from inside the running
wenzelm@36204
   110
  JVM only.