Admin/components/PLATFORMS
author wenzelm
Fri, 16 Sep 2022 16:34:45 +0200
changeset 76176 d6bd84eb94a3
parent 76028 105867f98630
child 76375 089e546f671f
permissions -rw-r--r--
update to scala-3.2.0; enforce rebuild of Isabelle/ML + Isabelle/Scala;
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
73646
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    16
Isabelle/POSIX standards, although many executables are native on
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    17
Windows (notably Poly/ML and Java).
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
73646
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    21
system functions. The Isabelle environment uses GNU bash and
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    22
Isabelle/Scala as portable system infrastructure, using somewhat
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    23
peculiar implementation techniques.
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
72366
ed99d0f9b536 clarified;
wenzelm
parents: 72359
diff changeset
    29
A broad range of hardware and operating system platforms are supported
ed99d0f9b536 clarified;
wenzelm
parents: 72359
diff changeset
    30
by building executables on base-line versions that are neither too old
73646
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    31
nor too new. Common OS families should work: Linux, macOS,
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    32
Windows. More exotic platforms are unsupported: NixOS, BSD, Solaris.
72366
ed99d0f9b536 clarified;
wenzelm
parents: 72359
diff changeset
    33
73646
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    34
Official platforms:
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    35
73598
461da479f95c update Linux base-line;
wenzelm
parents: 73183
diff changeset
    36
  x86_64-linux      Ubuntu 16.04 LTS
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    37
72366
ed99d0f9b536 clarified;
wenzelm
parents: 72359
diff changeset
    38
  x86_64-darwin     macOS 10.13 High Sierra (lapbroy68 MacBookPro11,2)
72390
ed95980cf198 updated tests for macOS 10.14 Mojave;
wenzelm
parents: 72371
diff changeset
    39
                    macOS 10.14 Mojave (mini2 Macmini8,1)
76027
00afd2c233c0 test macOS 12 Monterey via laramac01;
wenzelm
parents: 75634
diff changeset
    40
                    macOS 10.15 Catalina (???)
74063
ff466b272267 clarified version: Apple now counts like 11, 12, ...;
wenzelm
parents: 73646
diff changeset
    41
                    macOS 11 Big Sur (mini1 Macmini8,1)
76027
00afd2c233c0 test macOS 12 Monterey via laramac01;
wenzelm
parents: 75634
diff changeset
    42
                    macOS 12 Monterey (laramac01 Macmini8,1)
75634
13a0efd9f2ed more macOS versions;
wenzelm
parents: 74419
diff changeset
    43
                    macOS 13 Ventura (???)
72366
ed99d0f9b536 clarified;
wenzelm
parents: 72359
diff changeset
    44
74063
ff466b272267 clarified version: Apple now counts like 11, 12, ...;
wenzelm
parents: 73646
diff changeset
    45
  arm64-darwin      macOS 11 Big Sur
73646
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    46
72526
a3d096a98b69 clarified Windows base line;
wenzelm
parents: 72483
diff changeset
    47
  x86_64-windows    Windows 10
76028
105867f98630 updated to current Cygwin, near 3.3.5-1;
wenzelm
parents: 76027
diff changeset
    48
  x86_64-cygwin     Cygwin 3.3.x https://isabelle.sketis.net/cygwin_2022 (x86_64/release)
72366
ed99d0f9b536 clarified;
wenzelm
parents: 72359
diff changeset
    49
73646
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    50
Experimental platforms:
72359
9af8124f7f0d clarified platforms;
wenzelm
parents: 71537
diff changeset
    51
72371
3e84f4e9651a clarified arm64-linux base line: prefer Pi OS, which is based on slightly older Debian;
wenzelm
parents: 72366
diff changeset
    52
  arm64-linux       Raspberry Pi OS 64bit beta (Debian 10 / Buster)
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    53
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    54
66911
d122c24a93d6 misc tuning and modernization;
wenzelm
parents: 66908
diff changeset
    55
64 bit vs. 32 bit platform personality
d122c24a93d6 misc tuning and modernization;
wenzelm
parents: 66908
diff changeset
    56
