Admin/PLATFORMS
author wenzelm
Sat Jun 02 22:40:03 2018 +0200 (16 months ago)
changeset 68358 e761afd35baa
parent 68002 13d5b2fc9b02
child 68374 8740e1241555
permissions -rw-r--r--
tuned proofs;
wenzelm@64339
     1
Multi-platform support of Isabelle
wenzelm@64339
     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@68002
     8
environment, with a minimum of system-specific code in user-space
wenzelm@68002
     9
tools.
wenzelm@35610
    10
wenzelm@67235
    11
The Isabelle system infrastructure provides some facilities to make
wenzelm@67235
    12
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@61294
    14
provides some means for portability, e.g. the bash function
wenzelm@61294
    15
"platform_path" to keep the impression that Windows/Cygwin adheres to
wenzelm@64339
    16
Isabelle/POSIX standards, although Poly/ML and the JVM are native on
wenzelm@64339
    17
Windows.
wenzelm@35610
    18
wenzelm@35610
    19
When producing add-on tools, it is important to stay within this clean
wenzelm@67235
    20
room of Isabelle, and refrain from non-portable access to operating
wenzelm@67235
    21
system functions. The Isabelle environment uses peculiar scripts for
wenzelm@68002
    22
GNU bash and perl as system glue: this style should be observed as far
wenzelm@68002
    23
as possible.
wenzelm@35610
    24
wenzelm@35610
    25
wenzelm@35610
    26
Supported platforms
wenzelm@35610
    27
-------------------
wenzelm@35610
    28
wenzelm@35610
    29
The following hardware and operating system platforms are officially
wenzelm@36204
    30
supported by the Isabelle distribution (and bundled tools), with the
wenzelm@64339
    31
following base-line versions (which have been selected to be neither
wenzelm@36204
    32
too old nor too new):
wenzelm@35610
    33
wenzelm@63520
    34
  x86_64-linux      Ubuntu 12.04 LTS
wenzelm@35610
    35
wenzelm@67088
    36
  x86_64-darwin     Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2)
wenzelm@67088
    37
                    Mac OS X 10.11 El Capitan (macbroy2 MacPro4,1)
wenzelm@65369
    38
                    macOS 10.12 Sierra (macbroy30 MacBookPro6,2)
wenzelm@68002
    39
                    macOS 10.13 High Sierra
wenzelm@48833
    40
wenzelm@64339
    41
  x86_64-windows    Windows 7
wenzelm@66691
    42
  x86_64-cygwin     Cygwin 2.8 http://isabelle.in.tum.de/cygwin_2017 (x86_64/release)
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@35610
    46
wenzelm@68002
    47
Exotic platforms like BSD, Solaris, NixOS are not supported.
wenzelm@36204
    48
wenzelm@36204
    49
wenzelm@66911
    50
64 bit vs. 32 bit platform personality
wenzelm@66911
    51
--------------------------------------
wenzelm@36204
    52
wenzelm@67235
    53
Isabelle requires 64 bit hardware running a 64 bit operating
wenzelm@67235
    54
system. Windows and Mac OS X allow x86 executables as well, but for
wenzelm@67235
    55
Linux this requires separate installation of 32 bit shared
wenzelm@68002
    56
libraries. The POSIX emulation on Windows via Cygwin64 works
wenzelm@68002
    57
exclusively for x86_64.
wenzelm@66911
    58
wenzelm@68002
    59
Poly/ML supports both for x86_64 and x86, and the latter is preferred
wenzelm@68002
    60
for space and performance reasons. Java is always the x86_64 version
wenzelm@68002
    61
on all platforms.
wenzelm@48833
    62
wenzelm@49144
    63
Add-on executables are expected to work without manual user
wenzelm@66911
    64
configuration. Each component settings script needs to determine the
wenzelm@49144
    65
platform details appropriately.
wenzelm@48833
    66
wenzelm@65073
    67
wenzelm@68002
    68
The Isabelle settings environment provides the following important
wenzelm@68002
    69
variables to help configuring platform-dependent tools:
wenzelm@48833
    70
wenzelm@48833
    71
  ISABELLE_PLATFORM64  (potentially empty)
wenzelm@66691
    72
  ISABELLE_PLATFORM32  (potentially empty)
wenzelm@36204
    73
wenzelm@68002
    74
Each can be empty, but not both at the same time. Using GNU bash
wenzelm@68002
    75
notation, tools may express their platform preference, e.g. first 64
wenzelm@68002
    76
bit and second 32 bit, or the opposite:
wenzelm@48833
    77
wenzelm@48833
    78
  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
wenzelm@68002
    79
  "${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}"
wenzelm@36204
    80
wenzelm@65073
    81
wenzelm@68002
    82
There is a another set of settings for native Windows (instead of the
wenzelm@65073
    83
POSIX emulation of Cygwin used before):
wenzelm@65073
    84
wenzelm@66732
    85
  ISABELLE_WINDOWS_PLATFORM64
wenzelm@65073
    86
  ISABELLE_WINDOWS_PLATFORM32
wenzelm@65073
    87
wenzelm@68002
    88
These are always empty on Linux and Mac OS X, and non-empty on
wenzelm@68002
    89
Windows. They can be used like this to prefer native Windows and then
wenzelm@68002
    90
Unix (first 64 bit second 32 bit):
wenzelm@65073
    91
wenzelm@65073
    92
  "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"
wenzelm@65073
    93
wenzelm@65073
    94
wenzelm@35610
    95
Dependable system tools
wenzelm@35610
    96
-----------------------
wenzelm@35610
    97
wenzelm@35610
    98
The following portable system tools can be taken for granted:
wenzelm@35610
    99
wenzelm@68002
   100
* Scala on top of Java.  Isabelle/Scala irons out many oddities and
wenzelm@64339
   101
  portability issues of the Java platform.
wenzelm@64339
   102
wenzelm@68002
   103
* GNU bash as uniform shell on all platforms. The POSIX "standard"
wenzelm@68002
   104
  shell /bin/sh does *not* work portably -- there are too many
wenzelm@68002
   105
  non-standard implementations of it. On Debian and Ubuntu /bin/sh is
wenzelm@68002
   106
  actually /bin/dash and introduces many oddities.
wenzelm@35610
   107
wenzelm@58780
   108
* Perl as largely portable system programming language, with its
wenzelm@58780
   109
  fairly robust support for processes, signals, sockets etc.
wenzelm@35610
   110
wenzelm@35610
   111
wenzelm@35610
   112
Known problems
wenzelm@35610
   113
--------------
wenzelm@35610
   114
wenzelm@55391
   115
* Mac OS X: If MacPorts is installed there is some danger that
wenzelm@41668
   116
  accidental references to its shared libraries are created
wenzelm@41668
   117
  (e.g. libgmp).  Use otool -L to check if compiled binaries also work
wenzelm@41668
   118
  without MacPorts.
wenzelm@41668
   119
wenzelm@55391
   120
* Mac OS X: If MacPorts is installed and its version of Perl takes
wenzelm@35610
   121
  precedence over /usr/bin/perl in the PATH, then the end-user needs
wenzelm@36204
   122
  to take care of installing extra modules, e.g. for HTTP support.
wenzelm@36204
   123
  Such add-ons are usually included in Apple's /usr/bin/perl by
wenzelm@36204
   124
  default.
wenzelm@35610
   125
wenzelm@55438
   126
* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are
wenzelm@64339
   127
  notoriously non-portable an should be avoided.
wenzelm@66911
   128
wenzelm@66911
   129
* The traditional "uname" Unix tool only tells about its own executable
wenzelm@66911
   130
  format, not the underlying platform!