--- a/Admin/PLATFORMS Fri Aug 17 11:32:20 2012 +0200
+++ b/Admin/PLATFORMS Fri Aug 17 19:11:51 2012 +0200
@@ -5,21 +5,21 @@
--------
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.
+environment, with as little system-specific code in user-space tools
+as possible.
The basic Isabelle system infrastructure provides some facilities to
-make this work, e.g. see the ML structures File and Path, or functions
-like Isabelle_System.bash. The settings environment also provides
-some means for portability, e.g. jvm_path to keep the impression that
-Java on Windows/Cygwin adheres to Isabelle/POSIX standards (inside the
-JVM itself there are many Windows-specific things, though).
+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 "jvmpath"
+to keep the impression that Java on Windows/Cygwin adheres to
+Isabelle/POSIX standards, although inside the JVM itself there are
+many Windows-specific things.
When producing add-on tools, it is important to stay within this clean
room of Isabelle, and refrain from overly ambitious system hacking.
-The existing Isabelle scripts follow a certain style that might look
-odd at first sight, but it reflects long years of experience in
-getting system plumbing right (which is quite hard).
+The existing Isabelle scripts follow a peculiar style that reflects
+long years of experience in getting system plumbing right.
Supported platforms
@@ -31,23 +31,22 @@
too old nor too new):
x86-linux Ubuntu 10.04 LTS
- x86-darwin Mac OS Leopard (macbroy30)
- Mac OS Snow Leopard (macbroy2)
- Mac OS Lion (macbroy6)
- x86-cygwin Cygwin 1.7 (vmbroy9)
+ x86_64-linux Ubuntu 10.04 LTS
- x86_64-linux Ubuntu 10.04 LTS
- x86_64-darwin Mac OS Leopard (macbroy30)
- Mac OS Snow Leopard (macbroy2)
+ x86_64-darwin Mac OS Snow Leopard (macbroy2)
Mac OS Lion (macbroy6)
+ Mac OS Mountain Lion (macbroy30)
+
+ x86-cygwin Cygwin 1.7 (vmbroy9)
All of the above platforms are 100% supported by Isabelle -- end-users
should not have to care about the differences (at least in theory).
-There are also some additional platforms where Poly/ML also happens to
-work, but they are *not* covered by the official Isabelle
+There are also some additional platforms where Poly/ML might also
+happen to work, but they are *not* covered by the official Isabelle
distribution:
ppc-darwin
+ x86-darwin
sparc-solaris
x86-solaris
x86-bsd
@@ -55,31 +54,45 @@
There are increasing problems to make contributing components of
Isabelle work on such fringe platforms. Note that x86-bsd is silently
treated like x86-linux -- this works if certain Linux compatibility
-packages are installed on BSD.
+packages are installed on BSD. Old 32 bit Macintosh hardware is no
+longer supported due the its lack of Java 7.
32 bit vs. 64 bit platforms
---------------------------
-Most users already have 64 bit hardware, and many of them are running
-a 64 bit operating system. Native 64 bit support for ML and Scala/JVM
-is increasingly important for big Isabelle applications, but 32 bit is
-often the default to get started. Add-on executables need to work
-seamlessly without manual user configuration, either as native 64 bit
-executables or in 32 bit mode on a 64 bit platform.
+Most users have 64 bit hardware and are running a 64 bit operating
+system by default. For Linux this often means missing 32 bit shared
+libraries, so native x86_64-linux needs to be used by default, despite
+its doubled space requirements for Poly/ML heaps. For Mac OS X, the
+x86-darwin personality usually works seamlessly for C/C++ programs,
+but the Java 7 platform is only available for x86_64-darwin.
+
+Add-on executables are expected to without manual user configuration,
+Each component settings script needs to work out the platform details
+appropriately.
+
+The Isabelle settings environment provides the following variables to
+help configuring platform-dependent tools:
+
+ ISABELLE_PLATFORM64 (potentially empty)
+ ISABELLE_PLATFORM32
+ ISABELLE_PLATFORM
The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
-the platform, even on 64 bit hardware. Tools need to indicate 64 bit
-support explicitly via the (optional) ISABELLE_PLATFORM64 setting, if
-this is really required. The following bash expression prefers the 64
-bit platform, if that is available:
+the platform, even on 64 bit hardware. 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}"
- "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
+Moreover note that ML and JVM usually have a different idea of the
+platform, depending on the respective binaries that are actually run.
+Poly/ML 5.5.x runs most efficiently on 32 bit, even for large
+applications. The JVM usually performs better in 64 bit mode.
-Note that ML and JVM may have a different idea of the platform,
-depending on the respective binaries that are actually run. The
-"uname" Unix tool usually only tells about its own executable format,
-not the underlying platform.
+The traditional "uname" Unix tool usually only tells about its own
+executable format, not the underlying platform!
Dependable system tools
@@ -96,8 +109,8 @@
performs not as well in addressing various delicate details of
operating system concepts (processes, signals, sockets etc.).
-* Scala with Java Runtime 1.6. The Isabelle/Scala layer irons out
- many oddities and portability issues of the Java platform.
+* Scala with Java 1.7. The Isabelle/Scala layer irons out many
+ oddities and portability issues of the Java platform.
Known problems
@@ -115,12 +128,8 @@
default.
* The Java runtime has its own idea about the underlying platform,
- e.g. on a 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 cause extra portability problems and can make
- the JVM crash anyway.
-
- In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
+ which affects Java native libraries in particular. In
+ Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
platform. Since there can be many different Java installations on
the same machine, which can also be run with different options,
reliable JVM platform identification works from inside the running
--- a/Admin/README Fri Aug 17 11:32:20 2012 +0200
+++ b/Admin/README Fri Aug 17 19:11:51 2012 +0200
@@ -1,2 +1,2 @@
-This directory contains some administrative tools for the Isabelle
-repository at TUM. They do not appear in proper distributions.
+This directory contains some administrative tools for clones of the
+Isabelle repository. They do not appear in proper distributions.
--- a/Admin/component_repository/components.sha1 Fri Aug 17 11:32:20 2012 +0200
+++ b/Admin/component_repository/components.sha1 Fri Aug 17 19:11:51 2012 +0200
@@ -1,13 +1,16 @@
2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
+ae7ee5becb26512f18c609e83b34612918bae5f0 exec_process-1.0.tar.gz
683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
+ec740ee9ffd43551ddf1e5b91641405116af6291 jdk-7u6.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
9c221fe71af8a063fcffcce21672a97aea0a8d5b jedit_build-20120313.tar.gz
ed72630f307729df08fdedb095f0af8725f81b9c jedit_build-20120327.tar.gz
6425f622625024c1de27f3730d6811f6370a19cd jedit_build-20120414.tar.gz
+7b012f725ec1cc102dc259df178d511cc7890bba jedit_build-20120813.tar.gz
6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz
--- a/Admin/components Fri Aug 17 11:32:20 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-#contributed components
-contrib/cvc3-2.4.1
-contrib/e-1.5
-contrib/hol-light-bundle-0.5-126
-contrib/kodkodi-1.2.16
-contrib/spass-3.8ds
-contrib/vampire-1.0
-contrib/yices-1.0.28
-contrib/z3-4.0
-contrib/jdk-7u6
-contrib/scala-2.9.2
-contrib/jedit_build-20120813
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components/cygwin Fri Aug 17 19:11:51 2012 +0200
@@ -0,0 +1,2 @@
+#specific components for Windows/Cygwin only
+exec_process-1.0
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components/main Fri Aug 17 19:11:51 2012 +0200
@@ -0,0 +1,9 @@
+#main components for everyday use, without big impact on overall build time
+cvc3-2.4.1
+e-1.5
+jdk-7u6
+jedit_build-20120813
+kodkodi-1.2.16
+scala-2.9.2
+spass-3.8ds
+z3-4.0
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components/nonfree Fri Aug 17 19:11:51 2012 +0200
@@ -0,0 +1,3 @@
+#special components for internal testing only
+vampire-1.0
+yices-1.0.28
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components/optional Fri Aug 17 19:11:51 2012 +0200
@@ -0,0 +1,2 @@
+#optional components that could impact build time significantly
+hol-light-bundle-0.5-126
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components_old Fri Aug 17 19:11:51 2012 +0200
@@ -0,0 +1,13 @@
+#contributed components
+contrib/cvc3-2.4.1
+contrib/e-1.5
+contrib/hol-light-bundle-0.5-126
+contrib/kodkodi-1.2.16
+contrib/spass-3.8ds
+contrib/vampire-1.0
+contrib/yices-1.0.28
+contrib/z3-4.0
+contrib/jdk-7u6
+contrib/scala-2.9.2
+contrib/jedit_build-20120813
+
--- a/Admin/init_components Fri Aug 17 11:32:20 2012 +0200
+++ b/Admin/init_components Fri Aug 17 19:11:51 2012 +0200
@@ -12,4 +12,4 @@
/*) init_component "$REPLY" ;;
*) init_component "$COMPONENT/$REPLY" ;;
esac
-done < "$ISABELLE_HOME/Admin/components"
+done < "$ISABELLE_HOME/Admin/components_old"
--- a/Admin/lib/Tools/download_components Fri Aug 17 11:32:20 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,135 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Florian Haftmann
-# Author: Tjark Weber
-#
-# DESCRIPTION: download Isabelle components
-
-shopt -s -o errexit
-shopt -s -o nounset
-
-## directory layout
-
-: ${TMPDIR:="/tmp"}
-
-LOCAL="${ISABELLE_HOME_USER}/contrib"
-
-REMOTE="http://isabelle.in.tum.de/components"
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-trap 'echo "Error in ${PRG}" >&2' ERR
-
-function usage()
-{
- cat <<EOF
-
-Usage: ${PRG} [OPTIONS] [COMPONENTS ...]
-
- Options are:
- -c Download current components (as listed in Admin/components).
- -q Quiet (do not output diagnostic messages).
- -r Replace components already present (default is to skip).
- -x Exit on failed download (default is to ignore).
-
- Download and unpack Isabelle components from central component store
- (${REMOTE}/).
-
-EOF
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-## process command line
-
-# options
-
-DOWNLOAD_CURRENT=""
-ECHO="echo"
-REPLACE_EXISTING=""
-EXIT_ON_FAILED_DOWNLOAD=""
-
-function getoptions()
-{
- OPTIND=1
- while getopts "cqrx" OPT
- do
- case "$OPT" in
- c)
- DOWNLOAD_CURRENT=true
- ;;
- q)
- ECHO=":"
- ;;
- r)
- REPLACE_EXISTING=true
- ;;
- x)
- EXIT_ON_FAILED_DOWNLOAD=true
- ;;
- \?)
- usage
- ;;
- esac
- done
-}
-
-getoptions "$@"
-shift $(($OPTIND - 1))
-
-## download (and unpack) components
-
-function download()
-{
- if [ -e "${LOCAL}/${COMPONENT}" -a -z "${REPLACE_EXISTING}" ]; then
- "${ECHO}" "Skipping existing component ${COMPONENT}"
- else
- "${ECHO}" "${COMPONENT}"
- ARCHIVE="${COMPONENT}.tar.gz"
- if curl -s `"${ECHO}" --no-silent` -f -o "${TMPDIR}/${ARCHIVE}" "${REMOTE}/${ARCHIVE}"; then
- if [ -n "${REPLACE_EXISTING}" ]; then
- tar -xzf "${TMPDIR}/${ARCHIVE}" -C "${LOCAL}" --recursive-unlink
- else
- tar -xzf "${TMPDIR}/${ARCHIVE}" -C "${LOCAL}"
- fi
- else
- if [ -n "${EXIT_ON_FAILED_DOWNLOAD}" ]; then
- fail "Error downloading component ${COMPONENT} (non-free?)"
- else
- "${ECHO}" "Error downloading component ${COMPONENT} (non-free?)"
- fi
- fi
- fi
-}
-
-"${ECHO}" "Unpacking components into ${LOCAL}/"
-
-mkdir -p "${LOCAL}"
-
-# process Admin/components
-if [ -n "${DOWNLOAD_CURRENT}" ]; then
- while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
- do
- case "${REPLY}" in
- \#* | "")
- ;;
- *)
- COMPONENT="$(basename "${REPLY}")"
- download "${COMPONENT}"
- ;;
- esac
- done < "${ISABELLE_HOME}/Admin/components"
-fi
-
-# process args
-for COMPONENT in "$@"
-do
- download "${COMPONENT}"
-done
--- a/Admin/mira.py Fri Aug 17 11:32:20 2012 +0200
+++ b/Admin/mira.py Fri Aug 17 19:11:51 2012 +0200
@@ -39,7 +39,9 @@
Z3_NON_COMMERCIAL="yes"
-source "${ISABELLE_HOME}/Admin/init_components"
+init_components "$COMPONENT/contrib" "$ISABELLE_HOME/Admin/components/main"
+init_components "$COMPONENT/contrib" "$ISABELLE_HOME/Admin/components/optional"
+init_components "$COMPONENT/contrib" "$ISABELLE_HOME/Admin/components/nonfree"
''' + more_settings
--- a/NEWS Fri Aug 17 11:32:20 2012 +0200
+++ b/NEWS Fri Aug 17 19:11:51 2012 +0200
@@ -106,6 +106,10 @@
with "isabelle build", similar to former "isabelle mkdir" for
"isabelle usedir".
+* The "isabelle components" tool helps to resolve add-on components
+that are not bundled, or referenced from a bare-bones repository
+version of Isabelle.
+
* Discontinued support for Poly/ML 5.2.1, which was the last version
without exception positions and advanced ML compiler/toplevel
configuration.
--- a/README_REPOSITORY Fri Aug 17 11:32:20 2012 +0200
+++ b/README_REPOSITORY Fri Aug 17 19:11:51 2012 +0200
@@ -233,28 +233,34 @@
Building a repository version of Isabelle
-----------------------------------------
-A proper Isabelle distribution contains many add-on components that
-are important for practical use. Some extra configuration is required
-to approximate this system integration from a bare-bones repository
-snapshot; see also its directory Admin/ (which is absent in official
-releases).
+The regular "isabelle build" tool allows to build session images as
+usual, but this first requires to resolve add-on components first,
+including the ML system. Some extra configuration is required to
+approximate some of the system integration of official Isabelle
+releases from a bare-bones repository snapshot. The special directory
+Admin/ -- which is absent in official releases -- might provide some
+further clues.
- (1) Admin/components lists potentially relevant components, with
- explicit version information for the given repository version.
- For example, this allows to bisect over Mercurial history while
- the contributing components change accordingly.
+Here is a reasonably easy way to include important Isabelle components
+on the spot:
+
+ (1) The bash script ISABELLE_HOME_USER/etc/settings is augmented by
+ some shell function invocations like this:
- (2) Admin/init_components is a bash script that can be sourced in
- $ISABELLE_HOME_USER/etc/settings to initialize components listed
- in Admin/components and present in $ISABELLE_HOME_USER/contrib/.
+ init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"
+ init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/optional"
+
+ This uses some central place "$HOME/.isabelle/contrib" to keep
+ component directories that are shared by all Isabelle versions.
+
+ (2) Missing components are resolved on the command line like this:
- (3) http://isabelle.in.tum.de/components/ provides tar.gz archives
- of many components, excluding some non-free ones (which are also
- not part of Isabelle releases).
+ isabelle components -a
+
+ This will saturate the "$HOME/.isabelle/contrib" directory structure
+ from according to $ISABELLE_COMPONENT_REPOSITORY.
-Also note that the repository lacks some textual version identifiers
-in the sources and scripts; this implies some changed behavior when
-processing settings etc. -- especially the location of
-$ISABELLE_HOME_USER provided by the system.
-
-The isabelle build tool allows to build logic images.
+Since the given component catalogs in $ISABELLE_HOME/Admin/components
+are subject to the Mercurial history, it is possible to bisect over a
+range of Isabelle versions while references to the contributing
+components change accordingly.
--- a/doc-src/System/Thy/Basics.thy Fri Aug 17 11:32:20 2012 +0200
+++ b/doc-src/System/Thy/Basics.thy Fri Aug 17 19:11:51 2012 +0200
@@ -299,18 +299,18 @@
For example, the following setting allows to refer to files within
the component later on, without having to hardwire absolute paths:
- \begin{ttbox}
- MY_COMPONENT_HOME="$COMPONENT"
- \end{ttbox}
+\begin{ttbox}
+MY_COMPONENT_HOME="$COMPONENT"
+\end{ttbox}
Components can also add to existing Isabelle settings such as
@{setting_def ISABELLE_TOOLS}, in order to provide
component-specific tools that can be invoked by end-users. For
example:
- \begin{ttbox}
- ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
- \end{ttbox}
+\begin{ttbox}
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+\end{ttbox}
\item @{verbatim "etc/components"} holds a list of further
sub-components of the same structure. The directory specifications
@@ -328,12 +328,27 @@
\verb,init_component, shell function in the \verb,etc/settings,
script of \verb,$ISABELLE_HOME_USER, (or any other component
directory). For example:
- \begin{verbatim}
- if [ -d "$HOME/screwdriver-2.0" ]
- then
- init_component "$HOME/screwdriver-2.0"
- else
- \end{verbatim}
+\begin{ttbox}
+init_component "$HOME/screwdriver-2.0"
+\end{ttbox}
+
+ This is tolerant wrt.\ missing component directories, but might
+ produce a warning.
+
+ \medskip More complex situations may be addressed by initializing
+ components listed in a given catalog file, relatively to some base
+ directory:
+
+\begin{ttbox}
+init_components "$HOME/my_component_store" "some_catalog_file"
+\end{ttbox}
+
+ The component directories listed in the catalog file are treated as
+ relative to the given base directory.
+
+ See also \secref{sec:tool-components} for some tool-support for
+ resolving components that are formally initialized but not installed
+ yet.
*}
--- a/doc-src/System/Thy/Misc.thy Fri Aug 17 11:32:20 2012 +0200
+++ b/doc-src/System/Thy/Misc.thy Fri Aug 17 19:11:51 2012 +0200
@@ -10,6 +10,48 @@
*}
+section {* Resolving Isabelle components \label{sec:tool-components} *}
+
+text {*
+ The @{tool_def components} tool resolves Isabelle components:
+\begin{ttbox}
+Usage: isabelle components [OPTIONS] [COMPONENTS ...]
+
+ Options are:
+ -R URL component repository
+ (default $ISABELLE_COMPONENT_REPOSITORY)
+ -a all missing components
+ -l list status
+
+ Resolve Isabelle components via download and installation.
+ COMPONENTS are identified via base name.
+
+ ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
+\end{ttbox}
+
+ Components are initialized as described in \secref{sec:components}
+ in a permissive manner, which can mark components as ``missing''.
+ This state is amended by letting @{tool "components"} download and
+ unpack components that are published on the default component
+ repository \url{http://isabelle.in.tum.de/components/} in
+ particular.
+
+ Option @{verbatim "-R"} specifies an alternative component
+ repository. Note that @{verbatim "file:///"} URLs can be used for
+ local directories.
+
+ Option @{verbatim "-a"} selects all missing components to be
+ installed. Explicit components may be named as command
+ line-arguments as well. Note that components are uniquely
+ identified by their base name, while the installation takes place in
+ the location that was specified in the attempt to initialize the
+ component before.
+
+ Option @{verbatim "-l"} lists the current state of available and
+ missing components with their location (full name) within the
+ file-system. *}
+
+
section {* Displaying documents *}
text {* The @{tool_def display} tool displays documents in DVI or PDF
--- a/doc-src/System/Thy/document/Basics.tex Fri Aug 17 11:32:20 2012 +0200
+++ b/doc-src/System/Thy/document/Basics.tex Fri Aug 17 19:11:51 2012 +0200
@@ -310,18 +310,18 @@
For example, the following setting allows to refer to files within
the component later on, without having to hardwire absolute paths:
- \begin{ttbox}
- MY_COMPONENT_HOME="$COMPONENT"
- \end{ttbox}
+\begin{ttbox}
+MY_COMPONENT_HOME="$COMPONENT"
+\end{ttbox}
Components can also add to existing Isabelle settings such as
\indexdef{}{setting}{ISABELLE\_TOOLS}\hypertarget{setting.ISABELLE-TOOLS}{\hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}TOOLS}}}}}, in order to provide
component-specific tools that can be invoked by end-users. For
example:
- \begin{ttbox}
- ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
- \end{ttbox}
+\begin{ttbox}
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+\end{ttbox}
\item \verb|etc/components| holds a list of further
sub-components of the same structure. The directory specifications
@@ -339,12 +339,27 @@
\verb,init_component, shell function in the \verb,etc/settings,
script of \verb,$ISABELLE_HOME_USER, (or any other component
directory). For example:
- \begin{verbatim}
- if [ -d "$HOME/screwdriver-2.0" ]
- then
- init_component "$HOME/screwdriver-2.0"
- else
- \end{verbatim}%
+\begin{ttbox}
+init_component "$HOME/screwdriver-2.0"
+\end{ttbox}
+
+ This is tolerant wrt.\ missing component directories, but might
+ produce a warning.
+
+ \medskip More complex situations may be addressed by initializing
+ components listed in a given catalog file, relatively to some base
+ directory:
+
+\begin{ttbox}
+init_components "$HOME/my_component_store" "some_catalog_file"
+\end{ttbox}
+
+ The component directories listed in the catalog file are treated as
+ relative to the given base directory.
+
+ See also \secref{sec:tool-components} for some tool-support for
+ resolving components that are formally initialized but not installed
+ yet.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/System/Thy/document/Misc.tex Fri Aug 17 11:32:20 2012 +0200
+++ b/doc-src/System/Thy/document/Misc.tex Fri Aug 17 19:11:51 2012 +0200
@@ -28,6 +28,51 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{Resolving Isabelle components \label{sec:tool-components}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \indexdef{}{tool}{components}\hypertarget{tool.components}{\hyperlink{tool.components}{\mbox{\isa{\isatool{components}}}}} tool resolves Isabelle components:
+\begin{ttbox}
+Usage: isabelle components [OPTIONS] [COMPONENTS ...]
+
+ Options are:
+ -R URL component repository
+ (default $ISABELLE_COMPONENT_REPOSITORY)
+ -a all missing components
+ -l list status
+
+ Resolve Isabelle components via download and installation.
+ COMPONENTS are identified via base name.
+
+ ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
+\end{ttbox}
+
+ Components are initialized as described in \secref{sec:components}
+ in a permissive manner, which can mark components as ``missing''.
+ This state is amended by letting \hyperlink{tool.components}{\mbox{\isa{\isatool{components}}}} download and
+ unpack components that are published on the default component
+ repository \url{http://isabelle.in.tum.de/components/} in
+ particular.
+
+ Option \verb|-R| specifies an alternative component
+ repository. Note that \verb|file:///| URLs can be used for
+ local directories.
+
+ Option \verb|-a| selects all missing components to be
+ installed. Explicit components may be named as command
+ line-arguments as well. Note that components are uniquely
+ identified by their base name, while the installation takes place in
+ the location that was specified in the attempt to initialize the
+ component before.
+
+ Option \verb|-l| lists the current state of available and
+ missing components with their location (full name) within the
+ file-system.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Displaying documents%
}
\isamarkuptrue%
--- a/etc/components Fri Aug 17 11:32:20 2012 +0200
+++ b/etc/components Fri Aug 17 19:11:51 2012 +0200
@@ -10,7 +10,6 @@
src/LCF
src/Sequents
#misc components
-doc-src
src/Tools/Code
src/Tools/jEdit
src/Tools/WWW_Find
@@ -21,3 +20,4 @@
src/HOL/Tools/Predicate_Compile
src/HOL/Tools/SMT
src/HOL/TPTP
+doc-src
--- a/etc/settings Fri Aug 17 11:32:20 2012 +0200
+++ b/etc/settings Fri Aug 17 19:11:51 2012 +0200
@@ -96,6 +96,8 @@
### Misc path settings
###
+ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
+
# The place for user configuration, heap files, etc.
if [ -z "$ISABELLE_IDENTIFIER" ]; then
ISABELLE_HOME_USER="$USER_HOME/.isabelle"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/components Fri Aug 17 19:11:51 2012 +0200
@@ -0,0 +1,121 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: resolve Isabelle components
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]"
+ echo
+ echo " Options are:"
+ echo " -R URL component repository (default \$ISABELLE_COMPONENT_REPOSITORY)"
+ echo " -a all missing components"
+ echo " -l list status"
+ echo
+ echo " Resolve Isabelle components via download and installation."
+ echo " COMPONENTS are identified via base name."
+ echo
+ echo " ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+#options
+
+COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
+ALL_MISSING=""
+LIST_ONLY=""
+
+while getopts "R:al" OPT
+do
+ case "$OPT" in
+ R)
+ COMPONENT_REPOSITORY="$OPTARG"
+ ;;
+ a)
+ ALL_MISSING="true"
+ ;;
+ l)
+ LIST_ONLY="true"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ "$#" -eq 0 -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage
+
+if [ -z "$ALL_MISSING" ]; then
+ splitarray ":" "$@"
+else
+ splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@"
+fi
+declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}")
+
+
+## main
+
+splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}")
+splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}")
+
+if [ -n "$LIST_ONLY" ]; then
+ echo
+ echo "Available components:"
+ for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo " $NAME"; done
+ echo
+ echo "Missing components:"
+ for NAME in "${MISSING_COMPONENTS[@]}"; do echo " $NAME"; done
+else
+ for NAME in "${SELECTED_COMPONENTS[@]}"
+ do
+ BASE_NAME="$(basename "$NAME")"
+ FULL_NAME=""
+ for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}"
+ do
+ [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X"
+ done
+ if [ -z "$FULL_NAME" ]; then
+ echo "Ignoring irrelevant component \"$NAME\""
+ elif [ -d "$FULL_NAME" ]; then
+ echo "Skipping existing component \"$FULL_NAME\""
+ else
+ if [ ! -e "${FULL_NAME}.tar.gz" ]; then
+ REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
+ echo "Getting \"$REMOTE\""
+ mkdir -p "$(dirname "$FULL_NAME")"
+ perl -MLWP::Simple -e "getprint '$REMOTE';" > "${FULL_NAME}.tar.gz"
+ if perl -e "exit((stat('${FULL_NAME}.tar.gz'))[7] == 0 ? 0 : 1);"
+ then
+ rm -f "${FULL_NAME}.tar.gz"
+ fi
+ fi
+ if [ -e "${FULL_NAME}.tar.gz" ]; then
+ echo "Unpacking \"${FULL_NAME}.tar.gz\""
+ tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz"
+ fi
+ fi
+ done
+fi
+
--- a/lib/Tools/version Fri Aug 17 11:32:20 2012 +0200
+++ b/lib/Tools/version Fri Aug 17 19:11:51 2012 +0200
@@ -60,7 +60,7 @@
if [ -n "$ISABELLE_ID" ]; then
echo "$ISABELLE_ID"
else
- ${HG:-hg} id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
+ "${HG:-hg}" id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
fi
else
echo 'unidentified repository version' # filled in automatically!
--- a/lib/scripts/getsettings Fri Aug 17 11:32:20 2012 +0200
+++ b/lib/scripts/getsettings Fri Aug 17 19:11:51 2012 +0200
@@ -11,7 +11,7 @@
ISABELLE_SETTINGS_PRESENT=true
-#Cygwin vs Posix
+#Cygwin vs. POSIX
if [ "$OSTYPE" = cygwin ]
then
if [ -z "$USER_HOME" ]; then
@@ -34,11 +34,6 @@
fi
export ISABELLE_HOME
-if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
-then
- echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!"
- echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
-fi
#key executables
ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
@@ -58,7 +53,7 @@
#Isabelle distribution identifier -- filled in automatically!
ISABELLE_ID=""
-ISABELLE_IDENTIFIER=""
+[ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
#sometimes users put strange things in here ...
unset ENV
@@ -153,8 +148,13 @@
done
}
-#nested components
+
+# components
+
ISABELLE_COMPONENTS=""
+ISABELLE_COMPONENTS_MISSING=""
+
+#init component tree
function init_component ()
{
local COMPONENT="$1"
@@ -166,13 +166,21 @@
;;
esac
- if [ ! -d "$COMPONENT" ]; then
+ if [ -d "$COMPONENT" ]; then
+ if [ -z "$ISABELLE_COMPONENTS" ]; then
+ ISABELLE_COMPONENTS="$COMPONENT"
+ else
+ ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
+ fi
+ else
echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
- elif [ -z "$ISABELLE_COMPONENTS" ]; then
- ISABELLE_COMPONENTS="$COMPONENT"
- else
- ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
+ if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
+ ISABELLE_COMPONENTS_MISSING="$COMPONENT"
+ else
+ ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
+ fi
fi
+
if [ -f "$COMPONENT/etc/settings" ]; then
source "$COMPONENT/etc/settings"
local RC="$?"
@@ -182,17 +190,34 @@
fi
fi
if [ -f "$COMPONENT/etc/components" ]; then
- {
- while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
- do
- case "$REPLY" in
- \#* | "") ;;
- /*) init_component "$REPLY" ;;
- *) init_component "$COMPONENT/$REPLY" ;;
- esac
- done
- } < "$COMPONENT/etc/components"
+ init_components "$COMPONENT" "$COMPONENT/etc/components"
+ fi
+}
+
+#init component forest
+function init_components ()
+{
+ local BASE="$1"
+ local CATALOG="$2"
+
+ if [ ! -d "$BASE" ]; then
+ echo >&2 "Bad component base directory: \"$BASE\""
+ exit 2
fi
+ if [ ! -f "$CATALOG" ]; then
+ echo >&2 "Bad component catalog file: \"$CATALOG\""
+ exit 2
+ fi
+ {
+ while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
+ do
+ case "$REPLY" in
+ \#* | "") ;;
+ /*) init_component "$REPLY" ;;
+ *) init_component "$BASE/$REPLY" ;;
+ esac
+ done
+ } < "$CATALOG"
}
#main components
@@ -200,6 +225,7 @@
[ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
[ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
+
#ML system identifier
if [ -z "$ML_PLATFORM" ]; then
ML_IDENTIFIER="$ML_SYSTEM"
@@ -207,11 +233,11 @@
ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
fi
+ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
+
#enforce JAVA_HOME
export JAVA_HOME="$ISABELLE_JDK_HOME"
-ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
-
#build condition etc.
case "$ML_SYSTEM" in
polyml*)