Revu removeproof

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

Makefile

@@ -74,7 +74,7 @@ all:
 	$(MAKE) -C extraction
 	$(MAKE) -C runtime
 
-documentation:
+documentation: doc/removeproofs
 	@ln -f $(FILES) doc/
 	@mkdir -p doc/html
 	cd doc; $(COQDOC) --html -d html \
@@ -83,6 +83,12 @@ documentation:
 	cp doc/coqdoc.css doc/html/coqdoc.css
 	doc/removeproofs doc/html/*.html
 
+doc/removeproofs: doc/removeproofs.ml
+	ocamlopt -o doc/removeproofs doc/removeproofs.ml
+
+doc/removeproofs.ml: doc/removeproofs.mll
+	ocamllex doc/removeproofs.mll
+
 latexdoc:
 	cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES)
 
@@ -103,6 +109,7 @@ install:
 clean:
 	rm -f */*.vo *~ */*~
 	rm -rf doc/html doc/*.glob
+	rm -f doc/removeproofs.ml doc/removeproofs
 	$(MAKE) -C extraction clean
 	$(MAKE) -C runtime clean
 	$(MAKE) -C test/cminor clean

doc/index.html

@@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; }
 
 <H1 align="center">The Compcert verified compiler</H1>
 <H2 align="center">Commented Coq development</H2>
-<H3 align="center">Version 1.1, 2007-09-17</H3>
+<H3 align="center">Version 1.2, 2008-02-13</H3>
 
 <H2>Introduction</H2>
 
@@ -55,11 +55,14 @@ compiler written directly in Caml are omitted.  This development is a
 work in progress; some parts have substantially changed since the
 overview papers above were written.</P>
 
-<P>This document and all Coq source files referenced from it are
-copyright 2005, 2006, 2007 Institut National de Recherche en Informatique et
-en Automatique (INRIA) and distributed under the terms of the <A
-HREF="http://www.gnu.org/licenses/gpl.html">GNU General Public
-License</A> version 2.</P>
+<P>The complete sources for Compcert can be downloaded from
+<A HREF="http://compcert.inria.fr/">the Compcert Web site</A>.</P>
+
+<P>This document and the Compcert sources are
+copyright 2005, 2006, 2007, 2008 Institut National de Recherche en
+Informatique et en Automatique (INRIA) and distributed under the terms
+of the following <A HREF="LICENSE">license</A>.
+</P>
 
 <H2>Table of contents</H2>
 
@@ -67,14 +70,8 @@ License</A> version 2.</P>
 
 <UL>
 <LI> <A HREF="html/Coqlib.html">Coqlib</A>: addendum to the Coq standard library.
-     (Coq source file with proofs:
-      <A HREF="Coqlib.v"><code>Coqlib.v</code></a>.)
 <LI> <A HREF="html/Maps.html">Maps</A>: finite maps.
-     (Coq source file with proofs:
-      <A HREF="Maps.v"><code>Maps.v</code></a>.)
 <LI> <A HREF="html/Integers.html">Integers</A>: machine integers.
-     (Coq source file with proofs:
-      <A HREF="Integers.v"><code>Integers.v</code></a>.)
 <LI> <A HREF="html/Floats.html">Floats</A>: machine floating-point numbers.
 <LI> <A HREF="html/Iteration.html">Iteration</A>: various forms of "while" loops.
 <LI> <A HREF="html/Ordered.html">Ordered</A>: construction of
@@ -92,7 +89,6 @@ inequations by fixpoint iteration.
 <LI> <A HREF="html/Errors.html">Errors</A>: the Error monad.
 <LI> <A HREF="html/AST.html">AST</A>: identifiers, whole programs and other
 common elements of abstract syntaxes.
-     (Coq source file with proofs: <A HREF="AST.v"><code>AST.v</code></a>.)
 <LI> <A HREF="html/Values.html">Values</A>: run-time values.
 <LI> <A HREF="html/Events.html">Events</A>: observable events and traces.
 <LI> <A HREF="html/Mem.html">Mem</A>: the memory model.

doc/removeproofs

-#!/bin/sh
-
-for i in $*; do
-  mv $i $i.bak
-  sed -e '/<span class="keyword">Proof<\/span> *\./,/<span class="keyword">\(Qed\|Defined\)<\/span> *\./d' \
-      -e "s/\"'do' X <- A ; B\" error_monad_scope/doXAB error_monad_scope/g" \
-      -e "s/\"'do' X <- A ; B\"/doXAB/g" \
-      -e "s/\"'do' ( X , Y ) <- A ; B\"/doXYAB/g" \
-      $i.bak > $i
-  rm $i.bak
-done
-

doc/removeproofs.mll

+rule process inproof oc = parse
+  | "<span class=\"keyword\">Proof</span>" ' '* '.'
+      { process true oc lexbuf }
+  | "<span class=\"keyword\">" ("Qed" | "Defined") "</span>" ' '* '.'
+      { process false oc lexbuf }
+  | "<a class=\"idref\" href=\"" 
+    [^ '"'] + '#' '"' [^ '\n' '>']* '"' '"' '>'
+    ([^ '<' '\n']+ as ident)
+    "</a>"
+      { if not inproof then output_string oc ident;
+        process inproof oc lexbuf }
+  | _
+      { if not inproof then output_char oc (Lexing.lexeme_char lexbuf 0);
+        process inproof oc lexbuf }
+  | eof
+      { () }
+
+{
+
+let process_file name =
+  let ic = open_in name in
+  Sys.remove name;
+  let oc = open_out name in
+  process false oc (Lexing.from_channel ic);
+  close_out oc;
+  close_in ic
+
+let _ =
+  for i = 1 to Array.length Sys.argv - 1 do
+    process_file Sys.argv.(i)
+  done
+}
+