Admin/PLATFORMS
author wenzelm
Mon Sep 25 20:43:21 2017 +0200 (23 months ago)
changeset 66691 a8703e8ee1d3
parent 66529 f39e01e9c489
child 66728 ae332cd13955
permissions -rw-r--r--
basic support for x86_64-cygwin;
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@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@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@35610
    20
room of Isabelle, and refrain from overly ambitious system hacking.
wenzelm@64339
    21
The existing Isabelle bash scripts follow a peculiar style that
wenzelm@64339
    22
reflects 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@64339
    30
following base-line versions (which have been selected to be neither
wenzelm@36204
    31
too old nor too new):
wenzelm@35610
    32
wenzelm@63520
    33
  x86-linux         Ubuntu 12.04 LTS
wenzelm@63520
    34
  x86_64-linux      Ubuntu 12.04 LTS
wenzelm@35610
    35
wenzelm@65369
    36
  x86_64-darwin     Mac OS X 10.9 Mavericks (macbroy2 MacPro4,1)
wenzelm@64406
    37
                    Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2)
wenzelm@64402
    38
                    Mac OS X 10.11 El Capitan (?)
wenzelm@65369
    39
                    macOS 10.12 Sierra (macbroy30 MacBookPro6,2)
wenzelm@48833
    40
wenzelm@64339
    41
  x86-windows       Windows 7
wenzelm@64339
    42
  x86_64-windows    Windows 7
wenzelm@66529
    43
  x86-cygwin        Cygwin 2.8 http://isabelle.in.tum.de/cygwin_2017 (x86/release)
wenzelm@66691
    44
  x86_64-cygwin     Cygwin 2.8 http://isabelle.in.tum.de/cygwin_2017 (x86_64/release)
wenzelm@36204
    45
wenzelm@36204
    46
All of the above platforms are 100% supported by Isabelle -- end-users
wenzelm@44876
    47
should not have to care about the differences (at least in theory).
wenzelm@35610
    48
wenzelm@64339
    49
Fringe platforms like BSD or Solaris are not supported.
wenzelm@36204
    50
wenzelm@36204
    51
wenzelm@36204
    52
32 bit vs. 64 bit platforms
wenzelm@36204
    53
---------------------------
wenzelm@36204
    54
wenzelm@48833
    55
Most users have 64 bit hardware and are running a 64 bit operating
wenzelm@55391
    56
system by default.  For Linux this usually means missing 32 bit shared
wenzelm@48833
    57
libraries, so native x86_64-linux needs to be used by default, despite
wenzelm@48833
    58
its doubled space requirements for Poly/ML heaps.  For Mac OS X, the
wenzelm@48833
    59
x86-darwin personality usually works seamlessly for C/C++ programs,
wenzelm@65073
    60
but the Java platform is always for x86_64-darwin.
wenzelm@48833
    61
wenzelm@49144
    62
Add-on executables are expected to work without manual user
wenzelm@49144
    63
configuration.  Each component settings script needs to determine the
wenzelm@49144
    64
platform details appropriately.
wenzelm@48833
    65
wenzelm@65073
    66
wenzelm@48833
    67
The Isabelle settings environment provides the following variables to
wenzelm@48833
    68
help configuring platform-dependent tools:
wenzelm@48833
    69
wenzelm@48833
    70
  ISABELLE_PLATFORM64  (potentially empty)
wenzelm@66691
    71
  ISABELLE_PLATFORM32  (potentially empty)
wenzelm@48833
    72
  ISABELLE_PLATFORM
wenzelm@36204
    73
wenzelm@36204
    74
The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
wenzelm@48833
    75
the platform, even on 64 bit hardware.  Using regular bash notation,
wenzelm@48833
    76
tools may express their preference for 64 bit with a fall-back for 32
wenzelm@48833
    77
bit as follows:
wenzelm@48833
    78
wenzelm@48833
    79
  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
wenzelm@36204
    80
wenzelm@65073
    81
wenzelm@65073
    82
