diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/coq2html.css | 5 | ||||
| -rw-r--r-- | doc/coq2html.mll | 32 | ||||
| -rw-r--r-- | doc/index.html | 21 |
3 files changed, 46 insertions, 12 deletions
diff --git a/doc/coq2html.css b/doc/coq2html.css index 0f6680e8..c5627bfb 100644 --- a/doc/coq2html.css +++ b/doc/coq2html.css @@ -7,6 +7,7 @@ div.proofscript contents of proof script span.docright contents of (**r *) comments span.bracket contents of [ ] within comments + span.comment contents of (* *) comments span.kwd Coq keyword span.tactic Coq tactic span.id any other identifier @@ -86,6 +87,10 @@ span.kwd { color: #cf1d1d; } +span.comment { + color: #008000; +} + a:visited {color : #416DFF; text-decoration : none; } a:link {color : #416DFF; text-decoration : none; } a:hover {text-decoration : none; } diff --git a/doc/coq2html.mll b/doc/coq2html.mll index 329e9eaa..2f1bfdbc 100644 --- a/doc/coq2html.mll +++ b/doc/coq2html.mll @@ -206,15 +206,23 @@ let start_verbatim () = let end_verbatim () = fprintf !oc "</pre>\n" +let start_comment () = + fprintf !oc "<span class=\"comment\">(*" + +let end_comment () = + fprintf !oc "*)</span>" + let start_bracket () = fprintf !oc "<span class=\"bracket\">" let end_bracket () = fprintf !oc "</span>" +let in_proof = ref false let proof_counter = ref 0 let start_proof kwd = + in_proof := true; incr proof_counter; fprintf !oc "<div class=\"toggleproof\" onclick=\"toggleDisplay('proof%d')\">%s</div>\n" @@ -222,7 +230,8 @@ let start_proof kwd = fprintf !oc "<div class=\"proofscript\" id=\"proof%d\">\n" !proof_counter let end_proof kwd = - fprintf !oc "%s</div>\n" kwd + fprintf !oc "%s</div>\n" kwd; + in_proof := false let start_html_page modname = fprintf !oc "\ @@ -300,7 +309,8 @@ and coq = parse end_doc_right(); coq lexbuf } | "(*" - { comment lexbuf; + { if !in_proof then start_comment(); + comment lexbuf; coq lexbuf } | path as id { ident (Lexing.lexeme_start lexbuf) id; coq lexbuf } @@ -325,13 +335,23 @@ and bracket = parse and comment = parse | "*)" - { () } + { if !in_proof then end_comment() } | "(*" - { comment lexbuf; comment lexbuf } + { if !in_proof then start_comment(); + comment lexbuf; comment lexbuf } | eof { () } - | _ - { comment lexbuf } + | "\n" + { if !in_proof then newline(); + comment lexbuf } + | space* as s + { if !in_proof then space s; + comment lexbuf } + | eof + { () } + | _ as c + { if !in_proof then character c; + comment lexbuf } and doc_bol = parse | "<<" space* "\n" diff --git a/doc/index.html b/doc/index.html index 296d89e0..29a2fb30 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 2.3, 2015-05-05</H3> +<H3 align="center">Version 2.5, 2015-06-12</H3> <H2>Introduction</H2> @@ -63,7 +63,8 @@ written.</P> <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, 2009, 2010, 2011, 2012, 2013, 2014 Institut +copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 +Institut National de Recherche en Informatique et en Automatique (INRIA) and distributed under the terms of the following <A HREF="LICENSE">license</A>. @@ -115,7 +116,8 @@ semantics. <LI> The CompCert C source language: <A HREF="html/Csyntax.html">syntax</A> and <A HREF="html/Csem.html">semantics</A> and -<A HREF="html/Cstrategy.html">determinized semantics</A>.<BR> +<A HREF="html/Cstrategy.html">determinized semantics</A> and +<A HREF="html/Ctyping.html">type system</A>.<BR> See also: <A HREF="html/Ctypes.html">type expressions</A> and <A HREF="html/Cop.html">operators (syntax and semantics)</A> and <A HREF="html/Cexec.html">reference interpreter</A>. @@ -245,13 +247,20 @@ code. </TR> <TR valign="top"> - <TD>Dead code elimination</TD> + <TD>Redundancy elimination</TD> <TD>RTL to RTL</TD> <TD><A HREF="html/Deadcode.html">Deadcode</A></TD> <TD><A HREF="html/Deadcodeproof.html">Deadcodeproof</A></TD> </TR> <TR valign="top"> + <TD>Removal of unused static globals</TD> + <TD>RTL to RTL</TD> + <TD><A HREF="html/Unusedglob.html">Unusedglob</A></TD> + <TD><A HREF="html/Unusedglobproof.html">Unusedglobproof</A></TD> +</TR> + +<TR valign="top"> <TD>Register allocation (validation a posteriori)</TD> <TD>RTL to LTL</TD> <TD><A HREF="html/Allocation.html">Allocation</A></TD> @@ -315,9 +324,9 @@ See also: <A HREF="html/NeedOp.html"><I>NeedOp</I></A>: processor-dependent part <H3>Type systems</H3> -Simple type systems are used to statically capture well-formedness -conditions on some intermediate languages. +The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions. <UL> +<LI> <A HREF="html/Ctyping.html">RTLtyping</A>: typing for CompCert C + type-checking functions. <LI> <A HREF="html/RTLtyping.html">RTLtyping</A>: typing for RTL + type reconstruction. <LI> <A HREF="html/Lineartyping.html">Lineartyping</A>: typing for Linear. |