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