Isabelle installation notes===========================1) System installation----------------------The Isabelle distribution includes both complete sources andprecompiled binary packages for common Unix platforms.Quick installation------------------Ready-to-go packages are provided for the ML compiler and runtimesystem, the Isabelle sources, and some major object-logics. A minimalsite installation of Isabelle on Linux/x86 works like this: tar -C /usr/local -xzf Isabelle.tar.gz tar -C /usr/local -xzf polyml_base.tar.gz tar -C /usr/local -xzf polyml_x86-linux.tar.gz tar -C /usr/local -xzf HOL_x86-linux.tar.gzThe install prefix given above may be changed as appropriate. Bydefault the ML system (and other contributed packages) are expected inany of the following locations: 1) [ISABELLE_HOME]/contrib 2) [ISABELLE_HOME]/.. 3) /usr/share 4) /usr/local 5) /optThis may be changed by editing [ISABELLE_HOME]/etc/settings manually.The installation may be finished as follows: cd [ISABELLE_HOME] ./configure ./bin/isatool install -p /usr/local/binNote that the configure script is only required for systems that donot have bash and perl in the canonical places (/bin/bash and/usr/bin/perl).The install utility creates global references to the present Isabelleinstallation, enabling users to invoke the Isabelle executableswithout explicit path names. Incidently, this is the only place wherea static reference to [ISABELLE_HOME] is created; thus isatool installhas to be run again whenever the Isabelle distribution is moved later.Compiling logics----------------The Isabelle.tar.gz archive already contains all Isabelle sources (anddocumentation). Precompiled object-logics are provided forconvenience.Assuming proper configuration of the underlying ML system(cf. Isabelle's etc/settings), further object-logics may be compiledlike this: [ISABELLE_HOME]/build FOLSpecial object-logic targets may be specified as follows: [ISABELLE_HOME]/build -m HOL-Real HOL2) User installation--------------------Running the Isabelle binaries-----------------------------Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)directly from their location within the distribution directory[ISABELLE_HOME] like this: [ISABELLE_HOME]/bin/isabelle HOLThis starts an interactive Isabelle session within the current textterminal. [ISABELLE_HOME]/bin may be put into the shell's searchPATH. An alternative is to create global references to the Isabelleexecutables as follows: [ISABELLE_HOME]/bin/isatool install -p ~/binNote that the site-wide Isabelle installation may already provideIsabelle executables in some global bin directory (such as/usr/local/bin).Isabelle as KDE application---------------------------Users may install an Isabelle application icon on the KDE 2 desktop asfollows (version 1 may be specified as well): [ISABELLE_HOME]/bin/isatool install -k 2Clicking on Isabelle will invoke the interface wrapper script (capitalIsabelle), which is usually configured to run Proof General (cf. theISABELLE_INTERFACE setting). Additional options may be passed toIsabelle by editing the application's command line using the standardKDE properties editing facilities.$Id$