Removing the documentation of the XML plugin.

5 files changed, 2 insertions, 319 deletions

diff --git a/CHANGES b/CHANGES
index 5d014399a..839885376 100644
--- a/CHANGES
+++ b/CHANGES
@@ -228,6 +228,7 @@ Tools
   the files without playing the proof scripts, asynchronously checking
   that the quickly generated proofs are correct and generating the object
   files from the quickly generated proofs.
+- The XML plugin was discontinued and removed from the source.
 
 Interfaces
 
diff --git a/Makefile.common b/Makefile.common
index 812fbeeaf..6dc193d6e 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -127,7 +127,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \
   Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
   Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
-  Setoid.v.tex Helm.tex Classes.v.tex AsyncProofs.v.tex Universes.v.tex \
+  Setoid.v.tex Classes.v.tex AsyncProofs.v.tex Universes.v.tex \
   Misc.v.tex)
 
 REFMANTEXFILES:=$(addprefix doc/refman/, \
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index fba210c69..1c28063e6 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -295,7 +295,6 @@ There are graphical user interfaces:
 There are documentation and browsing tools:
 
 \begin{description}
-\item[Helm/Mowgli] A rendering, searching and publishing tool.
 \item[coq-tex] A tool to insert {\Coq} examples within .tex files. 
 \item[coqdoc] A documentation tool for \Coq.
 \item[coqgraph] A tool to generate a dependency graph from {\Coq} sources.
diff --git a/doc/refman/Helm.tex b/doc/refman/Helm.tex
deleted file mode 100644
index cbb097267..000000000
--- a/doc/refman/Helm.tex
+++ /dev/null
@@ -1,313 +0,0 @@
-\label{Helm}
-\index{XML exportation}
-\index{Proof rendering}
-
-This section describes the exportation of {\Coq} theories to XML that
-has been contributed by Claudio Sacerdoti Coen.  Currently, the main
-applications are the rendering and searching tool
-developed within the HELM\footnote{Hypertextual Electronic Library of
-Mathematics} and MoWGLI\footnote{Mathematics on the Web, Get it by
-Logic and Interfaces} projects mainly at the University of Bologna and
-partly at INRIA-Sophia Antipolis.
-
-\subsection{Practical use of the XML exportation tool}
-
-The basic way to export the logical content of a file into XML format
-is to use {\tt coqc} with option {\tt -xml}. 
-When the {\tt -xml} flag is set, every definition or declaration is
-immediately exported to XML once concluded.
-The system environment variable {\tt COQ\_XML\_LIBRARY\_ROOT} must be
-previously set to a directory in which the logical structure of the
-exported objects is reflected.
-
-  For {\tt Makefile} files generated by \verb+coq_makefile+ (see section
-  \ref{Makefile}), it is sufficient to compile the files using
- \begin{quotation}
-   \verb+make COQ_XML=-xml+
- \end{quotation}
- 
- To export a development to XML, the suggested procedure is then:
- 
- \begin{enumerate}
-  \item add to your own contribution a valid \verb+Make+ file and use
-      \verb+coq_makefile+ to generate the \verb+Makefile+ from the \verb+Make+
-      file.
- 
-      \Warning Since logical names are used to structure the XML
-      hierarchy, always add to the \verb+Make+ file at least one \verb+"-R"+
-      option to map physical file names to logical module paths.
-  \item set the \verb+COQ_XML_LIBRARY_ROOT+ environment variable to
-  the directory where the XML file hierarchy must be physically
-  rooted.
-  \item compile your contribution with \verb+"make COQ_XML=-xml"+
- \end{enumerate}
- 
-\Rem In case the system variable {\tt COQ\_XML\_LIBRARY\_ROOT} is not set,
-the output is done on the standard output. Also, the files are
-compressed using {\tt gzip} after creation. This is to save disk space
-since the XML format is very verbose.
-
-\subsection{Reflection of the logical structure into the file system}
-
-For each {\Coq} logical object, several independent files associated
-to this object are created.  The structure of the long name of the
-object is reflected in the directory structure of the file system.
-E.g. an object of long name 
-{\ident$_1$}{\tt .}{\ldots}{\tt .}{\ident$_n$}{\tt .}{\ident} is exported to files in the
-subdirectory {\ident$_1$}{\tt /}{\ldots}{\tt /}{\ident$_n$} of the directory 
-bound to the environment variable {\tt COQ\_XML\_LIBRARY\_ROOT}.
-
-\subsection{What is exported?}
-
-The XML exportation tool exports the logical content of {\Coq}
-theories. This covers global definitions (including lemmas, theorems,
-...), global assumptions (parameters and axioms), local assumptions or
-definitions, and inductive definitions.
-
-Vernacular files are exported to {\tt .theory.xml} files. 
-%Variables,
-%definitions, theorems, axioms and proofs are exported to individual
-%files whose suffixes range from {\tt .var.xml}, {\tt .con.xml}, {\tt
-%.con.body.xml}, {\tt .con.types.xml} to {\tt .con.proof_tree.xml}.
-Comments are pre-processed with {\sf coqdoc} (see section
-\ref{coqdoc}). Especially, they have to be enclosed within {\tt (**}
-and {\tt *)} to be exported.
-
-For each inductive definition of name
-{\ident$_1$}{\tt .}{\ldots}{\tt .}{\ident$_n$}.{\ident}, a file named
-{\ident}{\tt .ind.xml} is created in the subdirectory
-{\ident$_1$}{\tt /}{\ldots}{\tt /}{\ident$_n$} of the xml library root
-directory. It contains the arities and constructors of the type. For mutual inductive definitions, the file is named after the
-name of the first inductive type of the block.
-
-For each global definition of base name
-{\ident$_1$}{\tt .}{\ldots}{\tt .}{\ident$_n$}.{\ident}, files named
-{\tt {\ident}.con.body.xml} and {\tt {\ident}.con.xml} are created in the
-subdirectory {\ident$_1$}{\tt /}{\ldots}{\tt /}{\ident$_n$}. They
-respectively contain the body and the type of the definition.
-
-For each global assumption of base name {\ident$_1$}{\tt .}{\ident$_2$}{\tt .}
-{\ldots}{\tt .}{\ident$_n$}{\tt .}{\ident}, a file
-named {\ident}{\tt .con.xml} is created in the subdirectory
-{\ident$_1$}{\tt /}{\ldots}{\tt /}{\ident$_n$}.  It contains the type of the
-global assumption.
-
-For each local assumption or definition of base name {\ident} located
-in sections {\ident$'_1$}, {\ldots}, {\ident$'_p$} of the module
-{\ident$_1$}.{\ident$_2$}{\tt .}{\ldots}{\tt .}{\ident$_n$}.{\ident}, a file
-named {\tt {\ident}.var.xml} is created in the subdirectory
-{\ident$_1$}{\tt /}{\ldots}{\tt /}{\ident$_n$}{\tt /}{\ident$'_1$}{\tt /}\ldots{\tt /}{\ident$'_p$}.
-It contains its type and, if a definition, its body.
-
-In order to do proof-rendering (for example in natural language), some
-redundant typing information is required, i.e. the type of at least
-some of the subterms of the bodies and types of the CIC objects. These
-types are called inner types and are exported to files of suffix {\tt
-.types.xml} by the exportation tool.
-
-
-% Deactivated
-%% \subsection{Proof trees}
-
-%% For each definition or theorem that has been built with tactics, an
-%% extra file of suffix {\tt proof\_tree.xml} is created. It contains the
-%% proof scripts and is used for rendering the proof.
-
-\subsection[Inner types]{Inner types\label{inner-types}}
-
-The type of a subterm of a construction is called an {\em inner type}
-if it respects the following conditions.
- 
-\begin{enumerate}
-  \item Its sort is \verb+Prop+\footnote{or {\tt CProp} which is the
-    "sort"-like definition used in C-CoRN (see
-    \url{http://vacuumcleaner.cs.kun.nl/c-corn}) to type
-    computationally relevant predicative propositions.}.
- \item It is not a type cast nor an atomic term (variable, constructor or constant).
- \item If it's root is an abstraction, then the root's parent node is
-    not an abstraction, i.e. only the type of the outer abstraction of
-    a block of nested abstractions is printed.
-\end{enumerate}
-                                                                               
-The rationale for the 3$^{rd}$ condition is that the type of the inner
-abstractions could be easily computed starting from the type of the
-outer ones; moreover, the types of the inner abstractions requires a
-lot of disk/memory space: removing the 3$^{rd}$ condition leads to XML
-file that are two times as big as the ones exported applying the 3$^{rd}$
-condition.
-
-\subsection{Interactive exportation commands}
-
-There are also commands to be used interactively in {\tt coqtop}.
-
-\subsubsection[\tt Print XML {\qualid}]{\tt Print XML {\qualid}\comindex{Print XML}}
-
-If the variable {\tt COQ\_XML\_LIBRARY\_ROOT} is set, this command creates
-files containing the logical content in XML format of {\qualid}. If
-the variable is not set, the result is displayed on the standard
-output.
-
-\begin{Variants}
-\item {\tt Print XML File {\str} {\qualid}}\\
-This writes the logical content of {\qualid} in XML format to files
-whose prefix is {\str}.
-\end{Variants}
-
-\subsubsection[{\tt Show XML Proof}]{{\tt Show XML Proof}\comindex{Show XML Proof}}
-
-If the variable {\tt COQ\_XML\_LIBRARY\_ROOT} is set, this command creates
-files containing the current proof in progress in XML format. It
-writes also an XML file made of inner types.  If the variable is not
-set, the result is displayed on the standard output.
-
-\begin{Variants}
-\item {\tt Show XML File {\str} Proof}\\ This writes the
-logical content of {\qualid} in XML format to files whose prefix is
-{\str}. 
-\end{Variants}
-
-\subsection{Applications: rendering, searching and publishing}
-
-The HELM team at the University of Bologna has developed tools
-exploiting the XML exportation of {\Coq} libraries. This covers
-rendering, searching and publishing tools.
-
-All these tools require a running http server and, if possible, a
-MathML compliant browser.  The procedure to install the suite of tools
-ultimately allowing rendering and searching can be found on the HELM
-web site \url{http://helm.cs.unibo.it/library.html}.
-
-It may be easier though to upload your developments on the HELM http
-server and to re-use the infrastructure running on it. This requires
-publishing your development. To this aim, follow the instructions on
-\url{http://mowgli.cs.unibo.it}.
-
-Notice that the HELM server already hosts a copy of the standard
-library of {\Coq} and of the {\Coq} user contributions.
-
-\subsection{Technical informations}
-
-\subsubsection{CIC with Explicit Named Substitutions}
-                                                                               
-The exported files are XML encoding of the lambda-terms used by the
-\Coq\ system. The implementative details of the \Coq\ system are hidden as much
-as possible, so that the XML DTD is a straightforward encoding of the
-Calculus of (Co)Inductive Constructions.
-                                                                                
-Nevertheless, there is a feature of the \Coq\ system that can not be
-hidden in a completely satisfactory way: discharging (see Sect.\ref{Section}).
-In \Coq\ it is possible
-to open a section, declare variables and use them in the rest of the section
-as if they were axiom declarations. Once the section is closed, every definition and theorem in the section is discharged by abstracting it over the section
-variables. Variable declarations as well as section declarations are entirely
-dropped. Since we are interested in an XML encoding of definitions and
-theorems as close as possible to those directly provided the user, we
-do not want to export discharged forms. Exporting non-discharged theorem
-and definitions together with theorems that rely on the discharged forms
-obliges the tools that work on the XML encoding to implement discharging to
-achieve logical consistency. Moreover, the rendering of the files can be
-misleading, since hyperlinks can be shown between occurrences of the discharge
-form of a definition and the non-discharged definition, that are different
-objects.
-                                                                                
-To overcome the previous limitations, Claudio Sacerdoti Coen developed in his
-PhD. thesis an extension of CIC, called Calculus of (Co)Inductive Constructions
-with Explicit Named Substitutions, that is a slight extension of CIC where
-discharging is not necessary. The DTD of the exported XML files describes
-constants, inductive types and variables of the Calculus of (Co)Inductive
-Constructions with Explicit Named Substitutions. The conversion to the new
-calculus is performed during the exportation phase.
-
-The following example shows a very small \Coq\ development together with its
-version in CIC with Explicit Named Substitutions.
-
-\begin{verbatim}
-# CIC version: #
-Section S.
- Variable A : Prop.
-
- Definition impl := A -> A.
-
- Theorem t : impl.           (* uses the undischarged form of impl *)
-  Proof.
-   exact (fun (a:A) => a).
-  Qed.
-
-End S.
-
-Theorem t' : (impl False).   (* uses the discharged form of impl *)
- Proof.
-  exact (t False).           (* uses the discharged form of t *)
- Qed.
-\end{verbatim}
- 
-\begin{verbatim}
-# Corresponding CIC with Explicit Named Substitutions version: #
-Section S.
- Variable A : Prop.
- 
- Definition impl(A) := A -> A. (* theorems and definitions are
-                                  explicitly abstracted over the
-                                  variables. The name is sufficient to
-                                  completely describe the abstraction *)
- 
- Theorem t(A) : impl.          (* impl where A is not instantiated *)
-  Proof.
-   exact (fun (a:A) => a).
-  Qed.
- 
-End S.
- 
-Theorem t'() : impl{False/A}. (* impl where A is instantiated with False
-                                 Notice that t' does not depend on A     *)
- Proof.
-  exact t{False/A}.           (* t where A is instantiated with False *)
- Qed.
-\end{verbatim}
- 
-Further details on the typing and reduction rules of the calculus can be
-found in Claudio Sacerdoti Coen PhD. dissertation, where the consistency
-of the calculus is also proved.
- 
-\subsubsection{The CIC with Explicit Named Substitutions XML DTD}
- 
-A copy of the DTD can be found in the file ``\verb+cic.dtd+'' in the
-\verb+plugins/xml+ source directory of \Coq.
-The following is a very brief overview of the elements described in the DTD.
- 
-\begin{description}
- \item[]\texttt{<ConstantType>}
-   is the root element of the files that correspond to constant types.
- \item[]\texttt{<ConstantBody>}
-   is the root element of the files that correspond to constant bodies.
-   It is used only for closed definitions and theorems (i.e. when no
-   metavariable occurs in the body or type of the constant)
- \item[]\texttt{<CurrentProof>}
-   is the root element of the file that correspond to the body of a constant
-   that depends on metavariables (e.g. unfinished proofs)
- \item[]\texttt{<Variable>}
-   is the root element of the files that correspond to variables
- \item[]\texttt{<InductiveTypes>}
-   is the root element of the files that correspond to blocks
-   of mutually defined inductive definitions
-\end{description}
- 
-The elements
- \verb+<LAMBDA>+, \verb+<CAST>+, \verb+<PROD>+, \verb+<REL>+, \verb+<SORT>+,
- \verb+<APPLY>+, \verb+<VAR>+, \verb+<META>+, \verb+<IMPLICIT>+, \verb+<CONST>+, \verb+<LETIN>+, \verb+<MUTIND>+, \verb+<MUTCONSTRUCT>+, \verb+<MUTCASE>+,
- \verb+<FIX>+ and \verb+<COFIX>+ are used to encode the constructors of CIC.
- The \verb+sort+ or \verb+type+ attribute of the element, if present, is
- respectively the sort or the type of the term, that is a sort because of the
- typing rules of CIC.
- 
-The element \verb+<instantiate>+ correspond to the application of an explicit
-named substitution to its first argument, that is a reference to a definition
-or declaration in the environment.
- 
-All the other elements are just syntactic sugar.
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 2b852d5f4..85ed03430 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -150,10 +150,6 @@ automatically regenerated when \texttt{\_CoqProject} is updated afterward.
 
 \input{./coqdoc}
 
-\section{Exporting \Coq\ theories to XML}
-
-\input{./Helm}
-
 \section[Embedded \Coq\ phrases inside \LaTeX\ documents]{Embedded \Coq\ phrases inside \LaTeX\ documents\label{Latex}
   \index{Coqtex@{\tt coq-tex}}\index{Latex@{\LaTeX}}}