summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile9
-rw-r--r--doc/index.html22
-rwxr-xr-xdoc/removeproofs12
-rw-r--r--doc/removeproofs.mll33
4 files changed, 50 insertions, 26 deletions
diff --git a/Makefile b/Makefile
index afadd77..58d494c 100644
--- a/Makefile
+++ b/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
diff --git a/doc/index.html b/doc/index.html
index 1366a84..219e587 100644
--- a/doc/index.html
+++ b/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.
diff --git a/doc/removeproofs b/doc/removeproofs
deleted file mode 100755
index 266711f..0000000
--- a/doc/removeproofs
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/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
-
diff --git a/doc/removeproofs.mll b/doc/removeproofs.mll
new file mode 100644
index 0000000..d4b2431
--- /dev/null
+++ b/doc/removeproofs.mll
@@ -0,0 +1,33 @@
+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
+}
+