\end{figure}
\section{Architecture}
+\label{architettura}
Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
(circle nodes) and \emph{applications} (squared nodes) developed in the HELM
project.
content level terms; presentation level terms.
\subsection{Fully specified terms}
+\label{fully-spec}
\emph{Fully specified terms} are CIC terms where no information is
missing or left implicit. A fully specified term should be well-typed.
The mathematical notions (axioms, definitions, theorems) that are stored
\subsection{Indexing and searching}
-\subsection{Developments}
+
+\subsection{Compilation and decompilation}
+\label{compilazione}
+
+The aim of this section is to describe the way matita
+preserves the consistency and the availability of the library
+trough the \WHELP{} technology, in response to the user addition or
+deletion of mathematical objects.
+
+As already sketched in \ref{fully-spec} the output of the
+compilation of a script is split among two storage media, a
+classical filesystem and a relational database. The former is used to
+store the XML encoding of the objects defined in the script, the
+disambiguation aliases and the interpretation and notational convention defined,
+while the latter is used to store all the metadata needed by
+\WHELP{}. In addition the \emph{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
+the content of the library and is thus of poor interest (but really
+tedious to implement and keep bug-free), there is a more deep
+notion of mathematical consistency we need to provide. Each object
+must reference only defined object (i.e. each proof must use only
+already proved theorems).
+
+We will focus on how matita ensures the interesting kind
+of consistency during the formalization of a mathematical theory,
+giving the user the freedom of adding, deleting, modifying objects
+without loosing the feeling of an always visible and browsable
+library.
+
+\subsubsection{Compilation}
+The typechecker component guarantees that if an object is well typed
+it depends only on well defined objects available in the library,
+that is exactly what we need to be sure that the logic consistency of
+the library is preserved. We have only find the right order of
+compilation of the scripts that compose the user development.
+
+For this purpose we developed a low level tool called \emph{matitadep}
+that takes in input the list of files that compose the development and
+outputs their dependencies in a format suitable for the make utility.
+The user is not asked to run \emph{matitadep} nor make by hand, but
+simply to tell matita the root directory of his development (where all
+script files can be found) and matita will handle all the compilation
+tasks.\\
+To calculate dependencies it is enough to look at the script file for
+its inclusions of other parts of the development or for explicit
+references to other objects (i.e. with explicit aliases, see
+\ref{aliases}).
+
+The output of the compilation is immediately available to the user
+trough the \WHELP{} technology, since all metadata are stored in a
+user-specific area of the database where the search engine has read
+access, and all the automated tactics that operates on the whole
+library, like auto, have full visibility of the newly defined objects.
+
+Compilation is rather simple, and the only tricky case is when we want
+to compile again the same script, maybe after the deletion of a
+theorem. Here the policy is simple: decompile it before recompiling.
+As we will see in the next section decompilation will ensure that
+there will be no theorems in the development that depends on the
+removed item.
+
+\subsubsection{Decompilation}
+Decompiling an object involves,
+recursively, the decompilation of all the objects that depend on it.
+
+The calculation of the reverse dependencies can be computed in two
+ways, using the relational database or using a simpler set of metadata
+that matita saves in the filesystem as a result of compilation. The
+former technique is the same used by the \emph{Dependency Analyzer}
+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. Due to
+the complex deployment of a complex peace of software like a database,
+it is a common usage for the \HELM{} team to use a single and remote
+database, that may result unavailable if the user workstation lacks
+connectivity. This facility has to be intended only as a fall-back,
+since the whole \WHELP{} technology depends on the 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
+deletion of all the outputs of the compilation, metadata included, the
+library browsable trough the \WHELP{} technology is always up to date.
+
+\subsubsection{Interactive and batch (de)compilation}
+Matita includes an interactive graphical interface and a batch
+compiler. Only the former is intended to be used directly by the
+user, the latter is automatically invoked when a not yet compiled
+part of the user development is required.
+
+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 it can 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
+symmetrically to undo single steps, thus removing single objects.
+
+%
+%goals: consentire sviluppo di una librearia mantenendo integrita' referenziale e usando le teconologie nostre (quindi con metadati, XML, libreria visibile)
+%\subsubsection{Composition}
+%scripts.ma, .moo, XML, metadata
+%\subsubsection{Compilation}
+%analogie con compilazione classica dso.\\
+%granularita' differenti per uso interattivo e non
+%\paragraph{Batch}
+%- granularita' .ma/buri \\
+%-- motivazioni\\
+%- come si calcolano le dipendenze\\
+%- quando la si usa\\
+%- metodi (cc e clean)\\
+%- garanzie
+%\paragraph{Interactive}
+%- granularita' fine\\
+%-- 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).\\
+%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\\
+%--- granularita' baseuri (compilation unit) per la libreria\\
+%In entrmbi i casi ora:\\
+%--- matitaSync: add, remove, timetravel(facility-macro tra 2 stati)[obj]\\
+%--- matitaCleanLib: clean\_baseuri (che poi usa matitaSync a sua volta)[comp1]\\
+%Vincoli di add: typecheck ( ==$>$ tutto quello che usa sta in lib)\\
+%Vincoli di remove: \\
+%--- la remove di mSync non li controlla (ma sa cosa cancellare per ogni uri)\\
+%--- la clean\_baseuri calcola le dipendenze con i metadati (o anche i moo direi) e li rispetta\\
+%Undo di matita garantisce la consistenza a patto che l'history che tiene sia ok\\
+%Undo della lib (mClean) garantisce la consistenza (usando moo o Db).\\
\subsection{Automation}
expressiveness.
\subsubsection{Disambiguation aliases}
-
+\label{aliases}
Let's start with the definition of the ``strictly greater then'' notion over
(Peano) natural numbers.
projects / helm.git / commitdiff