Admin/PLATFORMS
author haftmann
Fri, 14 Jun 2019 08:34:27 +0000
changeset 70335 9bd8c16b6627
parent 69725 88b8bc6a6e5f
child 71537 93bdbac68d8d
permissions -rw-r--r--
using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64339
321065f9f55b misc tuning and updates;
wenzelm
parents: 64337
diff changeset
     1
Multi-platform support of Isabelle
321065f9f55b misc tuning and updates;
wenzelm
parents: 64337
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
68002
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
     8
environment, with a minimum of system-specific code in user-space
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
     9
tools.
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    10
67235
wenzelm
parents: 67088
diff changeset
    11
The Isabelle system infrastructure provides some facilities to make
wenzelm
parents: 67088
diff changeset
    12
this work, e.g. see the ML and Scala modules File and Path, or
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    13
functions like Isabelle_System.bash.  The settings environment also
61294
2d3d26e9b191 renamed jvmpath to platform_path;
wenzelm
parents: 59114
diff changeset
    14
provides some means for portability, e.g. the bash function
2d3d26e9b191 renamed jvmpath to platform_path;
wenzelm
parents: 59114
diff changeset
    15
"platform_path" to keep the impression that Windows/Cygwin adheres to
64339
321065f9f55b misc tuning and updates;
wenzelm
parents: 64337
diff changeset
    16
Isabelle/POSIX standards, although Poly/ML and the JVM are native on
321065f9f55b misc tuning and updates;
wenzelm
parents: 64337
diff changeset
    17
Windows.
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
67235
wenzelm
parents: 67088
diff changeset
    20
room of Isabelle, and refrain from non-portable access to operating
wenzelm
parents: 67088
diff changeset
    21
system functions. The Isabelle environment uses peculiar scripts for
68002
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    22
GNU bash and perl as system glue: this style should be observed as far
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    23
as possible.
35610
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
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    26
Supported platforms
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
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    29
The following hardware and operating system platforms are officially
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    30
supported by the Isabelle distribution (and bundled tools), with the
64339
321065f9f55b misc tuning and updates;
wenzelm
parents: 64337
diff changeset
    31
following base-line versions (which have been selected to be neither
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    32
too old nor too new):
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    33
69725
88b8bc6a6e5f updated x86_64-linux base line;
wenzelm
parents: 69309
diff changeset
    34
  x86_64-linux      Ubuntu 14.04 LTS
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    35
67088
89e82aed7813 Mac OS X 10.10 Yosemite is baseline;
wenzelm
parents: 66911
diff changeset
    36
  x86_64-darwin     Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2)
89e82aed7813 Mac OS X 10.10 Yosemite is baseline;
wenzelm
parents: 66911
diff changeset
    37
                    Mac OS X 10.11 El Capitan (macbroy2 MacPro4,1)
65369
27c1b5e952bd macbroy30 is on 10.12 Sierra (already since 04-Mar-2017) -- discontinued support for 10.8 Mountain Lion;
wenzelm
parents: 65073
diff changeset
    38
                    macOS 10.12 Sierra (macbroy30 MacBookPro6,2)
69309
283837b0b8b9 renovated macOS tests;
wenzelm
parents: 69244
diff changeset
    39
                    macOS 10.13 High Sierra (lapbroy68 MacBookPro11,2)
69244
264002272392 renovated macOS tests;
wenzelm
parents: 69165
diff changeset
    40
                    macOS 10.14 Mojave (lapnipkow3 MacBookPro9,2)
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    41
64339
321065f9f55b misc tuning and updates;
wenzelm
parents: 64337
diff changeset
    42
  x86_64-windows    Windows 7
68374
8740e1241555 updated to current Cygwin, after 2.10.0-1 from 02-Feb-2018;
wenzelm
parents: 68002
diff changeset
    43
  x86_64-cygwin     Cygwin 2.10 https://isabelle.sketis.net/cygwin_2018 (x86_64/release)
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    44
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    45
All of the above platforms are 100% supported by Isabelle -- end-users
44876
243e2a413787 some updates of PLATFORMS;
wenzelm
parents: 42424
diff changeset
    46
should not have to care about the differences (at least in theory).
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    47
68002
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    48
Exotic platforms like BSD, Solaris, NixOS are not supported.
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    49
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    50
66911
d122c24a93d6 misc tuning and modernization;
wenzelm
parents: 66908
diff changeset
    51
64 bit vs. 32 bit platform personality
d122c24a93d6 misc tuning and modernization;
wenzelm
parents: 66908
diff changeset
    52
--------------------------------------
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    53
67235
wenzelm
parents: 67088
diff changeset
    54
Isabelle requires 64 bit hardware running a 64 bit operating
wenzelm
parents: 67088
diff changeset
    55
system. Windows and Mac OS X allow x86 executables as well, but for
wenzelm
parents: 67088
diff changeset
    56
Linux this requires separate installation of 32 bit shared
68002
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    57
libraries. The POSIX emulation on Windows via Cygwin64 works
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    58
exclusively for x86_64.
66911
d122c24a93d6 misc tuning and modernization;
wenzelm
parents: 66908
diff changeset
    59
