Admin/PLATFORMS
author wenzelm
Sun Sep 11 14:42:15 2011 +0200 (2011-09-11)
changeset 44876 243e2a413787
parent 42424 e94350a2ed20
child 44977 1b2ce8d0f8e3
permissions -rw-r--r--
some updates of 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@44876
    13
like Isabelle_System.bash.  The settings environment also provides
wenzelm@44876
    14
some means for portability, e.g. jvm_path to keep the impression that
wenzelm@44876
    15
Java on Windows/Cygwin adheres to Isabelle/POSIX standards (inside the
wenzelm@44876
    16
JVM itself there are many Windows-specific things, though).
wenzelm@35610
    17
wenzelm@35610
    18
When producing add-on tools, it is important to stay within this clean
wenzelm@35610
    19
room of Isabelle, and refrain from overly ambitious system hacking.
wenzelm@36204
    20
The existing Isabelle scripts follow a certain style that might look
wenzelm@44876
    21
odd at first sight, but it reflects long years of experience in
wenzelm@44876
    22
getting system plumbing right (which is quite hard).
wenzelm@35610
    23
wenzelm@35610
    24
wenzelm@35610
    25
Supported platforms
wenzelm@35610
    26
-------------------
wenzelm@35610
    27
wenzelm@35610
    28
The following hardware and operating system platforms are officially
wenzelm@36204
    29
supported by the Isabelle distribution (and bundled tools), with the
wenzelm@36204
    30
following reference versions (which have been selected to be neither
wenzelm@36204
    31
too old nor too new):
wenzelm@35610
    32
wenzelm@44876
    33
  x86-linux         Ubuntu 10.04 LTS
wenzelm@42424
    34
  x86-darwin        Mac OS Leopard (macbroy30)
wenzelm@44876
    35
  x86-cygwin        Cygwin 1.7 (vmbroy9)
wenzelm@35610
    36
wenzelm@44876
    37
  x86_64-linux      Ubuntu 10.04 LTS
wenzelm@42424
    38
  x86_64-darwin     Mac OS Leopard (macbroy30)
wenzelm@36204
    39
wenzelm@36204
    40
All of the above platforms are 100% supported by Isabelle -- end-users
wenzelm@44876
    41
should not have to care about the differences (at least in theory).
wenzelm@44876
    42
There are also some additional platforms where Poly/ML also happens to
wenzelm@44876
    43
work, but they are *not* covered by the official Isabelle
wenzelm@44876
    44
distribution:
wenzelm@35610
    45
wenzelm@35610
    46
  ppc-darwin
wenzelm@35610
    47
  sparc-solaris
wenzelm@35610
    48
  x86-solaris
wenzelm@35610
    49
  x86-bsd
wenzelm@35610
    50
wenzelm@44876
    51
There are increasing problems to make contributing components of
wenzelm@44876
    52
Isabelle work on such fringe platforms.  Note that x86-bsd is silently
wenzelm@44876
    53
treated like x86-linux -- this works if certain Linux compatibility
wenzelm@44876
    54
packages are installed on BSD.
wenzelm@36204
    55
wenzelm@36204
    56
wenzelm@36204
    57
32 bit vs. 64 bit platforms
wenzelm@36204
    58
---------------------------
wenzelm@36204
    59
wenzelm@44876
    60
64 bit hardware becomes more and more important for many users.
wenzelm@36204
    61
Add-on tools need to work seamlessly without manual user
wenzelm@36204
    62
configuration, although it is often sufficient to fall back on 32 bit
wenzelm@36204
    63
executables.
wenzelm@36204
    64
wenzelm@36204
    65
The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
wenzelm@36204
    66
the platform, even on 64 bit hardware.  Power-tools need to indicate
wenzelm@36204
    67
64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
boehmes@41458
    68
setting.  The following bash expression prefers the 64 bit platform,
wenzelm@36204
    69
if that is available:
wenzelm@36204
    70
wenzelm@36204
    71
  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
wenzelm@36204
    72
wenzelm@36204
    73
Note that ML and JVM may have a different idea of the platform,
boehmes@41458
    74
depending on the respective binaries that are actually run.
wenzelm@35610
    75
wenzelm@35610
    76
wenzelm@35610
    77
Dependable system tools
wenzelm@35610
    78
-----------------------
wenzelm@35610
    79
wenzelm@35610
    80
The following portable system tools can be taken for granted:
wenzelm@35610
    81
wenzelm@36204
    82
* GNU bash as uniform shell on all platforms.  The POSIX "standard"
wenzelm@36204
    83
  shell /bin/sh is *not* appropriate, because there are too many
wenzelm@44876
    84
  non-standard implementations of it.
wenzelm@35610
    85
wenzelm@36204
    86
* Perl as largely portable system programming language.  In some
wenzelm@36204
    87
  situations Python may serve as an alternative, but it usually
wenzelm@36204
    88
  performs not as well in addressing various delicate details of
wenzelm@36204
    89
  operating system concepts (processes, signals, sockets etc.).
wenzelm@35610
    90
wenzelm@44876
    91
* Scala with Java Runtime 1.6.  The Isabelle/Scala layer irons out
wenzelm@44876
    92
  many oddities and portability issues of the Java platform.
wenzelm@35610
    93
wenzelm@35610
    94
wenzelm@35610
    95
Known problems
wenzelm@35610
    96
--------------
wenzelm@35610
    97
wenzelm@41668
    98
* Mac OS: If MacPorts is installed there is some danger that
wenzelm@41668
    99
  accidental references to its shared libraries are created
wenzelm@41668
   100
  (e.g. libgmp).  Use otool -L to check if compiled binaries also work
wenzelm@41668
   101
  without MacPorts.
wenzelm@41668
   102
wenzelm@35610
   103
* Mac OS: If MacPorts is installed and its version of Perl takes
wenzelm@35610
   104
  precedence over /usr/bin/perl in the PATH, then the end-user needs
wenzelm@36204
   105
  to take care of installing extra modules, e.g. for HTTP support.
wenzelm@36204
   106
  Such add-ons are usually included in Apple's /usr/bin/perl by
wenzelm@36204
   107
  default.
wenzelm@35610
   108
wenzelm@35610
   109
* The Java runtime has its own idea about the underlying platform,
wenzelm@36204
   110
  e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM
wenzelm@35610
   111
  could be x86_64-linux.  This affects Java native libraries in
wenzelm@36204
   112
  particular -- which cause extra portability problems and can make
wenzelm@36204
   113
  the JVM crash anyway.
wenzelm@36204
   114
wenzelm@36204
   115
  In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
wenzelm@36204
   116
  platform.  Since there can be many different Java installations on
wenzelm@36204
   117
  the same machine, which can also be run with different options,
wenzelm@36204
   118
  reliable JVM platform identification works from inside the running
wenzelm@36204
   119
  JVM only.