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