wenzelm@64339: Multi-platform support of Isabelle wenzelm@64339: ================================== wenzelm@35610: wenzelm@35610: Preamble wenzelm@35610: -------- wenzelm@35610: wenzelm@35610: The general programming model is that of a stylized ML + Scala + POSIX wenzelm@68002: environment, with a minimum of system-specific code in user-space wenzelm@68002: tools. wenzelm@35610: wenzelm@67235: The Isabelle system infrastructure provides some facilities to make wenzelm@67235: this work, e.g. see the ML and Scala modules File and Path, or wenzelm@48833: functions like Isabelle_System.bash. The settings environment also wenzelm@61294: provides some means for portability, e.g. the bash function wenzelm@61294: "platform_path" to keep the impression that Windows/Cygwin adheres to wenzelm@64339: Isabelle/POSIX standards, although Poly/ML and the JVM are native on wenzelm@64339: Windows. wenzelm@35610: wenzelm@35610: When producing add-on tools, it is important to stay within this clean wenzelm@67235: room of Isabelle, and refrain from non-portable access to operating wenzelm@67235: system functions. The Isabelle environment uses peculiar scripts for wenzelm@68002: GNU bash and perl as system glue: this style should be observed as far wenzelm@68002: as possible. wenzelm@35610: wenzelm@35610: wenzelm@35610: Supported platforms wenzelm@35610: ------------------- wenzelm@35610: wenzelm@35610: The following hardware and operating system platforms are officially wenzelm@36204: supported by the Isabelle distribution (and bundled tools), with the wenzelm@64339: following base-line versions (which have been selected to be neither wenzelm@36204: too old nor too new): wenzelm@35610: wenzelm@63520: x86_64-linux Ubuntu 12.04 LTS wenzelm@35610: wenzelm@67088: x86_64-darwin Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2) wenzelm@67088: Mac OS X 10.11 El Capitan (macbroy2 MacPro4,1) wenzelm@65369: macOS 10.12 Sierra (macbroy30 MacBookPro6,2) wenzelm@68002: macOS 10.13 High Sierra wenzelm@48833: wenzelm@64339: x86_64-windows Windows 7 wenzelm@68374: x86_64-cygwin Cygwin 2.10 https://isabelle.sketis.net/cygwin_2018 (x86_64/release) wenzelm@36204: wenzelm@36204: All of the above platforms are 100% supported by Isabelle -- end-users wenzelm@44876: should not have to care about the differences (at least in theory). wenzelm@35610: wenzelm@68002: Exotic platforms like BSD, Solaris, NixOS are not supported. wenzelm@36204: wenzelm@36204: wenzelm@66911: 64 bit vs. 32 bit platform personality wenzelm@66911: -------------------------------------- wenzelm@36204: wenzelm@67235: Isabelle requires 64 bit hardware running a 64 bit operating wenzelm@67235: system. Windows and Mac OS X allow x86 executables as well, but for wenzelm@67235: Linux this requires separate installation of 32 bit shared wenzelm@68002: libraries. The POSIX emulation on Windows via Cygwin64 works wenzelm@68002: exclusively for x86_64. wenzelm@66911: wenzelm@68002: Poly/ML supports both for x86_64 and x86, and the latter is preferred wenzelm@68002: for space and performance reasons. Java is always the x86_64 version wenzelm@68002: on all platforms. wenzelm@48833: wenzelm@49144: Add-on executables are expected to work without manual user wenzelm@66911: configuration. Each component settings script needs to determine the wenzelm@49144: platform details appropriately. wenzelm@48833: wenzelm@65073: wenzelm@68002: The Isabelle settings environment provides the following important wenzelm@68002: variables to help configuring platform-dependent tools: wenzelm@48833: wenzelm@48833: ISABELLE_PLATFORM64 (potentially empty) wenzelm@66691: ISABELLE_PLATFORM32 (potentially empty) wenzelm@36204: wenzelm@68002: Each can be empty, but not both at the same time. Using GNU bash wenzelm@68002: notation, tools may express their platform preference, e.g. first 64 wenzelm@68002: bit and second 32 bit, or the opposite: wenzelm@48833: wenzelm@48833: "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}" wenzelm@68002: "${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}" wenzelm@36204: wenzelm@65073: wenzelm@68002: There is a another set of settings for native Windows (instead of the wenzelm@65073: POSIX emulation of Cygwin used before): wenzelm@65073: wenzelm@66732: ISABELLE_WINDOWS_PLATFORM64 wenzelm@65073: ISABELLE_WINDOWS_PLATFORM32 wenzelm@65073: wenzelm@68002: These are always empty on Linux and Mac OS X, and non-empty on wenzelm@68002: Windows. They can be used like this to prefer native Windows and then wenzelm@68002: Unix (first 64 bit second 32 bit): wenzelm@65073: wenzelm@65073: "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}" wenzelm@65073: wenzelm@65073: wenzelm@35610: Dependable system tools wenzelm@35610: ----------------------- wenzelm@35610: wenzelm@35610: The following portable system tools can be taken for granted: wenzelm@35610: wenzelm@68002: * Scala on top of Java. Isabelle/Scala irons out many oddities and wenzelm@64339: portability issues of the Java platform. wenzelm@64339: wenzelm@68002: * GNU bash as uniform shell on all platforms. The POSIX "standard" wenzelm@68002: shell /bin/sh does *not* work portably -- there are too many wenzelm@68002: non-standard implementations of it. On Debian and Ubuntu /bin/sh is wenzelm@68002: actually /bin/dash and introduces many oddities. wenzelm@35610: wenzelm@58780: * Perl as largely portable system programming language, with its wenzelm@58780: fairly robust support for processes, signals, sockets etc. wenzelm@35610: wenzelm@35610: wenzelm@35610: Known problems wenzelm@35610: -------------- wenzelm@35610: wenzelm@55391: * Mac OS X: If MacPorts is installed there is some danger that wenzelm@41668: accidental references to its shared libraries are created wenzelm@41668: (e.g. libgmp). Use otool -L to check if compiled binaries also work wenzelm@41668: without MacPorts. wenzelm@41668: wenzelm@55391: * Mac OS X: If MacPorts is installed and its version of Perl takes wenzelm@35610: precedence over /usr/bin/perl in the PATH, then the end-user needs wenzelm@36204: to take care of installing extra modules, e.g. for HTTP support. wenzelm@36204: Such add-ons are usually included in Apple's /usr/bin/perl by wenzelm@36204: default. wenzelm@35610: wenzelm@55438: * Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are wenzelm@64339: notoriously non-portable an should be avoided. wenzelm@66911: wenzelm@66911: * The traditional "uname" Unix tool only tells about its own executable wenzelm@66911: format, not the underlying platform!