some explanations on isabelle components;
authorwenzelm
Fri Aug 17 17:35:07 2012 +0200 (2012-08-17)
changeset 488446408fb6f7d81
parent 48843 9055bf115e30
child 48845 eb2b65c348ca
some explanations on isabelle components;
NEWS
README_REPOSITORY
doc-src/System/Thy/Basics.thy
doc-src/System/Thy/Misc.thy
doc-src/System/Thy/document/Basics.tex
doc-src/System/Thy/document/Misc.tex
     1.1 --- a/NEWS	Fri Aug 17 17:52:10 2012 +0200
     1.2 +++ b/NEWS	Fri Aug 17 17:35:07 2012 +0200
     1.3 @@ -106,6 +106,10 @@
     1.4  with "isabelle build", similar to former "isabelle mkdir" for
     1.5  "isabelle usedir".
     1.6  
     1.7 +* The "isabelle components" tool helps to resolve add-on components
     1.8 +that are not bundled, or referenced from a bare-bones repository
     1.9 +version of Isabelle.
    1.10 +
    1.11  * Discontinued support for Poly/ML 5.2.1, which was the last version
    1.12  without exception positions and advanced ML compiler/toplevel
    1.13  configuration.
     2.1 --- a/README_REPOSITORY	Fri Aug 17 17:52:10 2012 +0200
     2.2 +++ b/README_REPOSITORY	Fri Aug 17 17:35:07 2012 +0200
     2.3 @@ -233,28 +233,34 @@
     2.4  Building a repository version of Isabelle
     2.5  -----------------------------------------
     2.6  
     2.7 -A proper Isabelle distribution contains many add-on components that
     2.8 -are important for practical use.  Some extra configuration is required
     2.9 -to approximate this system integration from a bare-bones repository
    2.10 -snapshot; see also its directory Admin/ (which is absent in official
    2.11 -releases).
    2.12 +The regular "isabelle build" tool allows to build session images as
    2.13 +usual, but this first requires to resolve add-on components first,
    2.14 +including the ML system.  Some extra configuration is required to
    2.15 +approximate some of the system integration of official Isabelle
    2.16 +releases from a bare-bones repository snapshot.  The special directory
    2.17 +Admin/ -- which is absent in official releases -- might provide some
    2.18 +further clues.
    2.19  
    2.20 -  (1) Admin/components lists potentially relevant components, with
    2.21 -    explicit version information for the given repository version.
    2.22 -    For example, this allows to bisect over Mercurial history while
    2.23 -    the contributing components change accordingly.
    2.24 +Here is a reasonably easy way to include important Isabelle components
    2.25 +on the spot:
    2.26 +
    2.27 +  (1) The bash script ISABELLE_HOME_USER/etc/settings is augmented by
    2.28 +  some shell function invocations like this:
    2.29  
    2.30 -  (2) Admin/init_components is a bash script that can be sourced in
    2.31 -    $ISABELLE_HOME_USER/etc/settings to initialize components listed
    2.32 -    in Admin/components and present in $ISABELLE_HOME_USER/contrib/.
    2.33 +      init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"
    2.34 +      init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/optional"
    2.35 +
    2.36 +  This uses some central place "$HOME/.isabelle/contrib" to keep
    2.37 +  component directories that are shared by all Isabelle versions.
    2.38 +
    2.39 +  (2) Missing components are resolved on the command line like this:
    2.40  
    2.41 -  (3) http://isabelle.in.tum.de/components/ provides tar.gz archives
    2.42 -    of many components, excluding some non-free ones (which are also
    2.43 -    not part of Isabelle releases).
    2.44 +      isabelle components -a
    2.45 +
    2.46 +  This will saturate the "$HOME/.isabelle/contrib" directory structure
    2.47 +  from according to $ISABELLE_COMPONENT_REPOSITORY.
    2.48  
    2.49 -Also note that the repository lacks some textual version identifiers
    2.50 -in the sources and scripts; this implies some changed behavior when
    2.51 -processing settings etc. -- especially the location of
    2.52 -$ISABELLE_HOME_USER provided by the system.
    2.53 -
    2.54 -The isabelle build tool allows to build logic images.
    2.55 +Since the given component catalogs in $ISABELLE_HOME/Admin/components
    2.56 +are subject to the Mercurial history, it is possible to bisect over a
    2.57 +range of Isabelle versions while references to the contributing
    2.58 +components change accordingly.
     3.1 --- a/doc-src/System/Thy/Basics.thy	Fri Aug 17 17:52:10 2012 +0200
     3.2 +++ b/doc-src/System/Thy/Basics.thy	Fri Aug 17 17:35:07 2012 +0200
     3.3 @@ -345,6 +345,10 @@
     3.4  
     3.5    The component directories listed in the catalog file are treated as
     3.6    relative to the given base directory.
     3.7 +
     3.8 +  See also \secref{sec:tool-components} for some tool-support for
     3.9 +  resolving components that are formally initialized but not installed
    3.10 +  yet.
    3.11  *}
    3.12  
    3.13  
     4.1 --- a/doc-src/System/Thy/Misc.thy	Fri Aug 17 17:52:10 2012 +0200
     4.2 +++ b/doc-src/System/Thy/Misc.thy	Fri Aug 17 17:35:07 2012 +0200
     4.3 @@ -10,6 +10,48 @@
     4.4  *}
     4.5  
     4.6  
     4.7 +section {* Resolving Isabelle components \label{sec:tool-components} *}
     4.8 +
     4.9 +text {*
    4.10 +  The @{tool_def components} tool resolves Isabelle components:
    4.11 +\begin{ttbox}
    4.12 +Usage: isabelle components [OPTIONS] [COMPONENTS ...]
    4.13 +
    4.14 +  Options are:
    4.15 +    -R URL       component repository
    4.16 +                 (default $ISABELLE_COMPONENT_REPOSITORY)
    4.17 +    -a           all missing components
    4.18 +    -l           list status
    4.19 +
    4.20 +  Resolve Isabelle components via download and installation.
    4.21 +  COMPONENTS are identified via base name.
    4.22 +
    4.23 +  ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
    4.24 +\end{ttbox}
    4.25 +
    4.26 +  Components are initialized as described in \secref{sec:components}
    4.27 +  in a permissive manner, which can mark components as ``missing''.
    4.28 +  This state is amended by letting @{tool "components"} download and
    4.29 +  unpack components that are published on the default component
    4.30 +  repository \url{http://isabelle.in.tum.de/components/} in
    4.31 +  particular.
    4.32 +
    4.33 +  Option @{verbatim "-R"} specifies an alternative component
    4.34 +  repository.  Note that @{verbatim "file:///"} URLs can be used for
    4.35 +  local directories.
    4.36 +
    4.37 +  Option @{verbatim "-a"} selects all missing components to be
    4.38 +  installed.  Explicit components may be named as command
    4.39 +  line-arguments as well.  Note that components are uniquely
    4.40 +  identified by their base name, while the installation takes place in
    4.41 +  the location that was specified in the attempt to initialize the
    4.42 +  component before.
    4.43 +
    4.44 +  Option @{verbatim "-l"} lists the current state of available and
    4.45 +  missing components with their location (full name) within the
    4.46 +  file-system.  *}
    4.47 +
    4.48 +
    4.49  section {* Displaying documents *}
    4.50  
    4.51  text {* The @{tool_def display} tool displays documents in DVI or PDF
     5.1 --- a/doc-src/System/Thy/document/Basics.tex	Fri Aug 17 17:52:10 2012 +0200
     5.2 +++ b/doc-src/System/Thy/document/Basics.tex	Fri Aug 17 17:35:07 2012 +0200
     5.3 @@ -355,7 +355,11 @@
     5.4  \end{ttbox}
     5.5  
     5.6    The component directories listed in the catalog file are treated as
     5.7 -  relative to the given base directory.%
     5.8 +  relative to the given base directory.
     5.9 +
    5.10 +  See also \secref{sec:tool-components} for some tool-support for
    5.11 +  resolving components that are formally initialized but not installed
    5.12 +  yet.%
    5.13  \end{isamarkuptext}%
    5.14  \isamarkuptrue%
    5.15  %
     6.1 --- a/doc-src/System/Thy/document/Misc.tex	Fri Aug 17 17:52:10 2012 +0200
     6.2 +++ b/doc-src/System/Thy/document/Misc.tex	Fri Aug 17 17:35:07 2012 +0200
     6.3 @@ -28,6 +28,51 @@
     6.4  \end{isamarkuptext}%
     6.5  \isamarkuptrue%
     6.6  %
     6.7 +\isamarkupsection{Resolving Isabelle components \label{sec:tool-components}%
     6.8 +}
     6.9 +\isamarkuptrue%
    6.10 +%
    6.11 +\begin{isamarkuptext}%
    6.12 +The \indexdef{}{tool}{components}\hypertarget{tool.components}{\hyperlink{tool.components}{\mbox{\isa{\isatool{components}}}}} tool resolves Isabelle components:
    6.13 +\begin{ttbox}
    6.14 +Usage: isabelle components [OPTIONS] [COMPONENTS ...]
    6.15 +
    6.16 +  Options are:
    6.17 +    -R URL       component repository
    6.18 +                 (default $ISABELLE_COMPONENT_REPOSITORY)
    6.19 +    -a           all missing components
    6.20 +    -l           list status
    6.21 +
    6.22 +  Resolve Isabelle components via download and installation.
    6.23 +  COMPONENTS are identified via base name.
    6.24 +
    6.25 +  ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
    6.26 +\end{ttbox}
    6.27 +
    6.28 +  Components are initialized as described in \secref{sec:components}
    6.29 +  in a permissive manner, which can mark components as ``missing''.
    6.30 +  This state is amended by letting \hyperlink{tool.components}{\mbox{\isa{\isatool{components}}}} download and
    6.31 +  unpack components that are published on the default component
    6.32 +  repository \url{http://isabelle.in.tum.de/components/} in
    6.33 +  particular.
    6.34 +
    6.35 +  Option \verb|-R| specifies an alternative component
    6.36 +  repository.  Note that \verb|file:///| URLs can be used for
    6.37 +  local directories.
    6.38 +
    6.39 +  Option \verb|-a| selects all missing components to be
    6.40 +  installed.  Explicit components may be named as command
    6.41 +  line-arguments as well.  Note that components are uniquely
    6.42 +  identified by their base name, while the installation takes place in
    6.43 +  the location that was specified in the attempt to initialize the
    6.44 +  component before.
    6.45 +
    6.46 +  Option \verb|-l| lists the current state of available and
    6.47 +  missing components with their location (full name) within the
    6.48 +  file-system.%
    6.49 +\end{isamarkuptext}%
    6.50 +\isamarkuptrue%
    6.51 +%
    6.52  \isamarkupsection{Displaying documents%
    6.53  }
    6.54  \isamarkuptrue%