tuned "Bootstrapping the environment";
authorwenzelm
Tue Aug 04 15:59:57 2009 +0200 (2009-08-04)
changeset 323238185d3bfcbf1
parent 32322 45cb4a86eca2
child 32324 a99e58e043ee
tuned "Bootstrapping the environment";
added "Additional components";
doc-src/System/Thy/Basics.thy
doc-src/System/Thy/document/Basics.tex
     1.1 --- a/doc-src/System/Thy/Basics.thy	Tue Aug 04 15:05:34 2009 +0200
     1.2 +++ b/doc-src/System/Thy/Basics.thy	Tue Aug 04 15:59:57 2009 +0200
     1.3 @@ -59,11 +59,14 @@
     1.4  *}
     1.5  
     1.6  
     1.7 -subsection {* Building the environment *}
     1.8 +subsection {* Bootstrapping the environment \label{sec:boot} *}
     1.9  
    1.10 -text {*
    1.11 -  Whenever any of the Isabelle executables is run, their settings
    1.12 -  environment is put together as follows.
    1.13 +text {* Isabelle executables need to be run within a proper settings
    1.14 +  environment.  This is bootstrapped as described below, on the first
    1.15 +  invocation of one of the outer wrapper scripts (such as
    1.16 +  @{executable_ref isabelle}).  This happens only once for each
    1.17 +  process tree, i.e.\ the environment is passed to subprocesses
    1.18 +  according to regular Unix conventions.
    1.19  
    1.20    \begin{enumerate}
    1.21  
    1.22 @@ -252,6 +255,52 @@
    1.23  *}
    1.24  
    1.25  
    1.26 +subsection {* Additional components \label{sec:components} *}
    1.27 +
    1.28 +text {* Any directory may be registered as an explicit \emph{Isabelle
    1.29 +  component}.  The general layout conventions are that of the main
    1.30 +  Isabelle distribution itself, and the following two files (both
    1.31 +  optional) have a special meaning:
    1.32 +
    1.33 +  \begin{itemize}
    1.34 +
    1.35 +  \item @{verbatim "etc/settings"} holds additional settings that are
    1.36 +  initialized when bootstrapping the overall Isabelle environment,
    1.37 +  cf.\ \secref{sec:boot}.  As usual, the content is interpreted as a
    1.38 +  @{verbatim bash} script.  It may refer to the component's enclosing
    1.39 +  directory via the @{verbatim "COMPONENT"} shell variable.
    1.40 +
    1.41 +  For example, the following setting allows to refer to files within
    1.42 +  the component later on, without having to hardwire absolute paths:
    1.43 +
    1.44 +  \begin{ttbox}
    1.45 +  MY_COMPONENT_HOME="$COMPONENT"
    1.46 +  \end{ttbox}
    1.47 +
    1.48 +  Components can also add to existing Isabelle settings such as
    1.49 +  @{setting_def ISABELLE_TOOLS}, in order to provide
    1.50 +  component-specific tools that can be invoked by end-users.  For
    1.51 +  example:
    1.52 +
    1.53 +  \begin{ttbox}
    1.54 +  ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
    1.55 +  \end{ttbox}
    1.56 +
    1.57 +  \item @{verbatim "etc/components"} holds a list of further
    1.58 +  sub-components of the same structure.  The directory specifications
    1.59 +  given here can be either absolute (with leading @{verbatim "/"}) or
    1.60 +  relative to the component's main directory.
    1.61 +
    1.62 +  \end{itemize}
    1.63 +
    1.64 +  The root of component initialization is @{setting ISABELLE_HOME}
    1.65 +  itself.  After initializing all of its sub-components recursively,
    1.66 +  @{setting ISABELLE_HOME_USER} is included in the same manner (if
    1.67 +  that directory exists).  Thus users can easily add private
    1.68 +  components to @{verbatim "$ISABELLE_HOME_USER/etc/components"}.
    1.69 +*}
    1.70 +
    1.71 +
    1.72  section {* The raw Isabelle process *}
    1.73  
    1.74  text {*
     2.1 --- a/doc-src/System/Thy/document/Basics.tex	Tue Aug 04 15:05:34 2009 +0200
     2.2 +++ b/doc-src/System/Thy/document/Basics.tex	Tue Aug 04 15:59:57 2009 +0200
     2.3 @@ -76,13 +76,17 @@
     2.4  \end{isamarkuptext}%
     2.5  \isamarkuptrue%
     2.6  %
     2.7 -\isamarkupsubsection{Building the environment%
     2.8 +\isamarkupsubsection{Bootstrapping the environment \label{sec:boot}%
     2.9  }
    2.10  \isamarkuptrue%
    2.11  %
    2.12  \begin{isamarkuptext}%
    2.13 -Whenever any of the Isabelle executables is run, their settings
    2.14 -  environment is put together as follows.
    2.15 +Isabelle executables need to be run within a proper settings
    2.16 +  environment.  This is bootstrapped as described below, on the first
    2.17 +  invocation of one of the outer wrapper scripts (such as
    2.18 +  \indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}).  This happens only once for each
    2.19 +  process tree, i.e.\ the environment is passed to subprocesses
    2.20 +  according to regular Unix conventions.
    2.21  
    2.22    \begin{enumerate}
    2.23  
    2.24 @@ -259,6 +263,55 @@
    2.25  \end{isamarkuptext}%
    2.26  \isamarkuptrue%
    2.27  %
    2.28 +\isamarkupsubsection{Additional components \label{sec:components}%
    2.29 +}
    2.30 +\isamarkuptrue%
    2.31 +%
    2.32 +\begin{isamarkuptext}%
    2.33 +Any directory may be registered as an explicit \emph{Isabelle
    2.34 +  component}.  The general layout conventions are that of the main
    2.35 +  Isabelle distribution itself, and the following two files (both
    2.36 +  optional) have a special meaning:
    2.37 +
    2.38 +  \begin{itemize}
    2.39 +
    2.40 +  \item \verb|etc/settings| holds additional settings that are
    2.41 +  initialized when bootstrapping the overall Isabelle environment,
    2.42 +  cf.\ \secref{sec:boot}.  As usual, the content is interpreted as a
    2.43 +  \verb|bash| script.  It may refer to the component's enclosing
    2.44 +  directory via the \verb|COMPONENT| shell variable.
    2.45 +
    2.46 +  For example, the following setting allows to refer to files within
    2.47 +  the component later on, without having to hardwire absolute paths:
    2.48 +
    2.49 +  \begin{ttbox}
    2.50 +  MY_COMPONENT_HOME="$COMPONENT"
    2.51 +  \end{ttbox}
    2.52 +
    2.53 +  Components can also add to existing Isabelle settings such as
    2.54 +  \indexdef{}{setting}{ISABELLE\_TOOLS}\hypertarget{setting.ISABELLE-TOOLS}{\hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOLS}}}}}, in order to provide
    2.55 +  component-specific tools that can be invoked by end-users.  For
    2.56 +  example:
    2.57 +
    2.58 +  \begin{ttbox}
    2.59 +  ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
    2.60 +  \end{ttbox}
    2.61 +
    2.62 +  \item \verb|etc/components| holds a list of further
    2.63 +  sub-components of the same structure.  The directory specifications
    2.64 +  given here can be either absolute (with leading \verb|/|) or
    2.65 +  relative to the component's main directory.
    2.66 +
    2.67 +  \end{itemize}
    2.68 +
    2.69 +  The root of component initialization is \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}
    2.70 +  itself.  After initializing all of its sub-components recursively,
    2.71 +  \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} is included in the same manner (if
    2.72 +  that directory exists).  Thus users can easily add private
    2.73 +  components to \verb|$ISABELLE_HOME_USER/etc/components|.%
    2.74 +\end{isamarkuptext}%
    2.75 +\isamarkuptrue%
    2.76 +%
    2.77  \isamarkupsection{The raw Isabelle process%
    2.78  }
    2.79  \isamarkuptrue%