--------------------------------------
36204
16c371c6ff86 some updates on multi-platform support;
wenzelm
parents: 35610
diff changeset
    57
67235
wenzelm
parents: 67088
diff changeset
    58
Isabelle requires 64 bit hardware running a 64 bit operating
72895
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    59
system. Only Windows still supports native x86 executables, but the
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    60
POSIX emulation on Windows via Cygwin64 works exclusively for x86_64.
65073
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    61
72895
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    62
The Isabelle settings environment provides variable
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    63
ISABELLE_PLATFORM64 to refer to the standard platform personality. On
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    64
Windows this is for Cygwin64, but the following native platform
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    65
identifiers are available as well:
65073
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    66
66732
e566fb4d43d4 more and updated documentation;
wenzelm
parents: 66728
diff changeset
    67
  ISABELLE_WINDOWS_PLATFORM64
65073
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    68
  ISABELLE_WINDOWS_PLATFORM32
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    69
72894
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72526
diff changeset
    70
These are always empty on Linux and macOS, and non-empty on
72895
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    71
Windows. For example, this is how to refer to native Windows and
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    72
fall-back on Unix (always 64 bit):
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    73
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    74
  "${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}"
65073
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    75
72895
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    76
And this is for old 32 bit executables on Windows, but still 64 bit on
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    77
Unix:
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    78
dc9f43a9ad23 update on platforms;
wenzelm
parents: 72894
diff changeset
    79
  "${ISABELLE_WINDOWS_PLATFORM32:-$ISABELLE_PLATFORM64}"
65073
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    80
73646
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    81
For Apple Silicon the native platform is "$ISABELLE_APPLE_PLATFORM64"
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    82
(arm64-darwin), but thanks to Rosetta 2 "$ISABELLE_PLATFORM64"
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    83
(x64_64-darwin) works routinely with fairly good performance.
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    84
65073
b5bf76cf2b4e more uniform platform settings;
wenzelm
parents: 64406
diff changeset
    85
35610
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    86
Dependable system tools
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
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    89
The following portable system tools can be taken for granted:
a5b7a0903441 Some notes on platform support of Isabelle.
wenzelm
parents:
diff changeset
    90
73646
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    91
* Scala on top of Java.  Isabelle/Scala irons out many fine points of
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
    92
  the Java platform to make it fully portable as described above.
64339
321065f9f55b misc tuning and updates;
wenzelm
parents: 64337
diff changeset
    93
68002
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    94
* GNU bash as uniform shell on all platforms. The POSIX "standard"
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    95
  shell /bin/sh does *not* work portably -- there are too many
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    96
  non-standard implementations of it. On Debian and Ubuntu /bin/sh is
13d5b2fc9b02 misc tuning and clarification;
wenzelm
parents: 67235
diff changeset
    97
  actually /bin/dash and introduces many oddities.
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
Known problems
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
73646
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
   103
* macOS: If Homebrew or MacPorts is installed, there is some danger
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
   104
  that accidental references to its shared libraries are created
41668
62ed9f31ea90 more platform hints;
wenzelm
parents: 41458
diff changeset
   105
  (e.g. libgmp).  Use otool -L to check if compiled binaries also work
62ed9f31ea90 more platform hints;
wenzelm
parents: 41458
diff changeset
   106
  without MacPorts.
62ed9f31ea90 more platform hints;
wenzelm
parents: 41458
diff changeset
   107
55438
3b95e70c5cb3 more platform notes;
wenzelm
parents: 55391
diff changeset
   108
* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are
64339
321065f9f55b misc tuning and updates;
wenzelm
parents: 64337
diff changeset
   109
  notoriously non-portable an should be avoided.
66911
d122c24a93d6 misc tuning and modernization;
wenzelm
parents: 66908
diff changeset
   110
73646
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
   111
* The traditional "uname" Unix tool only tells about its own
078ad17eb934 misc updates and clarification;
wenzelm
parents: 73645
diff changeset
   112
  executable format, not the underlying platform!