+
+
+\subsection{Generation and Invalidation}
+\label{sec:libmanagement}
+
+The aim of this section is to describe the way \MATITA{}
+preserves the consistency and the availability of the library
+using the \WHELP{} technology, in response to the user alteration or
+removal of mathematical objects.
+
+As already sketched in Sec.~\ref{sec:fullyspec} what we generate
+from 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{}.
+
+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
+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, removing, 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 typed 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 to find the right order of
+compilation of the scripts that compose the user development.
+
+For this purpose we provide a tool called \MATITADEP{}
+that takes in input the list of files that compose the development and
+outputs their dependencies in a format suitable for the GNU \texttt{make} tool.
+The user is not asked to run \MATITADEP{} 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
+related tasks, including dependencies calculation.
+To compute dependencies it is enough to look at the script files for
+inclusions of other parts of the development or for explicit
+references to other objects (i.e. with explicit aliases, see
+\ref{sec:disambaliases}).
+
+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 removal of a
+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{Cleaning}
+
+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
+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.\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.
+
+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{Batch vs Interactive}
+
+\MATITA{} includes an interactive authoring interface and a batch
+``compiler'' (\MATITAC). Only the former is intended to be used directly by the
+user, the latter is automatically invoked when a
+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 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}
+\label{sec:automation}
+
+\subsection{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 authoring interface}
+\label{sec:authoring}
+
+The authoring interface of \MATITA{} is very similar to Proof General. We
+chose not to build the \MATITA{} UI over Proof General for two reasons. First
+of all we wanted to integrate our XML-based rendering technologies, mainly
+\GTKMATHVIEW{}. At the time of writing Proof General supports only text based
+rendering.\footnote{This may change with the future release of Proof General
+based on Eclipse, but is not yet the case.} The second reason is that we wanted
+to build the \MATITA{} UI on top of a state-of-the-art and widespread toolkit
+as GTK is.
+
+Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface,
+featuring two windows. The background one is very like to the Proof General
+interface. The main difference is that we use the \GTKMATHVIEW{} widget to
+render sequents. Since \GTKMATHVIEW{} renders \MATHML{} markup we take
+advantage of the whole bidimensional mathematical notation.
+
+The foreground window, also implemented around \GTKMATHVIEW, is called
+``cicBrowser''. It is used to browse the library, including the proof being
+developed, and enable content based search over it. Proofs are rendered in
+natural language, automatically generated from the low-level lambda-terms,
+using techniques inspired by \cite{natural,YANNTHESIS} and already described
+in~\cite{remathematization}.
+
+Note that the syntax used in the script view is \TeX-like, however unicode is
+fully supported so that mathematical glyphs can be input as such.
+
+\begin{figure}[!ht]
+ \begin{center}
+ \includegraphics[width=0.95\textwidth]{matita-screenshot}
+ \caption{\MATITA{} look and feel}
+ \label{fig:screenshot}
+ \end{center}
+\end{figure}
+
+Since the concepts of script based proof authoring are well-known, the
+remaining part of this section is dedicated to the distinguishing
+features of the \MATITA{} authoring interface.
+
+\subsection{Direct manipulation of terms}
+
+While terms are input as \TeX-like formulae in \MATITA, they are converted to a
+mixed \MATHML+\BOXML{} markup for output purposes and then rendered by
+\GTKMATHVIEW. As described in~\cite{latexmathml} this mixed choice enables both
+high-quality bidimensional rendering of terms (including the use of fancy
+layout schemata like radicals and matrices) and the use of a
+concise and widespread textual syntax.
+
+Keeping pointers from the presentations level terms down to the
+partially specified ones \MATITA{} enable direct manipulation of
+rendered (sub)terms in the form of hyperlinks and semantic selection.
+
+\emph{Hyperlinks} have anchors on the occurrences of constant and
+inductive type constructors and point to the corresponding definitions
+in the library. Anchors are available notwithstanding the use of
+user-defined mathematical notation: as can be seen on the right of
+Fig.~\ref{fig:directmanip}, where we clicked on $\not|$, symbols
+encoding complex notations retain all the hyperlinks of constants or
+constructors used in the notation.
+
+\emph{Semantic selection} enables the selection of mixed
+\MATHML+\BOXML{} markup, constraining the selection to markup
+representing meaningful CIC (sub)terms. In the example on the left of
+Fig.~\ref{fig:directmanip} is thus possible to select the subterm
+$\mathrm{prime}~n$, whereas it would not be possible to select
+$\to n$ since the former denotes an application while the
+latter it not a subterm. Once a meaningful (sub)term has been
+selected actions can be done on it like reductions or tactic
+applications.