proper term_ord as in HOL/Library/positivstellensatz.ML, e.g. relevant for "0 <= c & 0 <= a ==> a + bb = 1 & c <= 1 ==> bb * c * 4 <= (12::real)";
Multi-platform support of Isabelle
==================================
Preamble
--------
The general programming model is that of a stylized ML + Scala + POSIX
environment, with as little system-specific code in user-space tools
as possible.
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 to get the plumbing right. This style should be
imitated as far as possible.
Supported platforms
-------------------
The following hardware and operating system platforms are officially
supported by the Isabelle distribution (and bundled tools), with the
following base-line versions (which have been selected to be neither
too old nor too new):
x86_64-linux Ubuntu 12.04 LTS
x86_64-darwin Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2)
Mac OS X 10.11 El Capitan (macbroy2 MacPro4,1)
macOS 10.12 Sierra (macbroy30 MacBookPro6,2)
x86_64-windows Windows 7
x86_64-cygwin Cygwin 2.8 http://isabelle.in.tum.de/cygwin_2017 (x86_64/release)
All of the above platforms are 100% supported by Isabelle -- end-users
should not have to care about the differences (at least in theory).
Fringe platforms like BSD or Solaris are not supported.
64 bit vs. 32 bit platform personality
--------------------------------------
Isabelle requires 64 bit hardware running a 64 bit operating
system. Windows and Mac OS X allow x86 executables as well, but for
Linux this requires separate installation of 32 bit shared
libraries. The POSIX emulation on Windows via Cygwin64 is exclusively
for x86_64.
ML works both for x86_64 and x86, and the latter is preferred for space
and performance reasons. Java is always for x86_64 on all platforms.
Add-on executables are expected to work without manual user
configuration. Each component settings script needs to determine the
platform details appropriately.
The Isabelle settings environment provides the following variables to
help configuring platform-dependent tools:
ISABELLE_PLATFORM64 (potentially empty)
ISABELLE_PLATFORM32 (potentially empty)
ISABELLE_PLATFORM
The ISABELLE_PLATFORM setting variable prefers the 32 bit personality of
the platform, if possible. Using regular bash notation, tools may
express their preference for 64 bit with a fall-back for 32 bit as
follows:
"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
There is a second set of settings for native Windows (instead of the
POSIX emulation of Cygwin used before):
ISABELLE_WINDOWS_PLATFORM64
ISABELLE_WINDOWS_PLATFORM32
ISABELLE_WINDOWS_PLATFORM
It can be used like this:
"${ISABELLE_WINDOWS_PLATFORM:-$ISABELLE_PLATFORM}"
"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"
Dependable system tools
-----------------------
The following portable system tools can be taken for granted:
* Scala on top of Java 8. 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 -- there are too many non-standard
implementations of it. On Debian and Ubuntu /bin/sh is actually
/bin/dash and thus introduces many oddities.
* Perl as largely portable system programming language, with its
fairly robust support for processes, signals, sockets etc.
Known problems
--------------
* Mac OS X: 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.
* Mac OS X: 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.
* The Java runtime has its own idea about the underlying platform, which
affects Java native libraries in particular. In Isabelle/Scala the
function isabelle.Platform.jvm_platform identifies the JVM platform.
In the settings environment, ISABELLE_JAVA_PLATFORM provides the same
information without running the JVM.
* 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!