# HG changeset patch # User wenzelm # Date 1249394397 -7200 # Node ID 8185d3bfcbf19b002dddb7240f1fde0fc24384c9 # Parent 45cb4a86eca2d4eec2bc52c5bcd13dd2331d8076 tuned "Bootstrapping the environment"; added "Additional components"; diff -r 45cb4a86eca2 -r 8185d3bfcbf1 doc-src/System/Thy/Basics.thy --- a/doc-src/System/Thy/Basics.thy Tue Aug 04 15:05:34 2009 +0200 +++ b/doc-src/System/Thy/Basics.thy Tue Aug 04 15:59:57 2009 +0200 @@ -59,11 +59,14 @@ *} -subsection {* Building the environment *} +subsection {* Bootstrapping the environment \label{sec:boot} *} -text {* - Whenever any of the Isabelle executables is run, their settings - environment is put together as follows. +text {* Isabelle executables need to be run within a proper settings + environment. This is bootstrapped as described below, on the first + invocation of one of the outer wrapper scripts (such as + @{executable_ref isabelle}). This happens only once for each + process tree, i.e.\ the environment is passed to subprocesses + according to regular Unix conventions. \begin{enumerate} @@ -252,6 +255,52 @@ *} +subsection {* Additional components \label{sec:components} *} + +text {* Any directory may be registered as an explicit \emph{Isabelle + component}. The general layout conventions are that of the main + Isabelle distribution itself, and the following two files (both + optional) have a special meaning: + + \begin{itemize} + + \item @{verbatim "etc/settings"} holds additional settings that are + initialized when bootstrapping the overall Isabelle environment, + cf.\ \secref{sec:boot}. As usual, the content is interpreted as a + @{verbatim bash} script. It may refer to the component's enclosing + directory via the @{verbatim "COMPONENT"} shell variable. + + 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} + + 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} + + \item @{verbatim "etc/components"} holds a list of further + sub-components of the same structure. The directory specifications + given here can be either absolute (with leading @{verbatim "/"}) or + relative to the component's main directory. + + \end{itemize} + + The root of component initialization is @{setting ISABELLE_HOME} + itself. After initializing all of its sub-components recursively, + @{setting ISABELLE_HOME_USER} is included in the same manner (if + that directory exists). Thus users can easily add private + components to @{verbatim "$ISABELLE_HOME_USER/etc/components"}. +*} + + section {* The raw Isabelle process *} text {* diff -r 45cb4a86eca2 -r 8185d3bfcbf1 doc-src/System/Thy/document/Basics.tex --- a/doc-src/System/Thy/document/Basics.tex Tue Aug 04 15:05:34 2009 +0200 +++ b/doc-src/System/Thy/document/Basics.tex Tue Aug 04 15:59:57 2009 +0200 @@ -76,13 +76,17 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{Building the environment% +\isamarkupsubsection{Bootstrapping the environment \label{sec:boot}% } \isamarkuptrue% % \begin{isamarkuptext}% -Whenever any of the Isabelle executables is run, their settings - environment is put together as follows. +Isabelle executables need to be run within a proper settings + environment. This is bootstrapped as described below, on the first + invocation of one of the outer wrapper scripts (such as + \indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}). This happens only once for each + process tree, i.e.\ the environment is passed to subprocesses + according to regular Unix conventions. \begin{enumerate} @@ -259,6 +263,55 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{Additional components \label{sec:components}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Any directory may be registered as an explicit \emph{Isabelle + component}. The general layout conventions are that of the main + Isabelle distribution itself, and the following two files (both + optional) have a special meaning: + + \begin{itemize} + + \item \verb|etc/settings| holds additional settings that are + initialized when bootstrapping the overall Isabelle environment, + cf.\ \secref{sec:boot}. As usual, the content is interpreted as a + \verb|bash| script. It may refer to the component's enclosing + directory via the \verb|COMPONENT| shell variable. + + 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} + + 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{\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} + + \item \verb|etc/components| holds a list of further + sub-components of the same structure. The directory specifications + given here can be either absolute (with leading \verb|/|) or + relative to the component's main directory. + + \end{itemize} + + The root of component initialization is \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} + itself. After initializing all of its sub-components recursively, + \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} is included in the same manner (if + that directory exists). Thus users can easily add private + components to \verb|$ISABELLE_HOME_USER/etc/components|.% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsection{The raw Isabelle process% } \isamarkuptrue%