-
-\subsection{Compilation and decompilation}
-\label{sec:libmanagement}
-
-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}
-
-\subsection{\MATITA's naming convention}
-A minor but not entirely negligible aspect of \MATITA{} is that of
-adopting a (semi)-rigid naming convention for identifiers, derived by
-our studies about metadata for statements.
-The convention is only applied to identifiers for theorems
-(not definitions), and relates the name of a proof to its statement.
-The basic rules are the following:
-\begin{itemize}
-\item each identifier is composed by an ordered list of (short)
-names occurring in a left to right traversal of the statement;
-\item all identifiers should (but this is not strictly compulsory)
-separated by an underscore,
-\item identifiers in two different hypothesis, or in an hypothesis
-and in the conlcusion must be separated by the string ``\verb+_to_+'';
-\item the identifier may be followed by a numerical suffix, or a
-single or duoble apostrophe.
-
-\end{itemize}
-Take for instance the theorem
-\[\forall n:nat. n = plus \; n\; O\]
-Possible legal names are: \verb+plus_n_O+, \verb+plus_O+,
-\verb+eq_n_plus_n_O+ and so on.
-Similarly, consider the theorem
-\[\forall n,m:nat. n<m \to n \leq m\]
-In this case \verb+lt_to_le+ is a legal name,
-while \verb+lt_le+ is not.\\
-But what about, say, the symmetric law of equality? Probably you would like
-to name such a theorem with something explicitly recalling symmetry.
-The correct approach,
-in this case, is the following. You should start with defining the
-symmetric property for relations
-
-\[definition\;symmetric\;= \lambda A:Type.\lambda R.\forall x,y:A.R x y \to R y x \]
-
-Then, you may state the symmetry of equality as
-\[ \forall A:Type. symmetric \;A\;(eq \; A)\]
-and \verb+symmetric_eq+ is valid \MATITA{} name for such a theorem.
-So, somehow unexpectedly, the introduction of semi-rigid naming convention
-has an important benefical effect on the global organization of the library,
-forcing the user to define abstract notions and properties before
-using them (and formalizing such use).
-
-Two cases have a special treatment. The first one concerns theorems whose
-conclusion is a (universally quantified) predicate variable, i.e.
-theorems of the shape
-$\forall P,\dots.P(t)$.
-In this case you may replace the conclusion with the word
-``elim'' or ``case''.
-For instance the name \verb+nat_elim2+ is a legal name for the double
-induction principle.
-
-The other special case is that of statements whose conclusion is a
-match expression.
-A typical example is the following
-\begin{verbatim}
- \forall n,m:nat.
- match (eqb n m) with
- [ true \Rightarrow n = m
- | false \Rightarrow n \neq m]
-\end{verbatim}
-where $eqb$ is boolean equality.
-In this cases, the name can be build starting from the matched
-expression and the suffix \verb+_to_Prop+. In the above example,
-\verb+eqb_to_Prop+ is accepted.
-
-\section{The \MATITA{} user interface}
-
-
-