diff -r 8338dd394144 -r b38bc78d9a9d doc-src/Ref/theories.tex --- a/doc-src/Ref/theories.tex Mon May 03 14:43:52 1999 +0200 +++ b/doc-src/Ref/theories.tex Mon May 03 18:35:48 1999 +0200 @@ -33,16 +33,12 @@ Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory definitions; here is an explanation of the constituent parts: \begin{description} -\item[{\it theoryDef}] is the full definition. The new theory is - called $id$. It is the union of the named {\bf parent +\item[{\it theoryDef}] is the full definition. The new theory is called $id$. + It is the union of the named {\bf parent theories}\indexbold{theories!parent}, possibly extended with new - components. \thydx{Pure} and \thydx{CPure} are the basic theories, - which contain only the meta-logic. They differ just in their - concrete syntax for function applications. - - Normally each {\it name\/} is an identifier, the name of the parent theory. - Quoted strings can be used to document additional file dependencies; see - \S\ref{LoadingTheories} for details. + components. \thydx{Pure} and \thydx{CPure} are the basic theories, which + contain only the meta-logic. They differ just in their concrete syntax for + function applications. \item[$classes$] is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\ @@ -231,143 +227,75 @@ \end{itemize} -\section{Loading a new theory}\label{LoadingTheories} -\index{theories!loading}\index{files!reading} +\section{The theory loader}\label{sec:more-theories} +\index{theories!reading}\index{files!reading} + +Isabelle's theory loader manages dependencies of the internal graph of theory +nodes (the \emph{theory database}) and the external view of the file system. +See \S\ref{sec:intro-theories} for its most basic commands, such as +\texttt{use_thy}. There are a few more operations available. + \begin{ttbox} -use_thy : string -> unit -time_use_thy : string -> unit -loadpath : string list ref \hfill{\bf initially {\tt["."]}} +use_thy_only : string -> unit +update_thy : string -> unit +touch_thy : string -> unit delete_tmpfiles : bool ref \hfill{\bf initially true} \end{ttbox} \begin{ttdescription} -\item[\ttindexbold{use_thy} $thyname$] - reads the theory $thyname$ and creates an \ML{} structure as described below. - -\item[\ttindexbold{time_use_thy} $thyname$] - calls {\tt use_thy} $thyname$ and reports the time taken. - -\item[\ttindexbold{loadpath}] - contains a list of directories to search when locating the files that - define a theory. This list is only used if the theory name in {\tt - use_thy} does not specify the path explicitly. - -\item[reset \ttindexbold{delete_tmpfiles};] -suppresses the deletion of temporary files. +\item[\ttindexbold{use_thy_only} $name$;] is similar to \texttt{use_thy}, but + processes the actual theory file $name$\texttt{.thy} only, ignoring + $name$\texttt{.ML}. This might be useful in replaying proof scripts by hand + from the very beginning, starting with the fresh theory. + +\item[\ttindexbold{update_thy} $name$;] is similar to \texttt{use_thy}, but + ensures that theory $name$ is fully up-to-date with respect to the file + system --- apart from $name$ itself its parents may be reloaded as well. + +\item[\ttindexbold{touch_thy} $name$;] marks theory node $name$ of the + internal graph as outdated. While the theory remains usable, subsequent + operations such as \texttt{use_thy} may cause a reload. + +\item[reset \ttindexbold{delete_tmpfiles};] processing theory files usually + involves temporary {\ML} files to be created. By default, these are deleted + afterwards. Resetting the \texttt{delete_tmpfiles} flag inhibits this, + leaving the generated code for debugging purposes. The basic location for + temporary files is determined by the \texttt{ISABELLE_TMP} environment + variable, which is private to the running Isabelle process (it may be + retrieved by \ttindex{getenv} from {\ML}). \end{ttdescription} -% -Each theory definition must reside in a separate file. Let the file -{\it T}{\tt.thy} contain the definition of a theory called~$T$, whose -parent theories are $TB@1$ \dots $TB@n$. Calling -\texttt{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy}, -writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the -latter file. Recursive {\tt use_thy} calls load those parent theories -that have not been loaded previously; the recursive calls may continue -to any depth. One {\tt use_thy} call can read an entire logic -provided all theories are linked appropriately. - -The result is an \ML\ structure~$T$ containing at least a component -{\tt thy} for the new theory and components for each of the rules. -The structure also contains the definitions of the {\tt ML} section, -if present. The file {\tt.{\it T}.thy.ML} is then deleted if {\tt - delete_tmpfiles} is set and no errors occurred. -Finally the file {\it T}{\tt.ML} is read, if it exists. The structure -$T$ is automatically open in this context. Proof scripts typically -refer to its components by unqualified names. +\medskip Theory and {\ML} files are located by skimming through the +directories listed in Isabelle's internal load path, which merely contains the +current directory ``\texttt{.}'' by default. The load path may be accessed by +the following operations. -Some applications construct theories directly by calling \ML\ functions. In -this situation there is no {\tt.thy} file, only an {\tt.ML} file. The -{\tt.ML} file must declare an \ML\ structure having the theory's name and a -component {\tt thy} containing the new theory object. -Section~\ref{sec:pseudo-theories} below describes a way of linking such -theories to their parents. - - -\section{Reloading modified theories}\label{sec:reloading-theories} -\indexbold{theories!reloading} \begin{ttbox} -update : unit -> unit -unlink_thy : string -> unit +show_path: unit -> string list +add_path: string -> unit +del_path: string -> unit +reset_path: unit -> unit \end{ttbox} -Changing a theory on disk often makes it necessary to reload all theories -descended from it. However, {\tt use_thy} reads only one theory, even if -some of the parent theories are out of date. In this case you should call -{\tt update()}. - -Isabelle keeps track of all loaded theories and their files. If -\texttt{use_thy} finds that the theory to be loaded has been read -before, it determines whether to reload the theory as follows. First -it looks for the theory's files in their previous location. If it -finds them, it compares their modification times to the internal data -and stops if they are equal. If the files have been moved, {\tt - use_thy} searches for them as it would for a new theory. After {\tt - use_thy} reloads a theory, it marks the children as out-of-date. \begin{ttdescription} -\item[\ttindexbold{update}()] - reloads all modified theories and their descendants in the correct order. - -\item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing} - informs Isabelle that theory $thyname$ no longer exists. If you delete the - theory files for $thyname$ then you must execute {\tt unlink_thy}; - otherwise {\tt update} will complain about a missing file. +\item[\ttindexbold{show_path}();] displays the load path components in + canonical string representation, which is always according to Unix rules. + +\item[\ttindexbold{add_path} $dir$;] adds component $dir$ to the beginning of + the load path. + +\item[\ttindexbold{del_path} $dir$;] removes any occurrences of component + $dir$ from the load path. + +\item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}'' + (current directory) only. \end{ttdescription} - -\subsection{*Pseudo theories}\label{sec:pseudo-theories} -\indexbold{theories!pseudo}% -Any automatic reloading facility requires complete knowledge of all -dependencies. Sometimes theories depend on objects created in \ML{} files -with no associated theory definition file. These objects may be theories but -they could also be theorems, proof procedures, etc. - -Unless such dependencies are documented, {\tt update} fails to reload these -\ML{} files and the system is left in a state where some objects, such as -theorems, still refer to old versions of theories. This may lead to the -error -\begin{ttbox} -Attempt to merge different versions of theories: \dots -\end{ttbox} -Therefore there is a way to link theories and {\bf orphaned} \ML{} files --- -those not associated with a theory definition. - -Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a -theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses -theorems proved in {\tt orphan.ML}. Then {\tt B.thy} should -mention this dependency as follows: -\begin{ttbox} -B = \(\ldots\) + "orphan" + \(\ldots\) -\end{ttbox} -Quoted strings stand for theories which have to be loaded before the -current theory is read but which are not used in building the base of -theory~$B$. Whenever {\tt orphan} changes and is reloaded, Isabelle -knows that $B$ has to be updated, too. - -Note that it's necessary for {\tt orphan} to declare a special ML -object of type {\tt theory} which is present in all theories. This is -normally achieved by adding the file {\tt orphan.thy} to make {\tt -orphan} a {\bf pseudo theory}. A minimum version of {\tt orphan.thy} -would be - -\begin{ttbox} -orphan = Pure -\end{ttbox} - -which uses {\tt Pure} to make a dummy theory. Normally though the -orphaned file has its own dependencies. If {\tt orphan.ML} depends on -theories or files $A@1$, \ldots, $A@n$, record this by creating the -pseudo theory in the following way: -\begin{ttbox} -orphan = \(A@1\) + \(\ldots\) + \(A@n\) -\end{ttbox} -The resulting theory ensures that {\tt update} reloads {\tt orphan} -whenever it reloads one of the $A@i$. - -For an extensive example of how this technique can be used to link -lots of theory files and load them by just a few {\tt use_thy} calls -see the sources of one of the major object-logics (e.g.\ \ZF). - +In operations referring indirectly to some file, such as +\texttt{use_thy}~$name$, the argument may be prefixed by some directory that +will be used as temporary load path. Note that, depending on which parts of +the ancestry of $name$ are already loaded, the dynamic change of paths might +be hard to predict. Use this feature with care only. \section{Basic operations on theories}\label{BasicOperationsOnTheories}