Admin/PLATFORMS
author huffman
Tue, 09 Oct 2012 17:33:46 +0200
changeset 49759 ecf1d5d87e5e
parent 49144 84699f37481d
child 55391 eae296b5ef33
permissions -rw-r--r--
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands; removed '(open)', '(set_name)' and '(open set_name)' options
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
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
     8
environment, with as little system-specific code in user-space tools
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
     9
as possible.
35610
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
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    12
make this work, e.g. see the ML and Scala modules File and Path, or
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    13
functions like Isabelle_System.bash.  The settings environment also
48836
wenzelm
parents: 48833
diff changeset
    14
provides some means for portability, e.g. the bash function "jvmpath"
wenzelm
parents: 48833
diff changeset
    15
to keep the impression that Java on Windows/Cygwin adheres to
wenzelm
parents: 48833
diff changeset
    16
Isabelle/POSIX standards, although inside the JVM itself there are
wenzelm
parents: 48833
diff changeset
    17
many Windows-specific things.
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    18
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    19
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
    20
room of Isabelle, and refrain from overly ambitious system hacking.
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    21
The existing Isabelle scripts follow a peculiar style that reflects
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    22
long years of experience in getting system plumbing right.
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
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    34
  x86_64-linux      Ubuntu 10.04 LTS
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    35
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    36
  x86_64-darwin     Mac OS Snow Leopard (macbroy2)
44977
1b2ce8d0f8e3 more Mac OS reference hardware;
wenzelm
parents: 44876
diff changeset
    37
                    Mac OS Lion (macbroy6)
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    38
                    Mac OS Mountain Lion (macbroy30)
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    39
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    40
  x86-cygwin        Cygwin 1.7 (vmbroy9)
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    41
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    42
All of the above platforms are 100% supported by Isabelle -- end-users
44876
243e2a413787 some updates of PLATFORMS;
wenzelm
parents: 42424
diff changeset
    43
should not have to care about the differences (at least in theory).
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    44
There are also some additional platforms where Poly/ML might also
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    45
happen to work, but they are *not* covered by the official Isabelle
44876
243e2a413787 some updates of PLATFORMS;
wenzelm
parents: 42424
diff changeset
    46
distribution:
35610
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
  ppc-darwin
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    49
  x86-darwin
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    50
  sparc-solaris
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    51
  x86-solaris
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    52
  x86-bsd
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    53
44876
243e2a413787 some updates of PLATFORMS;
wenzelm
parents: 42424
diff changeset
    54
There are increasing problems to make contributing components of
243e2a413787 some updates of PLATFORMS;
wenzelm
parents: 42424
diff changeset
    55
Isabelle work on such fringe platforms.  Note that x86-bsd is silently
243e2a413787 some updates of PLATFORMS;
wenzelm
parents: 42424
diff changeset
    56
treated like x86-linux -- this works if certain Linux compatibility
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    57
packages are installed on BSD.  Old 32 bit Macintosh hardware is no
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    58
longer supported due the its lack of Java 7.
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
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    64
Most users have 64 bit hardware and are running a 64 bit operating
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    65
system by default.  For Linux this often means missing 32 bit shared
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    66
libraries, so native x86_64-linux needs to be used by default, despite
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    67
its doubled space requirements for Poly/ML heaps.  For Mac OS X, the
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    68
x86-darwin personality usually works seamlessly for C/C++ programs,
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    69
but the Java 7 platform is only available for x86_64-darwin.
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    70
49144
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
    71
Add-on executables are expected to work without manual user
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
    72
configuration.  Each component settings script needs to determine the
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
    73
platform details appropriately.
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    74
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    75
The Isabelle settings environment provides the following variables to
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    76
help configuring platform-dependent tools:
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    77
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    78
  ISABELLE_PLATFORM64  (potentially empty)
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    79
  ISABELLE_PLATFORM32
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    80
  ISABELLE_PLATFORM
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    81
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    82
The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    83
the platform, even on 64 bit hardware.  Using regular bash notation,
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    84
tools may express their preference for 64 bit with a fall-back for 32
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    85
bit as follows:
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    86
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    87
  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    88
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    89
Moreover note that ML and JVM usually have a different idea of the
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    90
platform, depending on the respective binaries that are actually run.
49144
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
    91
Poly/ML 5.5.x performs best in 32 bit mode, even for large
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
    92
applications, thanks to its sophisticated heap management.  The JVM
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
    93
usually works better in 64 bit mode, which allows its heap to grow
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
    94
beyond 2 GB.
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    95
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    96
The traditional "uname" Unix tool usually only tells about its own
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    97
executable format, not the underlying platform!
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    98
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
Dependable system tools
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
The following portable system tools can be taken for granted:
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   104
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
   105
* GNU bash as uniform shell on all platforms.  The POSIX "standard"
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
   106
  shell /bin/sh is *not* appropriate, because there are too many
44876
243e2a413787 some updates of PLATFORMS;
wenzelm
parents: 42424
diff changeset
   107
  non-standard implementations of it.
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   108
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
   109
* Perl as largely portable system programming language.  In some
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
   110
  situations Python may serve as an alternative, but it usually
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
   111
  performs not as well in addressing various delicate details of
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
   112
  operating system concepts (processes, signals, sockets etc.).
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   113
49144
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
   114
* Scala with Java 1.7.  Isabelle/Scala irons out many oddities and
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
   115
  portability issues of the Java platform.
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
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   118
Known problems
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   119
--------------
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   120
41668
62ed9f31ea90 more platform hints;
wenzelm
parents: 41458
diff changeset
   121
* Mac OS: If MacPorts is installed there is some danger that
62ed9f31ea90 more platform hints;
wenzelm
parents: 41458
diff changeset
   122
  accidental references to its shared libraries are created
62ed9f31ea90 more platform hints;
wenzelm
parents: 41458
diff changeset
   123
  (e.g. libgmp).  Use otool -L to check if compiled binaries also work
62ed9f31ea90 more platform hints;
wenzelm
parents: 41458
diff changeset
   124
  without MacPorts.
62ed9f31ea90 more platform hints;
wenzelm
parents: 41458
diff changeset
   125
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   126
* Mac OS: If MacPorts is installed and its version of Perl takes
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   127
  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
   128
  to take care of installing extra modules, e.g. for HTTP support.
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
   129
  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
   130
  default.
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   131
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   132
* The Java runtime has its own idea about the underlying platform,
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
   133
  which affects Java native libraries in particular.  In
49144
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
   134
  Isabelle/Scala the function isabelle.Platform.jvm_platform
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
   135
  identifies the JVM platform.  Since a particular Java version is
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
   136
  always bundled with Isabelle, the resulting settings also provide
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
   137
  some clues about its platform, without running it.