From 9f66deafc611d91e5bd68d33aa4d603a99d40de9 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 23 Jan 2006 14:44:46 +0000 Subject: [PATCH] section re-ordering --- helm/papers/matita/matita2.tex | 132 ++++++++++++++++----------------- 1 file changed, 66 insertions(+), 66 deletions(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index f970c8c29..76fe5c6ce 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -205,15 +205,6 @@ add an authoring interface, and a set of functionalities for the overall management of the library, integrating everything into a single system. \MATITA{} is the result of this effort. -\subsection{The System} -DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE'' - -\begin{itemize} - \item scelta del sistema fondazionale - \item sistema indipendente (da \COQ) - \item compatibilit\`a con sistemi legacy -\end{itemize} - \subsection{Relationship with \COQ{}} At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is @@ -270,7 +261,70 @@ allow other developers to quickly understand our code and contribute. %be able to contribute to \COQ{}'s code is quite steep and requires direct %and frequent interactions with \COQ{} developers. +\subsection{The system} + +DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''\\ +ROBA CHE MANCA: +\begin{itemize} + \item scelta del sistema fondazionale + \item sistema indipendente (da \COQ) + \item compatibilit\`a con sistemi legacy +\end{itemize} + \begin{figure}[t] + \begin{center} +% \includegraphics[width=0.9\textwidth]{a.eps} + \caption{\MATITA{} screenshot} + \label{fig:screenshot} + \end{center} +\end{figure} + +\MATITA{} has a script based user interface. As can be seen in Fig.~... it is +split in two main windows: on the left a textual widget is used to edit the +script, on the right the list of open goal is shown using a MathML rendering +widget. A distinguished part of the script (shaded in the screenshot) represent +the commands already executed and can't be edited without undoing them. The +remaining part can be freely edited and commands from that part can be executed +moving down the execution point. An additional window --- the ``cicBrowser'' --- +can be used to browse the library, including the proof being developed, and +enable content based search on it. In the cicBrowser proofs are rendered in +natural language, automatically generated from the low-level $\lambda$-terms +using techniques inspired by \cite{natural,YANNTHESIS}. + +In the \MATITA{} philosophy the script is not relevant \emph{per se}, but is +only seen as a convenient way to create mathematical objects. The universe of +all these objects makes up the \HELM{} library, which is always completely +visible to the user. The mathematical library is thus conceived as a global +hypertext, where objects may freely reference each other. It is a duty of +the system to guide the user through the relevant parts of the library. + +This methodological assumption has many important consequences +which will be discussed in the next section. + +%on one side +%it requires functionalities for the overall management of the library, +%%%%%comprising efficient indexing techniques to retrieve and filter the +%information; +%on the other it introduces overloading in the use of +%identifiers and mathematical notation, requiring sophisticated disambiguation +%techniques for interpreting the user inputs. +%In the next two sections we shall separately discuss the two previous +%points. + +%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is +%organized in components which work on data in this format. For instance the +%rendering engine, which transform $\lambda$-terms encoded as XML document to +%MathML Presentation documents, can be used apart from \MATITA{} to print ... +%FINIRE + +A final section is devoted to some innovative aspects +of the authoring system, such as a step by step tactical execution, +content selection and copy-paste. + +\section{Architecture} +\label{architettura} + +\begin{figure}[ht] \begin{center} \includegraphics[width=0.9\textwidth]{librariesCluster.ps} \caption{\MATITA{} libraries} @@ -278,8 +332,6 @@ allow other developers to quickly understand our code and contribute. \end{center} \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. @@ -662,58 +714,6 @@ services missing from the standard library of the programming language. %In particular, the \texttt{xml} \component{} is used to easily represent, %parse and pretty-print XML files. -\section{Using \MATITA (boh \ldots cambiare titolo)} - -\begin{figure}[t] - \begin{center} -% \includegraphics[width=0.9\textwidth]{a.eps} - \caption{\MATITA{} screenshot} - \label{fig:screenshot} - \end{center} -\end{figure} - -\MATITA{} has a script based user interface. As can be seen in Fig.~... it is -split in two main windows: on the left a textual widget is used to edit the -script, on the right the list of open goal is shown using a MathML rendering -widget. A distinguished part of the script (shaded in the screenshot) represent -the commands already executed and can't be edited without undoing them. The -remaining part can be freely edited and commands from that part can be executed -moving down the execution point. An additional window --- the ``cicBrowser'' --- -can be used to browse the library, including the proof being developed, and -enable content based search on it. In the cicBrowser proofs are rendered in -natural language, automatically generated from the low-level $\lambda$-terms -using techniques inspired by \cite{natural,YANNTHESIS}. - -In the \MATITA{} philosophy the script is not relevant \emph{per se}, but is -only seen as a convenient way to create mathematical objects. The universe of -all these objects makes up the \HELM{} library, which is always completely -visible to the user. The mathematical library is thus conceived as a global -hypertext, where objects may freely reference each other. It is a duty of -the system to guide the user through the relevant parts of the library. - -This methodological assumption has many important consequences -which will be discussed in the next section. - -%on one side -%it requires functionalities for the overall management of the library, -%%%%%comprising efficient indexing techniques to retrieve and filter the -%information; -%on the other it introduces overloading in the use of -%identifiers and mathematical notation, requiring sophisticated disambiguation -%techniques for interpreting the user inputs. -%In the next two sections we shall separately discuss the two previous -%points. - -%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is -%organized in components which work on data in this format. For instance the -%rendering engine, which transform $\lambda$-terms encoded as XML document to -%MathML Presentation documents, can be used apart from \MATITA{} to print ... -%FINIRE - -A final section is devoted to some innovative aspects -of the authoring system, such as a step by step tactical execution, -content selection and copy-paste. - \section{Library Management} \subsection{Indexing and searching} @@ -866,7 +866,7 @@ interface inhibit undoing a step which is not the last executed. \subsection{Automation} -\subsection{\MATITA's naming convention} +\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. @@ -931,7 +931,7 @@ 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} +\section{User interface} \subsection{Disambiguation} \label{sec:disambiguation} @@ -1566,7 +1566,7 @@ even being a so simple idea: goal) gives you the feeling of what is going on. \end{description} -\section{The \MATITA{} library} +\section{Standard library} \MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{} can be read, checked and referenced in further developments. -- 2.39.2