From 24951d885fbadb8f2fa96ea44a6d3b2a397eab00 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 1 Jun 2018 10:40:04 +0200 Subject: Use the standalone coq2html tool to generate the HTML documentation coq2html is now a standalone project (https://github.com/xavierleroy/coq2html) packaged as coq-coq2html in OPAM-Coq. --- doc/coq2html.css | 97 ------------ doc/coq2html.js | 24 --- doc/coq2html.mll | 454 ------------------------------------------------------- doc/coqdoc.css | 62 -------- doc/index.html | 230 ++++++++++++++-------------- 5 files changed, 115 insertions(+), 752 deletions(-) delete mode 100644 doc/coq2html.css delete mode 100644 doc/coq2html.js delete mode 100644 doc/coq2html.mll delete mode 100644 doc/coqdoc.css (limited to 'doc') diff --git a/doc/coq2html.css b/doc/coq2html.css deleted file mode 100644 index c5627bfb..00000000 --- a/doc/coq2html.css +++ /dev/null @@ -1,97 +0,0 @@ -/* Classes: - h1.title the title of the page - div.coq encloses all generated body - div.doc contents of (** *) comments - div.footer footer - div.togglescript "Proof." line - 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 -*/ - -body { - color: black; - background: white; -} - -h1.title { - font-size: 2em; - text-align: center -} - -h1 { - font-size: 1.5em; -} -h2 { - font-size: 1.17em; -} -h3 { - font-size: 1em; -} - -h1, h2, h3 { - font-family: sans-serif; - margin-left: -5%; -} - -div.coq { - margin-left: 15%; - margin-right: 5%; - font-family: monospace; -} - -div.doc { - margin-left: -5%; - margin-top: 0.2em; - margin-bottom: 0.5em; - font-family: serif; -} - -div.toggleproof { - font-size: 0.8em; - text-decoration: underline; -} - -div.toggleproof:hover { - cursor: pointer; -} - -div.proofscript { - font-size: 0.8em; -} - -div.footer { - margin-top: 1em; - margin-bottom: 1em; - font-size: 0.8em; - font-style: italic; -} - -span.docright { - position: absolute; - left: 60%; - width: 40%; - font-family: serif; -} - -span.bracket { - font-family: monospace; - color: #008000; -} - -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; } -a:active {text-decoration : none; } diff --git a/doc/coq2html.js b/doc/coq2html.js deleted file mode 100644 index a840b004..00000000 --- a/doc/coq2html.js +++ /dev/null @@ -1,24 +0,0 @@ -function toggleDisplay(id) -{ - var elt = document.getElementById(id); - if (elt.style.display == 'none') { - elt.style.display = 'block'; - } else { - elt.style.display = 'none'; - } -} - -function hideAll(cls) -{ - var testClass = new RegExp("(^|s)" + cls + "(s|$)"); - var tag = tag || "*"; - var elements = document.getElementsByTagName("div"); - var current; - var length = elements.length; - for(var i=0; i", "<>" -> "" - | "<>", _ -> id - | _ , "<>" -> sp - | _ , _ -> sp ^ "." ^ id - -let add_module m = - (*eprintf "add_module %s\n" m;*) - Hashtbl.add xref_modules m () - -let add_reference curmod pos dp sp id ty = - (*eprintf "add_reference %s %d %s %s %s %s\n" curmod pos dp sp id ty;*) - if not (Hashtbl.mem xref_table (curmod, pos)) - then Hashtbl.add xref_table (curmod, pos) (Ref(dp, path sp id, ty)) - -let add_definition curmod pos sp id ty = - if not (Hashtbl.mem xref_table (curmod, pos)) - then Hashtbl.add xref_table (curmod, pos) (Def(path sp id, ty)) - -type link = Link of string | Anchor of string | Nolink - -let coqlib_url = "http://coq.inria.fr/library/" - -let re_coqlib = Str.regexp "Coq\\." -let re_sane_path = Str.regexp "[A-Za-z0-9_.]+$" -let re_shortname = Str.regexp "^.*\\." - -let shortname m = Str.replace_first re_shortname "" m - -let crossref m pos = - (*eprintf "crossref %s %d\n" m pos;*) - try match Hashtbl.find xref_table (m, pos) with - | Def(p, _) -> - Anchor p - | Ref(m', p, _) -> - let url = - if Hashtbl.mem xref_modules m' then - shortname m' ^ ".html" - else if Str.string_match re_coqlib m' 0 then - coqlib_url ^ m' ^ ".html" - else - raise Not_found in - if p = "" then - Link url - else if Str.string_match re_sane_path p 0 then - Link(url ^ "#" ^ p) - else - Nolink - with Not_found -> - Nolink - -(** Keywords, etc *) - -module StringSet = Set.Make(String) - -let mkset l = List.fold_right StringSet.add l StringSet.empty - -let coq_keywords = mkset [ - "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; - "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; - "where"; "struct"; "wf"; "measure"; - "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; - "Coercion"; "CoFixpoint"; "CoInductive"; "Corollary"; "Defined"; - "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix"; - "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; - "Hypotheses"; "Resolve"; "Unfold"; "Immediate"; "Extern"; - "Implicit"; "Import"; "Inductive"; "Infix"; "Lemma"; "Let"; "Load"; - "Local"; "Ltac"; "Module"; "Module Type"; "Declare Module"; - "Include"; "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; - "Qed"; "Record"; "Recursive"; "Remark"; "Require"; - "Save"; "Scheme"; "Induction"; "for"; "Sort"; "Section"; "Show"; - "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; "Set"; - "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; - "Notation"; "Reserved"; "Tactic"; "Delimit"; "Bind"; "Open"; - "Scope"; "Boxed"; "Unboxed"; "Inline"; "Implicit Arguments"; "Add"; - "Strict"; "Typeclasses"; "Instance"; "Global Instance"; "Class"; - "Instantiation"; "subgoal"; "Program"; "Example"; "Obligation"; - "Obligations"; "Solve"; "using"; "Next"; "Instance"; "Equations"; - "Equations_nocomp" -] - -let coq_tactics = mkset [ - "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; - "injection"; "elimtype"; "progress"; "setoid_rewrite"; "destruct"; - "destruction"; "destruct_call"; "dependent"; "elim"; - "extensionality"; "f_equal"; "generalize"; "generalize_eqs"; - "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; - "set"; "assert"; "do"; "repeat"; "cut"; "assumption"; "exact"; - "split"; "subst"; "try"; "discriminate"; "simpl"; "unfold"; "red"; - "compute"; "at"; "in"; "by"; "reflexivity"; "symmetry"; - "transitivity"; "replace"; "setoid_replace"; "inversion"; - "inversion_clear"; "pattern"; "intuition"; "congruence"; "fail"; - "fresh"; "trivial"; "exact"; "tauto"; "firstorder"; "ring"; - "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; - "eauto" -] - -(** HTML generation *) - -let oc = ref stdout - -let character = function - | '<' -> output_string !oc "<" - | '>' -> output_string !oc ">" - | '&' -> output_string !oc "&" - | c -> output_char !oc c - -let section_level = function - | "*" -> 1 - | "**" -> 2 - | _ -> 3 - -let start_section sect = - fprintf !oc "" (section_level sect) -let end_section sect = - fprintf !oc "\n" (section_level sect) - -let start_doc_right () = - fprintf !oc "(* " -let end_doc_right () = - fprintf !oc " *)" - -let enum_depth = ref 0 - -let set_enum_depth d = - if !enum_depth < d then begin - fprintf !oc "\n"; - decr enum_depth; - end - else if !enum_depth > 0 then begin - fprintf !oc "\n"; - fprintf !oc "
  • \n" - end - -let start_doc () = - fprintf !oc "
    " -let end_doc () = - set_enum_depth 0; - fprintf !oc "
    \n" - -let ident pos id = - if StringSet.mem id coq_keywords then - fprintf !oc "%s" id - else if StringSet.mem id coq_tactics then - fprintf !oc "%s" id - else match crossref !current_module pos with - | Nolink -> - fprintf !oc "%s" id - | Link p -> - fprintf !oc "%s" p id - | Anchor p -> - fprintf !oc "%s" p id - -let space s = - for _ = 1 to String.length s do fprintf !oc " " done - -let newline () = - fprintf !oc "
    \n" - -let dashes = function - | "-" -> set_enum_depth 1 - | "--" -> set_enum_depth 2 - | "---" -> set_enum_depth 3 - | "----" -> set_enum_depth 4 - | _ -> fprintf !oc "
    \n" - -let start_verbatim () = - fprintf !oc "
    \n"
-
-let end_verbatim () =
-  fprintf !oc "
    \n" - -let start_comment () = - fprintf !oc "(*" - -let end_comment () = - fprintf !oc "*)" - -let start_bracket () = - fprintf !oc "" - -let end_bracket () = - fprintf !oc "" - -let in_proof = ref false -let proof_counter = ref 0 - -let start_proof kwd = - in_proof := true; - incr proof_counter; - fprintf !oc - "
    %s
    \n" - !proof_counter kwd; - fprintf !oc "
    \n" !proof_counter - -let end_proof kwd = - fprintf !oc "%s
    \n" kwd; - in_proof := false - -let start_html_page modname = - fprintf !oc -{| - - - - -Module %s - - - - - - -

    Module %s

    -
    -|} modname modname modname - -let end_html_page () = - fprintf !oc -{|
    -
    Generated by coq2html
    - - -|} - -} - -let space = [' ' '\t'] -let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* -let path = ident ("." ident)* -let start_proof = ("Proof" space* ".") | ("Proof" space+ "with") | ("Next" space+ "Obligation.") -let end_proof = "Qed." | "Defined." | "Save." | "Admitted." | "Abort." - -let xref = ['A'-'Z' 'a'-'z' '0'-'9' '_' '.']+ | "<>" -let integer = ['0'-'9']+ - -rule coq_bol = parse - | space* (start_proof as sp) - { start_proof sp; - skip_newline lexbuf } - | space* "(** " ("*"+ as sect) - { start_section sect; - doc lexbuf; - end_section sect; - skip_newline lexbuf } - | space* "(** " - { start_doc(); - doc lexbuf; - end_doc(); - skip_newline lexbuf } - | space* "(*" - { comment lexbuf; - skip_newline lexbuf } - | eof - { () } - | space* as s - { space s; - coq lexbuf } - -and skip_newline = parse - | space* "\n" - { coq_bol lexbuf } - | "" - { coq lexbuf } - -and coq = parse - | end_proof as ep - { end_proof ep; - skip_newline lexbuf } - | "(**r " - { start_doc_right(); - doc lexbuf; - end_doc_right(); - coq lexbuf } - | "(*" - { if !in_proof then start_comment(); - comment lexbuf; - coq lexbuf } - | path as id - { ident (Lexing.lexeme_start lexbuf) id; coq lexbuf } - | "\n" - { newline(); coq_bol lexbuf } - | eof - { () } - | _ as c - { character c; coq lexbuf } - -and bracket = parse - | ']' - { () } - | '[' - { character '['; bracket lexbuf; character ']'; bracket lexbuf } - | path as id - { ident (Lexing.lexeme_start lexbuf) id; bracket lexbuf } - | eof - { () } - | _ as c - { character c; bracket lexbuf } - -and comment = parse - | "*)" - { if !in_proof then end_comment() } - | "(*" - { if !in_proof then start_comment(); - comment lexbuf; comment lexbuf } - | eof - { () } - | "\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" - { start_verbatim(); - verbatim lexbuf; - end_verbatim(); - doc_bol lexbuf } - | "-"+ as d - { dashes d; doc lexbuf } - | "\n" - { set_enum_depth 0; doc_bol lexbuf } - | "" - { doc lexbuf } - -and doc = parse - | "*)" - { () } - | "\n" - { character '\n'; doc_bol lexbuf } - | "[" - { start_bracket(); bracket lexbuf; end_bracket(); doc lexbuf } - | "$" [^ '\n' '$']* "$" - { doc lexbuf } - | "#" ([^ '\n' '#']* as html) "#" - { output_string !oc html; doc lexbuf } - | eof - { () } - | _ as c - { character c; doc lexbuf } - -and verbatim = parse - | "\n>>" space* "\n" - { () } - | eof - { () } - | _ as c - { character c; verbatim lexbuf } - -and globfile = parse - | eof - { () } - | "F" (path as m) space* "\n" - { current_module := m; add_module m; - globfile lexbuf } - | "R" (integer as pos) ":" (integer) - space+ (xref as dp) - space+ (xref as sp) - space+ (xref as id) - space+ (ident as ty) - space* "\n" - { add_reference !current_module (int_of_string pos) dp sp id ty; - globfile lexbuf } - | (ident as ty) - space+ (integer as pos) ":" (integer) - space+ (xref as sp) - space+ (xref as id) - space* "\n" - { add_definition !current_module (int_of_string pos) sp id ty; - globfile lexbuf } - | [^ '\n']* "\n" - { globfile lexbuf } - -{ - -let output_name = ref "-" - -let process_file f = - if Filename.check_suffix f ".v" then begin - let pref_f = Filename.chop_suffix f ".v" in - let base_f = Filename.basename pref_f in - current_module := - "compcert." ^ Str.global_replace (Str.regexp "/") "." pref_f; - let ic = open_in f in - if !output_name = "-" then - oc := stdout - else - oc := open_out (Str.global_replace (Str.regexp "%") base_f !output_name); - start_html_page base_f; - coq_bol (Lexing.from_channel ic); - end_html_page(); - if !output_name <> "-" then (close_out !oc; oc := stdout); - close_in ic - end else - if Filename.check_suffix f ".glob" then begin - current_module := ""; - let ic = open_in f in - globfile (Lexing.from_channel ic); - close_in ic - end else begin - eprintf "Don't know what to do with file %s\n" f; - exit 2 - end - -let _ = - Arg.parse [ - "-o", Arg.String (fun s -> output_name := s), - " Set output file ('%' replaced by module name)" - ] process_file - "Usage: coq2html [options] file.v\nOptions are:" -} diff --git a/doc/coqdoc.css b/doc/coqdoc.css deleted file mode 100644 index f2ae96da..00000000 --- a/doc/coqdoc.css +++ /dev/null @@ -1,62 +0,0 @@ -body { - color: black; - background: white; - margin-left: 15%; - margin-right: 5%; -} - -#main a.idref:visited {color : #416DFF; text-decoration : none; } -#main a.idref:link {color : #416DFF; text-decoration : none; } -#main a.idref:hover {text-decoration : none; } -#main a.idref:active {text-decoration : none; } - -#main a.modref:visited {color : #416DFF; text-decoration : none; } -#main a.modref:link {color : #416DFF; text-decoration : none; } -#main a.modref:hover {text-decoration : none; } -#main a.modref:active {text-decoration : none; } - -#main .keyword { color : #cf1d1d } - -#main .doc { - margin-left: -5%; -} - -#main span.docright { - position: absolute; - left: 60%; - width: 40% -} - -h1.libtitle { - font-size: 2em; - margin-left: -15%; - margin-right: -5%; - text-align: center -} - -h1 { - font-size: 1.5em; -} -h2 { - font-size: 1.17em; -} - -h1, h2 { - font-family: sans-serif; -} - -.doc code { - color: #008000; -} - -/* Pied de page */ - -hr { margin-left: -15%; margin-right:-5%; } - -#footer { font-size: 0.83em; - font-family: sans-serif; } - -#footer a:visited { color: blue; } -#footer a:link { text-decoration: none; - color: #888888; } - diff --git a/doc/index.html b/doc/index.html index 2ac5f698..60c4e9a0 100644 --- a/doc/index.html +++ b/doc/index.html @@ -69,73 +69,73 @@ following license.

    General-purpose libraries, data structures and algorithms

      -
    • Coqlib: addendum to the Coq standard library. -
    • Maps: finite maps. -
    • Integers: machine integers. -
    • Floats: machine floating-point numbers. -
    • Iteration: various forms of "while" loops. -
    • Ordered: construction of +
    • Coqlib: addendum to the Coq standard library. +
    • Maps: finite maps. +
    • Integers: machine integers. +
    • Floats: machine floating-point numbers. +
    • Iteration: various forms of "while" loops. +
    • Ordered: construction of ordered types. -
    • Lattice: construction of +
    • Lattice: construction of semi-lattices. -
    • Kildall: resolution of dataflow +
    • Kildall: resolution of dataflow inequations by fixpoint iteration. -
    • UnionFind: a persistent union-find data structure. -
    • Postorder: postorder numbering of a directed graph. +
    • UnionFind: a persistent union-find data structure. +
    • Postorder: postorder numbering of a directed graph.

    Definitions and theorems used in many parts of the development

      -
    • Errors: the Error monad. -
    • AST: identifiers, whole programs and other +
    • Errors: the Error monad. +
    • AST: identifiers, whole programs and other common elements of abstract syntaxes. -
    • Linking: generic framework to define syntactic linking over the CompCert languages. -
    • Values: run-time values. -
    • Events: observable events and traces. -
    • Memory: memory model.
      -See also: Memdata (in-memory representation of data). -
    • Globalenvs: global execution environments. -
    • Smallstep: tools for small-step semantics. -
    • Behaviors: from small-step semantics to observable behaviors of programs. -
    • Determinism: determinism properties of small-step semantics. -
    • Op: operators, addressing modes and their +
    • Linking: generic framework to define syntactic linking over the CompCert languages. +
    • Values: run-time values. +
    • Events: observable events and traces. +
    • Memory: memory model.
      +See also: Memdata (in-memory representation of data). +
    • Globalenvs: global execution environments. +
    • Smallstep: tools for small-step semantics. +
    • Behaviors: from small-step semantics to observable behaviors of programs. +
    • Determinism: determinism properties of small-step semantics. +
    • Op: operators, addressing modes and their semantics. -
    • Unityping: a solver for atomic unification constraints. +
    • Unityping: a solver for atomic unification constraints.

    Source, intermediate and target languages: syntax and semantics

    @@ -153,170 +153,170 @@ code. Pulling side-effects out of expressions;
    fixing an evaluation order CompCert C to Clight - SimplExpr - SimplExprspec
    - SimplExprproof + SimplExpr + SimplExprspec
    + SimplExprproof Pulling non-adressable scalar local variables out of memory Clight to Clight - SimplLocals - SimplLocalsproof + SimplLocals + SimplLocalsproof Simplification of control structures;
    explication of type-dependent computations Clight to Csharpminor - Cshmgen - Cshmgenproof + Cshmgen + Cshmgenproof Stack allocation of local variables
    whose address is taken;
    simplification of switch statements Csharpminor to Cminor - Cminorgen - Cminorgenproof + Cminorgen + Cminorgenproof Recognition of operators
    and addressing modes Cminor to CminorSel - Selection
    - SelectOp
    - SelectLong
    - SelectDiv
    - SplitLong - Selectionproof
    - SelectOpproof
    - SelectLongproof
    - SelectDivproof
    - SplitLongproof + Selection
    + SelectOp
    + SelectLong
    + SelectDiv
    + SplitLong + Selectionproof
    + SelectOpproof
    + SelectLongproof
    + SelectDivproof
    + SplitLongproof Construction of the CFG,
    3-address code generation CminorSel to RTL - RTLgen - RTLgenspec
    - RTLgenproof + RTLgen + RTLgenspec
    + RTLgenproof Recognition of tail calls RTL to RTL - Tailcall - Tailcallproof + Tailcall + Tailcallproof Function inlining RTL to RTL - Inlining - Inliningspec
    - Inliningproof + Inlining + Inliningspec
    + Inliningproof Postorder renumbering of the CFG RTL to RTL - Renumber - Renumberproof + Renumber + Renumberproof Constant propagation RTL to RTL - Constprop
    - ConstpropOp - Constpropproof
    - ConstproppOproof + Constprop
    + ConstpropOp + Constpropproof
    + ConstproppOproof Common subexpression elimination RTL to RTL - CSE
    - CombineOp - CSEproof
    - CombineOpproof + CSE
    + CombineOp + CSEproof
    + CombineOpproof Redundancy elimination RTL to RTL - Deadcode - Deadcodeproof + Deadcode + Deadcodeproof Removal of unused static globals RTL to RTL - Unusedglob - Unusedglobproof + Unusedglob + Unusedglobproof Register allocation (validation a posteriori) RTL to LTL - Allocation - Allocproof + Allocation + Allocproof Branch tunneling LTL to LTL - Tunneling - Tunnelingproof + Tunneling + Tunnelingproof Linearization of the CFG LTL to Linear - Linearize - Linearizeproof + Linearize + Linearizeproof Removal of unreferenced labels Linear to Linear - CleanupLabels - CleanupLabelsproof + CleanupLabels + CleanupLabelsproof Synthesis of debugging information Linear to Linear - Debugvar - Debugvarproof + Debugvar + Debugvarproof Laying out the activation records Linear to Mach - Stacking
    - Bounds
    - Stacklayout - Stackingproof
    - Separation + Stacking
    + Bounds
    + Stacklayout + Stackingproof
    + Separation Emission of assembly code Mach to Asm - Asmgen - Asmgenproof0
    - Asmgenproof1
    - Asmgenproof + Asmgen + Asmgenproof0
    + Asmgenproof1
    + Asmgenproof

    All together

      -
    • Compiler: composing the passes together; +
    • Compiler: composing the passes together; whole-compiler semantic preservation theorems. -
    • Complements: interesting consequences of the semantic preservation theorems. +
    • Complements: interesting consequences of the semantic preservation theorems.

    Static analyses

    @@ -325,23 +325,23 @@ The following static analyses are performed over the RTL intermediate representation to support optimizations such as constant propagation, CSE, and dead code elimination.
      -
    • Liveness: liveness analysis. -
    • ValueAnalysis: value and alias analysis
      -See also: ValueDomain: the abstract domain for value analysis.
      -See also: ValueAOp: processor-dependent parts of value analysis. -
    • Deadcode: neededness analysis
      -See also: NeedDomain: the abstract domain for neededness analysis.
      -See also: NeedOp: processor-dependent parts of neededness analysis. +
    • Liveness: liveness analysis. +
    • ValueAnalysis: value and alias analysis
      +See also: ValueDomain: the abstract domain for value analysis.
      +See also: ValueAOp: processor-dependent parts of value analysis. +
    • Deadcode: neededness analysis
      +See also: NeedDomain: the abstract domain for neededness analysis.
      +See also: NeedOp: processor-dependent parts of neededness analysis.

    Type systems

    -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. +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.
    -- cgit