diff options
| -rw-r--r-- | Makefile | 9 | ||||
| -rw-r--r-- | doc/index.html | 22 | ||||
| -rwxr-xr-x | doc/removeproofs | 12 | ||||
| -rw-r--r-- | doc/removeproofs.mll | 33 |
4 files changed, 50 insertions, 26 deletions
@@ -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 +} + |