# HG changeset patch # User wenzelm # Date 1620398679 -7200 # Node ID dea7f6a2485e7aebb8c606ed6db2cfcea5ea1631 # Parent 0da9e824255fa5d56a9789d453a6e37518a6bdd5 clarified file name; diff -r 0da9e824255f -r dea7f6a2485e Admin/PLATFORMS --- a/Admin/PLATFORMS Fri May 07 13:37:48 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,115 +0,0 @@ -Multi-platform support of Isabelle -================================== - -Preamble --------- - -The general programming model is that of a stylized ML + Scala + POSIX -environment, with a minimum of system-specific code in user-space -tools. - -The Isabelle system infrastructure provides some facilities to make -this work, e.g. see the ML and Scala modules File and Path, or -functions like Isabelle_System.bash. The settings environment also -provides some means for portability, e.g. the bash function -"platform_path" to keep the impression that Windows/Cygwin adheres to -Isabelle/POSIX standards, although Poly/ML and the JVM are native on -Windows. - -When producing add-on tools, it is important to stay within this clean -room of Isabelle, and refrain from non-portable access to operating -system functions. The Isabelle environment uses peculiar scripts for -GNU bash and perl as system glue: this style should be observed as far -as possible. - - -Supported platforms -------------------- - -A broad range of hardware and operating system platforms are supported -by building executables on base-line versions that are neither too old -nor too new. Common OS families work: Linux, Windows, macOS, but -exotic ones are unsupported: BSD, Solaris, NixOS. - -Official (full support): - - x86_64-linux Ubuntu 16.04 LTS - - x86_64-darwin macOS 10.13 High Sierra (lapbroy68 MacBookPro11,2) - macOS 10.14 Mojave (mini2 Macmini8,1) - macOS 10.15 Catalina (laramac01 Macmini8,1) - macOS 11.1 Big Sur (mini1 Macmini8,1) - - x86_64-windows Windows 10 - x86_64-cygwin Cygwin 3.1.x https://isabelle.sketis.net/cygwin_2021 (x86_64/release) - -New (experimental): - - arm64-linux Raspberry Pi OS 64bit beta (Debian 10 / Buster) - - arm64-darwin macOS 11.1 Big Sur - - -64 bit vs. 32 bit platform personality --------------------------------------- - -Isabelle requires 64 bit hardware running a 64 bit operating -system. Only Windows still supports native x86 executables, but the -POSIX emulation on Windows via Cygwin64 works exclusively for x86_64. - -The Isabelle settings environment provides variable -ISABELLE_PLATFORM64 to refer to the standard platform personality. On -Windows this is for Cygwin64, but the following native platform -identifiers are available as well: - - ISABELLE_WINDOWS_PLATFORM64 - ISABELLE_WINDOWS_PLATFORM32 - -These are always empty on Linux and macOS, and non-empty on -Windows. For example, this is how to refer to native Windows and -fall-back on Unix (always 64 bit): - - "${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}" - -And this is for old 32 bit executables on Windows, but still 64 bit on -Unix: - - "${ISABELLE_WINDOWS_PLATFORM32:-$ISABELLE_PLATFORM64}" - - -Dependable system tools ------------------------ - -The following portable system tools can be taken for granted: - -* Scala on top of Java. Isabelle/Scala irons out many oddities and - portability issues of the Java platform. - -* GNU bash as uniform shell on all platforms. The POSIX "standard" - shell /bin/sh does *not* work portably -- there are too many - non-standard implementations of it. On Debian and Ubuntu /bin/sh is - actually /bin/dash and introduces many oddities. - -* Perl as largely portable system programming language, with its - fairly robust support for processes, signals, sockets etc. - - -Known problems --------------- - -* macOS: If MacPorts is installed there is some danger that - accidental references to its shared libraries are created - (e.g. libgmp). Use otool -L to check if compiled binaries also work - without MacPorts. - -* macOS: If MacPorts is installed and its version of Perl takes - precedence over /usr/bin/perl in the PATH, then the end-user needs - to take care of installing extra modules, e.g. for HTTP support. - Such add-ons are usually included in Apple's /usr/bin/perl by - default. - -* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are - notoriously non-portable an should be avoided. - -* The traditional "uname" Unix tool only tells about its own executable - format, not the underlying platform! diff -r 0da9e824255f -r dea7f6a2485e Admin/components/PLATFORMS --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/components/PLATFORMS Fri May 07 16:44:39 2021 +0200 @@ -0,0 +1,115 @@ +Multi-platform support of Isabelle +================================== + +Preamble +-------- + +The general programming model is that of a stylized ML + Scala + POSIX +environment, with a minimum of system-specific code in user-space +tools. + +The Isabelle system infrastructure provides some facilities to make +this work, e.g. see the ML and Scala modules File and Path, or +functions like Isabelle_System.bash. The settings environment also +provides some means for portability, e.g. the bash function +"platform_path" to keep the impression that Windows/Cygwin adheres to +Isabelle/POSIX standards, although Poly/ML and the JVM are native on +Windows. + +When producing add-on tools, it is important to stay within this clean +room of Isabelle, and refrain from non-portable access to operating +system functions. The Isabelle environment uses peculiar scripts for +GNU bash and perl as system glue: this style should be observed as far +as possible. + + +Supported platforms +------------------- + +A broad range of hardware and operating system platforms are supported +by building executables on base-line versions that are neither too old +nor too new. Common OS families work: Linux, Windows, macOS, but +exotic ones are unsupported: BSD, Solaris, NixOS. + +Official (full support): + + x86_64-linux Ubuntu 16.04 LTS + + x86_64-darwin macOS 10.13 High Sierra (lapbroy68 MacBookPro11,2) + macOS 10.14 Mojave (mini2 Macmini8,1) + macOS 10.15 Catalina (laramac01 Macmini8,1) + macOS 11.1 Big Sur (mini1 Macmini8,1) + + x86_64-windows Windows 10 + x86_64-cygwin Cygwin 3.1.x https://isabelle.sketis.net/cygwin_2021 (x86_64/release) + +New (experimental): + + arm64-linux Raspberry Pi OS 64bit beta (Debian 10 / Buster) + + arm64-darwin macOS 11.1 Big Sur + + +64 bit vs. 32 bit platform personality +-------------------------------------- + +Isabelle requires 64 bit hardware running a 64 bit operating +system. Only Windows still supports native x86 executables, but the +POSIX emulation on Windows via Cygwin64 works exclusively for x86_64. + +The Isabelle settings environment provides variable +ISABELLE_PLATFORM64 to refer to the standard platform personality. On +Windows this is for Cygwin64, but the following native platform +identifiers are available as well: + + ISABELLE_WINDOWS_PLATFORM64 + ISABELLE_WINDOWS_PLATFORM32 + +These are always empty on Linux and macOS, and non-empty on +Windows. For example, this is how to refer to native Windows and +fall-back on Unix (always 64 bit): + + "${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}" + +And this is for old 32 bit executables on Windows, but still 64 bit on +Unix: + + "${ISABELLE_WINDOWS_PLATFORM32:-$ISABELLE_PLATFORM64}" + + +Dependable system tools +----------------------- + +The following portable system tools can be taken for granted: + +* Scala on top of Java. Isabelle/Scala irons out many oddities and + portability issues of the Java platform. + +* GNU bash as uniform shell on all platforms. The POSIX "standard" + shell /bin/sh does *not* work portably -- there are too many + non-standard implementations of it. On Debian and Ubuntu /bin/sh is + actually /bin/dash and introduces many oddities. + +* Perl as largely portable system programming language, with its + fairly robust support for processes, signals, sockets etc. + + +Known problems +-------------- + +* macOS: If MacPorts is installed there is some danger that + accidental references to its shared libraries are created + (e.g. libgmp). Use otool -L to check if compiled binaries also work + without MacPorts. + +* macOS: If MacPorts is installed and its version of Perl takes + precedence over /usr/bin/perl in the PATH, then the end-user needs + to take care of installing extra modules, e.g. for HTTP support. + Such add-ons are usually included in Apple's /usr/bin/perl by + default. + +* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are + notoriously non-portable an should be avoided. + +* The traditional "uname" Unix tool only tells about its own executable + format, not the underlying platform!