# HG changeset patch # User wenzelm # Date 1345217707 -7200 # Node ID 6408fb6f7d81241ceb119c3fb02069a80e4d3f9d # Parent 9055bf115e30423a55fc22c526c4a92cef4b3b2e some explanations on isabelle components; diff -r 9055bf115e30 -r 6408fb6f7d81 NEWS --- a/NEWS Fri Aug 17 17:52:10 2012 +0200 +++ b/NEWS Fri Aug 17 17:35:07 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. diff -r 9055bf115e30 -r 6408fb6f7d81 README_REPOSITORY --- a/README_REPOSITORY Fri Aug 17 17:52:10 2012 +0200 +++ b/README_REPOSITORY Fri Aug 17 17:35:07 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. diff -r 9055bf115e30 -r 6408fb6f7d81 doc-src/System/Thy/Basics.thy --- a/doc-src/System/Thy/Basics.thy Fri Aug 17 17:52:10 2012 +0200 +++ b/doc-src/System/Thy/Basics.thy Fri Aug 17 17:35:07 2012 +0200 @@ -345,6 +345,10 @@ 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. *} diff -r 9055bf115e30 -r 6408fb6f7d81 doc-src/System/Thy/Misc.thy --- a/doc-src/System/Thy/Misc.thy Fri Aug 17 17:52:10 2012 +0200 +++ b/doc-src/System/Thy/Misc.thy Fri Aug 17 17:35:07 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 diff -r 9055bf115e30 -r 6408fb6f7d81 doc-src/System/Thy/document/Basics.tex --- a/doc-src/System/Thy/document/Basics.tex Fri Aug 17 17:52:10 2012 +0200 +++ b/doc-src/System/Thy/document/Basics.tex Fri Aug 17 17:35:07 2012 +0200 @@ -355,7 +355,11 @@ \end{ttbox} The component directories listed in the catalog file are treated as - relative to the given base directory.% + 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% % diff -r 9055bf115e30 -r 6408fb6f7d81 doc-src/System/Thy/document/Misc.tex --- a/doc-src/System/Thy/document/Misc.tex Fri Aug 17 17:52:10 2012 +0200 +++ b/doc-src/System/Thy/document/Misc.tex Fri Aug 17 17:35:07 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%