\newcommand{\LOCATE}{\textsc{Locate}}
\newcommand{\MATCH}{\textsc{Match}}
\newcommand{\MATITA}{Matita}
+\newcommand{\MATITAC}{\texttt{matitac}}
+\newcommand{\MATITADEP}{\texttt{matitadep}}
\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
\newcommand{\MOWGLI}{MoWGLI}
\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
\subsection{Compilation and decompilation}
\label{sec:libmanagement}
-The aim of this section is to describe the way matita
+%
+%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).\\
+
+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.
+using the \WHELP{} technology, in response to the user addition or
+removal 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
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 \GETTER component
-should be updated with the the new mapping between the logical URI
-and the physical path of objects.
+\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
-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
+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
+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
+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 defined objects available in the library,
+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 find the right order 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 developed a low level tool called \emph{matitadep}
+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 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
+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{aliases}).
+\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.
+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
+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
there will be no theorems in the development that depends on the
-removed item.
+removed items.
\subsubsection{Decompilation}
-Decompiling an object involves,
-recursively, the decompilation of all the objects that depend on it.
+
+Decompiling an object involves the (recursive)
+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
+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.
+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
-deletion of all the outputs of the compilation, metadata included, the
-library browsable trough the \WHELP{} technology is always up to date.
+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}
+
\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.
+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 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
+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
-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).\\
+consequently to undo single steps, thus removing single objects.
\subsection{Automation}
expressiveness.
\subsubsection{Disambiguation aliases}
-\label{aliases}
+\label{sec:disambaliases}
Let's start with the definition of the ``strictly greater then'' notion over
(Peano) natural numbers.
\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
While one would expect to find structured constructs like
$\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
-This is essential for base idea behind matita tacticals: step-by-step execution.
+This is essential for base idea behind \MATITA{} tacticals: step-by-step
+execution.
The low-level tacticals implementation of \MATITA{} allows a step-by-step
execution of a tactical, that substantially means that a $\NT{block\_kind}$ is
projects / helm.git / commitdiff