\end{opening}
+\tableofcontents
\section{Introduction}
\label{sec:intro}
\subsection{Indexing and searching}
-\subsection{Compilation and decompilation}
+\subsection{Compilation and cleaning}
\label{sec:libmanagement}
%
%-- motivazioni
%\label{sec:libmanagement}
%consistenza: integrita' referenziale
-%Goals: mantenere consistente la rappresentazione della libreria su memoria persistente consentendo di compilare e decompilare le compilation unit (.ma).\\
+%Goals: mantenere consistente la rappresentazione della libreria su
+%memoria persistente consentendo di compilare e pulire le compilation
+%unit (.ma).\\
%Vincoli: dipendenze oggetti-oggetti e metadati-oggetti\\
%Due livelli di gestione libreria, uno e' solo in fase interattiva dove la compilazione e' passo passo: \\
%--- granularita' oggetto per matita interactive\\
disambiguation aliases and the interpretation and notational convention defined,
while the latter is used to store all the metadata needed by
\WHELP{}.
-% Non serve piu' l'update: by --Zack
-% In addition the \GETTER{} component
-% should be updated with the the new mapping between the logical URI
-% and the physical path of objects.
-While this kind of consistency has nothing to do with the nature of
+While the consistency of the data store in the two media has
+nothing to do with the nature of
the content of the library and is thus uninteresting (but really
tedious to implement and keep bug-free), there is a deeper
notion of mathematical consistency we need to provide. Each object
Compilation is rather simple, and the only tricky case is when we want
to compile again the same script, maybe after the removal of a
-theorem. Here the policy is simple: decompile it before recompiling.
-As we will see in the next section decompilation will ensure that
+theorem. Here the policy is simple: clean the output before recompiling.
+As we will see in the next section cleaning will ensure that
there will be no theorems in the development that depends on the
removed items.
-\subsubsection{Decompilation}
+\subsubsection{Cleaning}
-Decompiling an object involves the (recursive)
-decompilation of all the objects that depend on it.
+With the term ``cleaning'' we mean the process of removing all the
+results of an object compilation. In order to keep the consistency of
+the library, cleaning an object requires the (recursive) cleaning
+of all the objects that depend on it (\emph{reverse dependencies}).
The calculation of the reverse dependencies can be computed in two
ways, using the relational database or using a simpler set of metadata
described in \cite{zack-master} and really depends on a relational
database.
-The latter is a fall-back in case the database is not available.\footnote{Due to
-the complex deployment of a large piece of software like a database,
-it is a common practice for the \HELM{} team to use a shared remote
-database, that may be unavailable if the user workstation lacks
-network connectivity.} This facility has to be intended only as a fall-back,
-since the queries of the \WHELP{} technology depend require a working database.
+The latter is a fall-back in case the database is not
+available.\footnote{Due to the complex deployment of a large piece of
+software like a database, it is a common practice for the \HELM{} team
+to use a shared remote database, that may be unavailable if the user
+workstation lacks network connectivity.} This facility has to be
+intended only as a fall-back, since the queries of the \WHELP{}
+technology depend require a working database.
-Decompilation guarantees that if an object is removed there are no
-dandling references to it, and that the part of the library still
-compiled is logically consistent. Since decompilation involves the
-removal of all the results of the compilation, metadata included, the
-library browsable trough the \WHELP{} technology is always kept up to date.
+Cleaning guarantees that if an object is removed there are no dandling
+references to it, and that the part of the library still compiled is
+consistent. Since cleaning involves the removal of all the results of
+the compilation, metadata included, the library browsable trough the
+\WHELP{} technology is always kept up to date.
-\subsubsection{Interactive and batch (de)compilation}
+\subsubsection{Batch vs Interactive}
\MATITA{} includes an interactive graphical interface and a batch
compiler (\MATITAC). Only the former is intended to be used directly by the
part of the user development is required (for example issuing an
\texttt{include} command) but not yet compiled.
-While they share the same engine for compilation and decompilation,
-they provide different granularity. The batch compiler is only able to
-compile a whole script file and reciprocally to decompile only a whole
-script, and consequently all the other scripts that rely on an object
-defined in it. The interactive interface is able to execute single steps
-of compilation, that may include the definition of an object, and
-consequently to undo single steps, thus removing single objects.
+While they share the same engine for compilation and cleaning, they
+provide different granularity. The batch compiler is only able to
+compile a whole script and similarly to clean only a whole script
+(together with all the other scripts that rely on an object defined in
+it). The interactive interface is able to execute single steps of
+compilation, that may include the definition of an object, and
+similarly to undo single steps. Note that in the latter case there is
+no risk of introducing dangling references since the \MATITA{} user
+interface inhibit undoing a step which is not the last executed.
\subsection{Automation}
projects / helm.git / commitdiff