Admin/PLATFORMS
author wenzelm
Wed Dec 28 14:38:14 2011 +0100 (2011-12-28)
changeset 46006 36cd232b18bb
parent 44977 1b2ce8d0f8e3
child 48833 10584ca5785f
permissions -rw-r--r--
updated platform information;
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@44977
    35
                    Mac OS Snow Leopard (macbroy2)
wenzelm@44977
    36
                    Mac OS Lion (macbroy6)
wenzelm@44876
    37
  x86-cygwin        Cygwin 1.7 (vmbroy9)
wenzelm@35610
    38
wenzelm@44876
    39
  x86_64-linux      Ubuntu 10.04 LTS
wenzelm@42424
    40
  x86_64-darwin     Mac OS Leopard (macbroy30)
wenzelm@44977
    41
                    Mac OS Snow Leopard (macbroy2)
wenzelm@44977
    42
                    Mac OS Lion (macbroy6)
wenzelm@36204
    43
wenzelm@36204
    44
All of the above platforms are 100% supported by Isabelle -- end-users
wenzelm@44876
    45
should not have to care about the differences (at least in theory).
wenzelm@44876
    46
There are also some additional platforms where Poly/ML also happens to
wenzelm@44876
    47
work, but they are *not* covered by the official Isabelle
wenzelm@44876
    48
distribution:
wenzelm@35610
    49
wenzelm@35610
    50
  ppc-darwin
wenzelm@35610
    51
  sparc-solaris
wenzelm@35610
    52
  x86-solaris
wenzelm@35610
    53
  x86-bsd
wenzelm@35610
    54
wenzelm@44876
    55
There are increasing problems to make contributing components of
wenzelm@44876
    56
Isabelle work on such fringe platforms.  Note that x86-bsd is silently
wenzelm@44876
    57
treated like x86-linux -- this works if certain Linux compatibility
wenzelm@44876
    58
packages are installed on BSD.
wenzelm@36204
    59
wenzelm@36204
    60
wenzelm@36204
    61
32 bit vs. 64 bit platforms
wenzelm@36204
    62
---------------------------
wenzelm@36204
    63
wenzelm@46006
    64
Most users already have 64 bit hardware, and many of them are running
wenzelm@46006
    65
a 64 bit operating system.  Native 64 bit support for ML and Scala/JVM
wenzelm@46006
    66
is increasingly important for big Isabelle applications, but 32 bit is
wenzelm@46006
    67
often the default to get started.  Add-on executables need to work
wenzelm@46006
    68
seamlessly without manual user configuration, either as native 64 bit
wenzelm@46006
    69
executables or in 32 bit mode on a 64 bit platform.
wenzelm@36204
    70
wenzelm@36204
    71
The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
wenzelm@46006
    72
the platform, even on 64 bit hardware.  Tools need to indicate 64 bit
wenzelm@46006
    73
support explicitly via the (optional) ISABELLE_PLATFORM64 setting, if
wenzelm@46006
    74
this is really required.  The following bash expression prefers the 64
wenzelm@46006
    75
bit platform, if that is available:
wenzelm@36204
    76
wenzelm@36204
    77
  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
wenzelm@36204
    78
wenzelm@36204
    79
Note that ML and JVM may have a different idea of the platform,
wenzelm@46006
    80
depending on the respective binaries that are actually run.  The
wenzelm@46006
    81
"uname" Unix tool usually only tells about its own executable format,
wenzelm@46006
    82
not the underlying platform.
wenzelm@35610
    83
wenzelm@35610
    84
wenzelm@35610
    85
Dependable system tools
wenzelm@35610
    86
-----------------------
wenzelm@35610
    87
wenzelm@35610
    88
The following portable system tools can be taken for granted:
wenzelm@35610
    89
wenzelm@36204
    90
* GNU bash as uniform shell on all platforms.  The POSIX "standard"
wenzelm@36204
    91
  shell /bin/sh is *not* appropriate, because there are too many
wenzelm@44876
    92
  non-standard implementations of it.
wenzelm@35610
    93
wenzelm@36204
    94
* Perl as largely portable system programming language.  In some
wenzelm@36204
    95
  situations Python may serve as an alternative, but it usually
wenzelm@36204
    96
  performs not as well in addressing various delicate details of
wenzelm@36204
    97
  operating system concepts (processes, signals, sockets etc.).
wenzelm@35610
    98
wenzelm@44876
    99
* Scala with Java Runtime 1.6.  The Isabelle/Scala layer irons out
wenzelm@44876
   100
  many oddities and portability issues of the Java platform.
wenzelm@35610
   101
wenzelm@35610
   102
wenzelm@35610
   103
Known problems
wenzelm@35610
   104
--------------
wenzelm@35610
   105
wenzelm@41668
   106
* Mac OS: If MacPorts is installed there is some danger that
wenzelm@41668
   107
  accidental references to its shared libraries are created
wenzelm@41668
   108
  (e.g. libgmp).  Use otool -L to check if compiled binaries also work
wenzelm@41668
   109
  without MacPorts.
wenzelm@41668
   110
wenzelm@35610
   111
* Mac OS: If MacPorts is installed and its version of Perl takes
wenzelm@35610
   112
  precedence over /usr/bin/perl in the PATH, then the end-user needs
wenzelm@36204
   113
  to take care of installing extra modules, e.g. for HTTP support.
wenzelm@36204
   114
  Such add-ons are usually included in Apple's /usr/bin/perl by
wenzelm@36204
   115
  default.
wenzelm@35610
   116
wenzelm@35610
   117
* The Java runtime has its own idea about the underlying platform,
wenzelm@36204
   118
  e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM
wenzelm@35610
   119
  could be x86_64-linux.  This affects Java native libraries in
wenzelm@36204
   120
  particular -- which cause extra portability problems and can make
wenzelm@36204
   121
  the JVM crash anyway.
wenzelm@36204
   122
wenzelm@36204
   123
  In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
wenzelm@36204
   124
  platform.  Since there can be many different Java installations on
wenzelm@36204
   125
  the same machine, which can also be run with different options,
wenzelm@36204
   126
  reliable JVM platform identification works from inside the running
wenzelm@36204
   127
  JVM only.