Admin/PLATFORMS
author blanchet
Wed May 21 14:09:42 2014 +0200 (2014-05-21)
changeset 57037 c51132be8e16
parent 55438 3b95e70c5cb3
child 58780 1f8c0da85664
permissions -rw-r--r--
avoid markup-generating @{make_string}
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@48833
     8
environment, with as little system-specific code in user-space tools
wenzelm@48833
     9
as possible.
wenzelm@35610
    10
wenzelm@35610
    11
The basic Isabelle system infrastructure provides some facilities to
wenzelm@48833
    12
make this work, e.g. see the ML and Scala modules File and Path, or
wenzelm@48833
    13
functions like Isabelle_System.bash.  The settings environment also
wenzelm@48836
    14
provides some means for portability, e.g. the bash function "jvmpath"
wenzelm@48836
    15
to keep the impression that Java on Windows/Cygwin adheres to
wenzelm@48836
    16
Isabelle/POSIX standards, although inside the JVM itself there are
wenzelm@48836
    17
many Windows-specific things.
wenzelm@35610
    18
wenzelm@35610
    19
When producing add-on tools, it is important to stay within this clean
wenzelm@35610
    20
room of Isabelle, and refrain from overly ambitious system hacking.
wenzelm@48833
    21
The existing Isabelle scripts follow a peculiar style that reflects
wenzelm@48833
    22
long years of experience in getting system plumbing right.
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@48833
    34
  x86_64-linux      Ubuntu 10.04 LTS
wenzelm@35610
    35
wenzelm@55391
    36
  x86_64-darwin     Mac OS X Lion (macbroy6)
wenzelm@55391
    37
                    Mac OS X Mountain Lion (macbroy30)
wenzelm@55391
    38
                    Mac OS X Mavericks (macbroy2)
wenzelm@48833
    39
wenzelm@48833
    40
  x86-cygwin        Cygwin 1.7 (vmbroy9)
wenzelm@36204
    41
wenzelm@36204
    42
All of the above platforms are 100% supported by Isabelle -- end-users
wenzelm@44876
    43
should not have to care about the differences (at least in theory).
wenzelm@35610
    44
wenzelm@55391
    45
Fringe platforms like BSD or Solaris are unsupported.
wenzelm@36204
    46
wenzelm@36204
    47
wenzelm@36204
    48
32 bit vs. 64 bit platforms
wenzelm@36204
    49
---------------------------
wenzelm@36204
    50
wenzelm@48833
    51
Most users have 64 bit hardware and are running a 64 bit operating
wenzelm@55391
    52
system by default.  For Linux this usually means missing 32 bit shared
wenzelm@48833
    53
libraries, so native x86_64-linux needs to be used by default, despite
wenzelm@48833
    54
its doubled space requirements for Poly/ML heaps.  For Mac OS X, the
wenzelm@48833
    55
x86-darwin personality usually works seamlessly for C/C++ programs,
wenzelm@48833
    56
but the Java 7 platform is only available for x86_64-darwin.
wenzelm@48833
    57
wenzelm@49144
    58
Add-on executables are expected to work without manual user
wenzelm@49144
    59
configuration.  Each component settings script needs to determine the
wenzelm@49144
    60
platform details appropriately.
wenzelm@48833
    61
wenzelm@48833
    62
The Isabelle settings environment provides the following variables to
wenzelm@48833
    63
help configuring platform-dependent tools:
wenzelm@48833
    64
wenzelm@48833
    65
  ISABELLE_PLATFORM64  (potentially empty)
wenzelm@48833
    66
  ISABELLE_PLATFORM32
wenzelm@48833
    67
  ISABELLE_PLATFORM
wenzelm@36204
    68
wenzelm@36204
    69
The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
wenzelm@48833
    70
the platform, even on 64 bit hardware.  Using regular bash notation,
wenzelm@48833
    71
tools may express their preference for 64 bit with a fall-back for 32
wenzelm@48833
    72
bit as follows:
wenzelm@48833
    73
wenzelm@48833
    74
  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
wenzelm@36204
    75
wenzelm@48833
    76
Moreover note that ML and JVM usually have a different idea of the
wenzelm@48833
    77
platform, depending on the respective binaries that are actually run.
wenzelm@49144
    78
Poly/ML 5.5.x performs best in 32 bit mode, even for large
wenzelm@49144
    79
applications, thanks to its sophisticated heap management.  The JVM
wenzelm@49144
    80
usually works better in 64 bit mode, which allows its heap to grow
wenzelm@49144
    81
beyond 2 GB.
wenzelm@36204
    82
wenzelm@48833
    83
The traditional "uname" Unix tool usually only tells about its own
wenzelm@48833
    84
executable format, not the underlying platform!
wenzelm@35610
    85
wenzelm@35610
    86
wenzelm@35610
    87
Dependable system tools
wenzelm@35610
    88
-----------------------
wenzelm@35610
    89
wenzelm@35610
    90
The following portable system tools can be taken for granted:
wenzelm@35610
    91
wenzelm@36204
    92
* GNU bash as uniform shell on all platforms.  The POSIX "standard"
wenzelm@36204
    93
  shell /bin/sh is *not* appropriate, because there are too many
wenzelm@44876
    94
  non-standard implementations of it.
wenzelm@35610
    95
wenzelm@36204
    96
* Perl as largely portable system programming language.  In some
wenzelm@36204
    97
  situations Python may serve as an alternative, but it usually
wenzelm@36204
    98
  performs not as well in addressing various delicate details of
wenzelm@36204
    99
  operating system concepts (processes, signals, sockets etc.).
wenzelm@35610
   100
wenzelm@49144
   101
* Scala with Java 1.7.  Isabelle/Scala irons out many oddities and
wenzelm@49144
   102
  portability issues of the Java platform.
wenzelm@35610
   103
wenzelm@35610
   104
wenzelm@35610
   105
Known problems
wenzelm@35610
   106
--------------
wenzelm@35610
   107
wenzelm@55391
   108
* Mac OS X: If MacPorts is installed there is some danger that
wenzelm@41668
   109
  accidental references to its shared libraries are created
wenzelm@41668
   110
  (e.g. libgmp).  Use otool -L to check if compiled binaries also work
wenzelm@41668
   111
  without MacPorts.
wenzelm@41668
   112
wenzelm@55391
   113
* Mac OS X: If MacPorts is installed and its version of Perl takes
wenzelm@35610
   114
  precedence over /usr/bin/perl in the PATH, then the end-user needs
wenzelm@36204
   115
  to take care of installing extra modules, e.g. for HTTP support.
wenzelm@36204
   116
  Such add-ons are usually included in Apple's /usr/bin/perl by
wenzelm@36204
   117
  default.
wenzelm@35610
   118
wenzelm@35610
   119
* The Java runtime has its own idea about the underlying platform,
wenzelm@48833
   120
  which affects Java native libraries in particular.  In
wenzelm@49144
   121
  Isabelle/Scala the function isabelle.Platform.jvm_platform
wenzelm@49144
   122
  identifies the JVM platform.  Since a particular Java version is
wenzelm@49144
   123
  always bundled with Isabelle, the resulting settings also provide
wenzelm@49144
   124
  some clues about its platform, without running it.
wenzelm@55438
   125
wenzelm@55438
   126
* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are
wenzelm@55438
   127
  notoriously non-portable an should be avoided.