68002
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    60
Poly/ML supports both for x86_64 and x86, and the latter is preferred
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    61
for space and performance reasons. Java is always the x86_64 version
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    62
on all platforms.
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    63
49144
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
    64
Add-on executables are expected to work without manual user
66911
d122c24a93d6 misc tuning and modernization;
wenzelm
parents: 66908
diff changeset
    65
configuration. Each component settings script needs to determine the
49144
84699f37481d misc tuning;
wenzelm
parents: 48836
diff changeset
    66
platform details appropriately.
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    67
65073
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    68
68002
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    69
The Isabelle settings environment provides the following important
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    70
variables to help configuring platform-dependent tools:
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    71
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    72
  ISABELLE_PLATFORM64  (potentially empty)
66691
a8703e8ee1d3 basic support for x86_64-cygwin;
wenzelm
parents: 66529
diff changeset
    73
  ISABELLE_PLATFORM32  (potentially empty)
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    74
68002
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    75
Each can be empty, but not both at the same time. Using GNU bash
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    76
notation, tools may express their platform preference, e.g. first 64
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    77
bit and second 32 bit, or the opposite:
48833
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    78
10584ca5785f updates on 32 bit vs. 64 bit platforms;
wenzelm
parents: 46006
diff changeset
    79
  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
68002
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    80
  "${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}"
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    81
65073
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    82
68002
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    83
There is a another set of settings for native Windows (instead of the
65073
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    84
POSIX emulation of Cygwin used before):
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    85
66732
e566fb4d43d4 more and updated documentation;
wenzelm
parents: 66728
diff changeset
    86
  ISABELLE_WINDOWS_PLATFORM64
65073
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    87
  ISABELLE_WINDOWS_PLATFORM32
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    88
68002
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    89
These are always empty on Linux and Mac OS X, and non-empty on
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    90
Windows. They can be used like this to prefer native Windows and then
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    91
Unix (first 64 bit second 32 bit):
65073
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    92
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    93
  "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    94
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    95
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    96
Dependable system tools
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    97
-----------------------
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
The following portable system tools can be taken for granted:
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   100
68002
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
   101
* Scala on top of Java.  Isabelle/Scala irons out many oddities and
64339
321065f9f55b misc tuning and updates;
wenzelm
parents: 64337
diff changeset
   102
  portability issues of the Java platform.
321065f9f55b misc tuning and updates;
wenzelm
parents: 64337
diff changeset
   103
68002
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
   104
* GNU bash as uniform shell on all platforms. The POSIX "standard"
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
   105
  shell /bin/sh does *not* work portably -- there are too many
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
   106
  non-standard implementations of it. On Debian and Ubuntu /bin/sh is
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
   107
  actually /bin/dash and introduces many oddities.
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   108
58780
1f8c0da85664 discontinued python from standard system environment;
wenzelm
parents: 55438
diff changeset
   109
* Perl as largely portable system programming language, with its
1f8c0da85664 discontinued python from standard system environment;
wenzelm
parents: 55438
diff changeset
   110
  fairly robust support for processes, signals, sockets etc.
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   111
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   112
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   113
Known problems
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   114
--------------
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   115
55391
eae296b5ef33 Mac OS X Lion (macbroy6) is baseline for portable executables;
wenzelm
parents: 49144
diff changeset
   116
* Mac OS X: If MacPorts is installed there is some danger that
41668
62ed9f31ea90 more platform hints;
wenzelm
parents: 41458
diff changeset
   117
  accidental references to its shared libraries are created
62ed9f31ea90 more platform hints;
wenzelm
parents: 41458
diff changeset
   118
  (e.g. libgmp).  Use otool -L to check if compiled binaries also work
62ed9f31ea90 more platform hints;
wenzelm
parents: 41458
diff changeset
   119
  without MacPorts.
62ed9f31ea90 more platform hints;
wenzelm
parents: 41458
diff changeset
   120
55391
eae296b5ef33 Mac OS X Lion (macbroy6) is baseline for portable executables;
wenzelm
parents: 49144
diff changeset
   121
* Mac OS X: If MacPorts is installed and its version of Perl takes
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   122
  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
   123
  to take care of installing extra modules, e.g. for HTTP support.
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
   124
  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
   125
  default.
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
   126
55438
3b95e70c5cb3 more platform notes;
wenzelm
parents: 55391
diff changeset
   127
* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are
64339
321065f9f55b misc tuning and updates;
wenzelm
parents: 64337
diff changeset
   128
  notoriously non-portable an should be avoided.
66911
d122c24a93d6 misc tuning and modernization;
wenzelm
parents: 66908
diff changeset
   129
d122c24a93d6 misc tuning and modernization;
wenzelm
parents: 66908
diff changeset
   130
* The traditional "uname" Unix tool only tells about its own executable
d122c24a93d6 misc tuning and modernization;
wenzelm
parents: 66908
diff changeset
   131
  format, not the underlying platform!