From: Enrico Tassi Date: Sun, 22 Jan 2006 13:43:15 +0000 (+0000) Subject: draft of compilation/decompilatio X-Git-Tag: make_still_working~7792 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cfa2988321970b9db1d0d3722a4764253d374aed;p=helm.git draft of compilation/decompilatio --- diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index f2e411d4a..49c531590 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -275,6 +275,7 @@ allow other developers to quickly understand our code and contribute. \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. @@ -346,6 +347,7 @@ fully specified terms; partially specified terms; 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 @@ -691,7 +693,140 @@ content selection and copy-paste. \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} @@ -785,7 +920,7 @@ some of its parameters, helps in keeping the input terse without sacrificing expressiveness. \subsubsection{Disambiguation aliases} - +\label{aliases} Let's start with the definition of the ``strictly greater then'' notion over (Peano) natural numbers.