There is a second set of settings for native Windows (instead of the
wenzelm@65073
    83
POSIX emulation of Cygwin used before):
wenzelm@65073
    84
wenzelm@65073
    85
  ISABELLE_WINDOWS_PLATFORM64  (potentially empty)
wenzelm@65073
    86
  ISABELLE_WINDOWS_PLATFORM32
wenzelm@65073
    87
  ISABELLE_WINDOWS_PLATFORM
wenzelm@65073
    88
wenzelm@65073
    89
It can be used like this:
wenzelm@65073
    90
wenzelm@65073
    91
  "${ISABELLE_WINDOWS_PLATFORM:-$ISABELLE_PLATFORM}"
wenzelm@65073
    92
wenzelm@65073
    93
  "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"
wenzelm@65073
    94
wenzelm@65073
    95
wenzelm@48833
    96
Moreover note that ML and JVM usually have a different idea of the
wenzelm@48833
    97
platform, depending on the respective binaries that are actually run.
wenzelm@64339
    98
Poly/ML 5.6.x performs best in 32 bit mode, even for large
wenzelm@49144
    99
applications, thanks to its sophisticated heap management.  The JVM
wenzelm@49144
   100
usually works better in 64 bit mode, which allows its heap to grow
wenzelm@49144
   101
beyond 2 GB.
wenzelm@36204
   102
wenzelm@64339
   103
The traditional "uname" Unix tool only tells about its own executable
wenzelm@64339
   104
format, not the underlying platform!
wenzelm@35610
   105
wenzelm@35610
   106
wenzelm@35610
   107
Dependable system tools
wenzelm@35610
   108
-----------------------
wenzelm@35610
   109
wenzelm@35610
   110
The following portable system tools can be taken for granted:
wenzelm@35610
   111
wenzelm@64339
   112
* Scala on top of Java 8.  Isabelle/Scala irons out many oddities and
wenzelm@64339
   113
  portability issues of the Java platform.
wenzelm@64339
   114
wenzelm@36204
   115
* GNU bash as uniform shell on all platforms.  The POSIX "standard"
wenzelm@64339
   116
  shell /bin/sh does *not* work -- there are too many non-standard
wenzelm@64339
   117
  implementations of it.
wenzelm@35610
   118
wenzelm@58780
   119
* Perl as largely portable system programming language, with its
wenzelm@58780
   120
  fairly robust support for processes, signals, sockets etc.
wenzelm@35610
   121
wenzelm@35610
   122
wenzelm@35610
   123
Known problems
wenzelm@35610
   124
--------------
wenzelm@35610
   125
wenzelm@55391
   126
* Mac OS X: If MacPorts is installed there is some danger that
wenzelm@41668
   127
  accidental references to its shared libraries are created
wenzelm@41668
   128
  (e.g. libgmp).  Use otool -L to check if compiled binaries also work
wenzelm@41668
   129
  without MacPorts.
wenzelm@41668
   130
wenzelm@55391
   131
* Mac OS X: If MacPorts is installed and its version of Perl takes
wenzelm@35610
   132
  precedence over /usr/bin/perl in the PATH, then the end-user needs
wenzelm@36204
   133
  to take care of installing extra modules, e.g. for HTTP support.
wenzelm@36204
   134
  Such add-ons are usually included in Apple's /usr/bin/perl by
wenzelm@36204
   135
  default.
wenzelm@35610
   136
wenzelm@35610
   137
* The Java runtime has its own idea about the underlying platform,
wenzelm@48833
   138
  which affects Java native libraries in particular.  In
wenzelm@49144
   139
  Isabelle/Scala the function isabelle.Platform.jvm_platform
wenzelm@49144
   140
  identifies the JVM platform.  Since a particular Java version is
wenzelm@49144
   141
  always bundled with Isabelle, the resulting settings also provide
wenzelm@49144
   142
  some clues about its platform, without running it.
wenzelm@55438
   143
wenzelm@55438
   144
* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are
wenzelm@64339
   145
  notoriously non-portable an should be avoided.