Admin/PLATFORMS

eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints;

Some notes on platform support of Isabelle
==========================================

Preamble
--------

The general programming model is that of a stylized ML + Scala + POSIX
environment, with hardly any system specific code in user-space tools
and packages.

The basic Isabelle system infrastructure provides some facilities to
make this work, e.g. see the ML structures File and Path, or functions
like bash_output.  The settings environment also provides some means
for portability, e.g. jvm_path to hold up the impression that even
Java on Windows/Cygwin adheres to Isabelle/POSIX standards.

When producing add-on tools, it is important to stay within this clean
room of Isabelle, and refrain from overly ambitious system hacking.


Supported platforms
-------------------

The following hardware and operating system platforms are officially
supported by the Isabelle distribution (and bundled tools):

  x86-linux
  x86-darwin
  x86-cygwin
  x86_64-linux
  x86_64-darwin

As of Cygwin 1.7 there is only a 32 bit version of that platform.  The
other 64 bit platforms become more and more important for power users
and always need to be taken into account when testing tools.

All of the above platforms are 100% supported -- end-users should not
have to care about the differences at all.  There are also some
secondary platforms where Poly/ML also happens to work:

  ppc-darwin
  sparc-solaris
  x86-solaris
  x86-bsd

There is no guarantee that Isabelle add-ons work on these fringe
platforms.  Even Isabelle/Scala already fails on ppc-darwin due to
lack of JVM 1.6 support on that platform.


Dependable system tools
-----------------------

The following portable system tools can be taken for granted:

  * GNU bash as uniform shell on all platforms.  Note that the POSIX
    "standard" shell /bin/sh is *not* appropriate, because there are
    too many different implementations of it.

  * Perl as largely portable system programming language.  In some
    situations Python may as an alternative, but it usually performs
    not as well in addressing various delicate details of basic
    operating system concepts (processes, signals, sockets etc.).

  * Scala with Java Runtime 1.6.  The Isabelle/Pure.jar library irons
    out many oddities and portability problems of the Java platform.


Known problems
--------------

* Mac OS: 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 add-on modules, e.g. 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,
  e.g. on 64 bit machine Isabelle/ML could be x86-linux, but the JVM
  could be x86_64-linux.  This affects Java native libraries in
  particular -- which are very hard to support in a platform
  independent manner, and should be avoided in the first place.