diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 00000000..d2a9a513 --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,9 @@ +version: 2 +updates: + - package-ecosystem: "github-actions" + directory: "/" + schedule: + # Check for updates to GitHub Actions every weekday + interval: "daily" + labels: + - "dependencies" diff --git a/.github/workflows/ci_build.yaml b/.github/workflows/ci_build.yaml index bfa86005..6f87fabc 100644 --- a/.github/workflows/ci_build.yaml +++ b/.github/workflows/ci_build.yaml @@ -35,7 +35,16 @@ jobs: - name: repo checkout uses: actions/checkout@v3 - + + - name: Initialise variables + run: | + # Only deploy if the build follows from pushing to master + if [[ '${{ github.ref }}' == 'refs/heads/main' ]]; then + echo "DOC_DEPLOY=true" >> $GITHUB_ENV + else + echo "DOC_DEPLOY=false" >> $GITHUB_ENV + fi + - name: container registry log in uses: docker/login-action@v3 with: @@ -56,19 +65,21 @@ jobs: sudo chown -R coq:coq . endGroup script: | - startGroup "Build Coq lib" - cd theories/ - make -j ${{ steps.cpu-cores.outputs.count }} pretty-timed + startGroup "Build binary" + if [[ "$DOC" ]]; then + make coqdoc + else + make + fi endGroup after_script: | - startGroup "Build binary" - cd .. - make + startGroup "after" endGroup export: "OPAMJOBS OPAMYES" env: OPAMJOBS: ${{ steps.cpu-cores.outputs.count }} OPAMYES: "true" + DOC: ${{ env.DOC_DEPLOY }} - name: permissions revert # to avoid a warning at cleanup time diff --git a/.gitignore b/.gitignore index 0c348ed6..b3928d05 100644 --- a/.gitignore +++ b/.gitignore @@ -18,6 +18,7 @@ CoqMakefile.mk* !CoqMakefile.mk.local !CoqMakefile.mk.local-late *.log +theories/html/ # Editor related ## Emacs diff --git a/Makefile b/Makefile index 2f1df769..a690d785 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,13 @@ .PHONY: all clean all: - @make -C theories + @$(MAKE) -C theories @dune build +coqdoc: all + @${MAKE} coqdoc -C theories + clean: - @make clean -C theories + @$(MAKE) clean -C theories @dune clean @echo "Cleaning finished." diff --git a/README.md b/README.md index cb10422d..c2c90121 100644 --- a/README.md +++ b/README.md @@ -9,6 +9,9 @@ sound and complete: a program passes typechecking if and only if it is a well-ty program in MLTT. This will be the first verified proof assistant (despite being elementary) and serves as a basis for future extensions. +## Online Documentation + +We have generated a [Coqdoc](toc.html) for browsing our Coq proof. ## Architecture @@ -67,19 +70,21 @@ opam install ppx_inline_test ## Development -Before anything, the Coq parser must be extracted to OCaml code. Then, you can run `dune build` like normal for all other changes. +Use the toplevel `make` to build the whole project: +``` +make +``` +Makefile will try to find out the number of your CPU cores and parallel as much as +possible. -You can build changes to the Coq parser with the following commands: +Once `make` finishes, you can run the binary: ``` -cd theories -make -j16 # or the number of your cpus -cd .. -dune build +_build/default/driver/mcltt.exe examples/nary.mcl # or your own example ``` -Then you can interact with the parser at the toplevel with `dune utop`: +To build Coq proof only, you can go into and only build the Coq folder: ``` -# open Mcltt;; -# open Parser.Cst;; -# Main.parse "" +cd theories +make ``` + diff --git a/assets/extra/footer.html b/assets/extra/footer.html new file mode 100644 index 00000000..2ff40b3f --- /dev/null +++ b/assets/extra/footer.html @@ -0,0 +1,8 @@ + + + + + + diff --git a/assets/extra/header.html b/assets/extra/header.html new file mode 100644 index 00000000..98ff925f --- /dev/null +++ b/assets/extra/header.html @@ -0,0 +1,27 @@ + + + + + + + + + + + + + +
+
diff --git a/assets/extra/resources/config.js b/assets/extra/resources/config.js new file mode 100644 index 00000000..72be6131 --- /dev/null +++ b/assets/extra/resources/config.js @@ -0,0 +1,72 @@ +var coqdocjs = coqdocjs || {}; + +coqdocjs.repl = { + "forall": "∀", + "exists": "∃", + "~": "¬", + "/\\": "∧", + "\\/": "∨", + "->": "→", + "<-": "←", + "<->": "↔", + "=>": "⇒", + "<>": "≠", + "<=": "≤", + ">=": "≥", + "el": "∈", + "nel": "∉", + "<<=": "⊆", + "|-": "⊢", + ">>": "»", + "<<": "⊆", + "++": "⧺", + "===": "≡", + "=/=": "≢", + "=~=": "≅", + "==>": "⟹", + "lhd": "⊲", + "rhd": "⊳", + "nat": "ℕ", + "alpha": "α", + "beta": "β", + "gamma": "γ", + "delta": "δ", + "epsilon": "ε", + "eta": "η", + "iota": "ι", + "kappa": "κ", + "lambda": "λ", + "mu": "μ", + "nu": "ν", + "omega": "ω", + "phi": "ϕ", + "pi": "π", + "psi": "ψ", + "rho": "ρ", + "sigma": "σ", + "tau": "τ", + "theta": "θ", + "xi": "ξ", + "zeta": "ζ", + "Delta": "Δ", + "Gamma": "Γ", + "Pi": "Π", + "Sigma": "Σ", + "Omega": "Ω", + "Xi": "Ξ" +}; + +coqdocjs.subscr = { + "0" : "₀", + "1" : "₁", + "2" : "₂", + "3" : "₃", + "4" : "₄", + "5" : "₅", + "6" : "₆", + "7" : "₇", + "8" : "₈", + "9" : "₉", +}; + +coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="]; diff --git a/assets/extra/resources/coqdoc.css b/assets/extra/resources/coqdoc.css new file mode 100644 index 00000000..18dad894 --- /dev/null +++ b/assets/extra/resources/coqdoc.css @@ -0,0 +1,197 @@ +@import url(https://fonts.googleapis.com/css?family=Open+Sans:400,700); + +body{ + font-family: 'Open Sans', sans-serif; + font-size: 14px; + color: #2D2D2D +} + +a { + text-decoration: none; + border-radius: 3px; + padding-left: 3px; + padding-right: 3px; + margin-left: -3px; + margin-right: -3px; + color: inherit; + font-weight: bold; +} + +#main .code a, #main .inlinecode a, #toc a { + font-weight: inherit; +} + +a[href]:hover, [clickable]:hover{ + background-color: rgba(0,0,0,0.1); + cursor: pointer; +} + +h, h1, h2, h3, h4, h5 { + line-height: 1; + color: black; + text-rendering: optimizeLegibility; + font-weight: normal; + letter-spacing: 0.1em; + text-align: left; +} + +div + br { + display: none; +} + +div:empty{ display: none;} + +#main h1 { + font-size: 2em; +} + +#main h2 { + font-size: 1.667rem; +} + +#main h3 { + font-size: 1.333em; +} + +#main h4, #main h5, #main h6 { + font-size: 1em; +} + +#toc h2 { + padding-bottom: 0; +} + +#main .doc { + margin: 0; + text-align: justify; +} + +.inlinecode, .code, #main pre { + font-family: monospace; +} + +.code > br:first-child { + display: none; +} + +.doc + .code{ + margin-top:0.5em; +} + +.block{ + display: block; + margin-top: 5px; + margin-bottom: 5px; + padding: 10px; + text-align: center; +} + +.block img{ + margin: 15px; +} + +table.infrule { + border: 0px; + margin-left: 50px; + margin-top: 10px; + margin-bottom: 10px; +} + +td.infrule { + font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace; + text-align: center; + padding: 0; + line-height: 1; +} + +tr.infrulemiddle hr { + margin: 1px 0 1px 0; +} + +.infrulenamecol { + color: rgb(60%,60%,60%); + padding-left: 1em; + padding-bottom: 0.1em +} + +.id[type="constructor"], .id[type="projection"], .id[type="method"], +.id[title="constructor"], .id[title="projection"], .id[title="method"] { + color: #A30E16; +} + +.id[type="var"], .id[type="variable"], +.id[title="var"], .id[title="variable"] { + color: inherit; +} + +.id[type="definition"], .id[type="record"], .id[type="class"], .id[type="instance"], .id[type="inductive"], .id[type="library"], +.id[title="definition"], .id[title="record"], .id[title="class"], .id[title="instance"], .id[title="inductive"], .id[title="library"] { + color: #A6650F; +} + +.id[type="lemma"], +.id[title="lemma"]{ + color: #188B0C; +} + +.id[type="keyword"], .id[type="notation"], .id[type="abbreviation"], +.id[title="keyword"], .id[title="notation"], .id[title="abbreviation"]{ + color : #2874AE; +} + +.comment { + color: #808080; +} + +/* TOC */ + +#toc h2{ + letter-spacing: 0; + font-size: 1.333em; +} + +/* Index */ + +#index { + margin: 0; + padding: 0; + width: 100%; +} + +#index #frontispiece { + margin: 1em auto; + padding: 1em; + width: 60%; +} + +.booktitle { font-size : 140% } +.authors { font-size : 90%; + line-height: 115%; } +.moreauthors { font-size : 60% } + +#index #entrance { + text-align: center; +} + +#index #entrance .spacer { + margin: 0 30px 0 30px; +} + +ul.doclist { + margin-top: 0em; + margin-bottom: 0em; +} + +#toc > * { + clear: both; +} + +#toc > a { + display: block; + float: left; + margin-top: 1em; +} + +#toc a h2{ + display: inline; +} diff --git a/assets/extra/resources/coqdocjs.css b/assets/extra/resources/coqdocjs.css new file mode 100644 index 00000000..d94bb581 --- /dev/null +++ b/assets/extra/resources/coqdocjs.css @@ -0,0 +1,249 @@ +/* replace unicode */ + +.id[repl] .hidden { + font-size: 0; +} + +.id[repl]:before{ + content: attr(repl); +} + +/* folding proofs */ + +@keyframes show-proof { + 0% { + max-height: 1.2em; + opacity: 1; + } + 99% { + max-height: 1000em; + } + 100%{ + } +} + +@keyframes hide-proof { + from { + visibility: visible; + max-height: 10em; + opacity: 1; + } + to { + max-height: 1.2em; + } +} + +.proof { + cursor: pointer; +} +.proof * { + cursor: pointer; +} + +.proof { + overflow: hidden; + position: relative; + transition: opacity 1s; + display: inline-block; +} + +.proof[show="false"] { + max-height: 1.2em; + visibility: visible; + opacity: 0.3; +} + +.proof[show="false"][animate] { + animation-name: hide-proof; + animation-duration: 0.25s; +} + +.proof[show=true] { + animation-name: show-proof; + animation-duration: 10s; +} + +.proof[show="false"]:before { + position: absolute; + visibility: visible; + width: 100%; + height: 100%; + display: block; + opacity: 0; + content: "M"; +} +.proof[show="false"]:hover:before { + content: ""; +} + +.proof[show="false"] + br + br { + display: none; +} + +.proof[show="false"]:hover { + visibility: visible; + opacity: 0.5; +} + +#toggle-proofs[proof-status="no-proofs"] { + display: none; +} + +#toggle-proofs[proof-status="some-hidden"]:before { + content: "Show Proofs"; +} + +#toggle-proofs[proof-status="all-shown"]:before { + content: "Hide Proofs"; +} + + +/* page layout */ + +html, body { + height: 100%; + margin:0; + padding:0; +} + +@media only screen { /* no div with internal scrolling to allow printing of whole content */ + body { + display: flex; + flex-direction: column + } + + #content { + flex: 1; + overflow: auto; + display: flex; + flex-direction: column; + } +} + +#content:focus { + outline: none; /* prevent glow in OS X */ +} + +#main { + display: block; + padding: 16px; + padding-top: 1em; + padding-bottom: 2em; + margin-left: auto; + margin-right: auto; + max-width: 60em; + flex: 1 0 auto; +} + +.libtitle { + display: none; +} + +/* header */ +#header { + width:100%; + padding: 0; + margin: 0; + display: flex; + align-items: center; + background-color: rgb(21,57,105); + color: white; + font-weight: bold; + overflow: hidden; +} + + +.button { + cursor: pointer; +} + +#header * { + text-decoration: none; + vertical-align: middle; + margin-left: 15px; + margin-right: 15px; +} + +#header > .right, #header > .left { + display: flex; + flex: 1; + align-items: center; +} +#header > .left { + text-align: left; +} +#header > .right { + flex-direction: row-reverse; +} + +#header a, #header .button { + color: white; + box-sizing: border-box; +} + +#header a { + border-radius: 0; + padding: 0.2em; +} + +#header .button { + background-color: rgb(63, 103, 156); + border-radius: 1em; + padding-left: 0.5em; + padding-right: 0.5em; + margin: 0.2em; +} + +#header a:hover, #header .button:hover { + background-color: rgb(181, 213, 255); + color: black; +} + +#header h1 { padding: 0; + margin: 0;} + +/* footer */ +#footer { + text-align: center; + opacity: 0.5; + font-size: 75%; +} + +/* hyperlinks */ + +@keyframes highlight { + 50%{ + background-color: black; + } +} + +:target * { + animation-name: highlight; + animation-duration: 1s; +} + +a[name]:empty { + float: right; +} + +/* Proviola */ + +div.code { + width: auto; + float: none; +} + +div.goal { + position: fixed; + left: 75%; + width: 25%; + top: 3em; +} + +div.doc { + clear: both; +} + +span.command:hover { + background-color: inherit; +} diff --git a/assets/extra/resources/coqdocjs.js b/assets/extra/resources/coqdocjs.js new file mode 100644 index 00000000..7ff56988 --- /dev/null +++ b/assets/extra/resources/coqdocjs.js @@ -0,0 +1,189 @@ +var coqdocjs = coqdocjs || {}; +(function(){ + +function replace(s){ + var m; + if (m = s.match(/^(.+)'/)) { + return replace(m[1])+"'"; + } else if (m = s.match(/^([A-Za-z]+)_?(\d+)$/)) { + return replace(m[1])+m[2].replace(/\d/g, function(d){ + if (coqdocjs.subscr.hasOwnProperty(d)) { + return coqdocjs.subscr[d]; + } else { + return d; + } + }); + } else if (coqdocjs.repl.hasOwnProperty(s)){ + return coqdocjs.repl[s] + } else { + return s; + } +} + +function toArray(nl){ + return Array.prototype.slice.call(nl); +} + +function replInTextNodes() { + coqdocjs.replInText.forEach(function(toReplace){ + toArray(document.getElementsByClassName("code")).concat(toArray(document.getElementsByClassName("inlinecode"))).forEach(function(elem){ + toArray(elem.childNodes).forEach(function(node){ + if (node.nodeType != Node.TEXT_NODE) return; + var fragments = node.textContent.split(toReplace); + node.textContent = fragments[fragments.length-1]; + for (var k = 0; k < fragments.length - 1; ++k) { + node.parentNode.insertBefore(document.createTextNode(fragments[k]),node); + var replacement = document.createElement("span"); + replacement.appendChild(document.createTextNode(toReplace)); + replacement.setAttribute("class", "id"); + replacement.setAttribute("type", "keyword"); + node.parentNode.insertBefore(replacement, node); + } + }); + }); + }); +} + +function replNodes() { + toArray(document.getElementsByClassName("id")).forEach(function(node){ + if (["var", "variable", "keyword", "notation", "definition", "inductive"].indexOf(node.getAttribute("type"))>=0){ + var text = node.textContent; + var replText = replace(text); + if(text != replText) { + node.setAttribute("repl", replText); + node.setAttribute("title", text); + var hidden = document.createElement("span"); + hidden.setAttribute("class", "hidden"); + while (node.firstChild) { + hidden.appendChild(node.firstChild); + } + node.appendChild(hidden); + } + } + }); +} + +function isVernacStart(l, t){ + t = t.trim(); + for(var s of l){ + if (t == s || t.startsWith(s+" ") || t.startsWith(s+".")){ + return true; + } + } + return false; +} + +function isProofStart(n){ + return isVernacStart(["Proof"], n.textContent) && !isVernacStart(["Default", "Suggest"], n.previousSibling.previousSibling.textContent) || + (isVernacStart(["Next"], n.textContent) && isVernacStart(["Obligation"], n.nextSibling.nextSibling.textContent)); +} + +function isProofEnd(s){ + return isVernacStart(["Qed", "Admitted", "Defined", "Abort"], s); +} + +function proofStatus(){ + var proofs = toArray(document.getElementsByClassName("proof")); + if(proofs.length) { + for(var proof of proofs) { + if (proof.getAttribute("show") === "false") { + return "some-hidden"; + } + } + return "all-shown"; + } + else { + return "no-proofs"; + } +} + +function updateView(){ + document.getElementById("toggle-proofs").setAttribute("proof-status", proofStatus()); +} + +function foldProofs() { + var hasCommands = true; + var nodes = document.getElementsByClassName("command"); + if(nodes.length == 0) { + hasCommands = false; + console.log("no command tags found") + nodes = document.getElementsByClassName("id"); + } + toArray(nodes).forEach(function(node){ + if(isProofStart(node)) { + var proof = document.createElement("span"); + proof.setAttribute("class", "proof"); + + node.parentNode.insertBefore(proof, node); + if(proof.previousSibling.nodeType === Node.TEXT_NODE) + proof.appendChild(proof.previousSibling); + while(node && !isProofEnd(node.textContent)) { + proof.appendChild(node); + node = proof.nextSibling; + } + if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the Qed + if (!hasCommands && proof.nextSibling) proof.appendChild(proof.nextSibling); // the dot after the Qed + + proof.addEventListener("click", function(proof){return function(e){ + if (e.target.parentNode.tagName.toLowerCase() === "a") + return; + proof.setAttribute("show", proof.getAttribute("show") === "true" ? "false" : "true"); + proof.setAttribute("animate", ""); + updateView(); + };}(proof)); + proof.setAttribute("show", "false"); + } + }); +} + +function toggleProofs(){ + var someProofsHidden = proofStatus() === "some-hidden"; + toArray(document.getElementsByClassName("proof")).forEach(function(proof){ + proof.setAttribute("show", someProofsHidden); + proof.setAttribute("animate", ""); + }); + updateView(); +} + +function repairDom(){ + // pull whitespace out of command + toArray(document.getElementsByClassName("command")).forEach(function(node){ + while(node.firstChild && node.firstChild.textContent.trim() == ""){ + console.log("try move"); + node.parentNode.insertBefore(node.firstChild, node); + } + }); + toArray(document.getElementsByClassName("id")).forEach(function(node){ + node.setAttribute("type", node.getAttribute("title")); + }); + toArray(document.getElementsByClassName("idref")).forEach(function(ref){ + toArray(ref.childNodes).forEach(function(child){ + if (["var", "variable"].indexOf(child.getAttribute("type")) > -1) + ref.removeAttribute("href"); + }); + }); + +} + +function fixTitle(){ + var url = "/" + window.location.pathname; + var basename = url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.')); + if (basename === "toc") {document.title = "Table of Contents";} + else if (basename === "indexpage") {document.title = "Index";} + else {document.title = basename;} +} + +function postprocess(){ + repairDom(); + replInTextNodes() + replNodes(); + foldProofs(); + document.getElementById("toggle-proofs").addEventListener("click", toggleProofs); + updateView(); +} + +fixTitle(); +document.addEventListener('DOMContentLoaded', postprocess); + +coqdocjs.toggleProofs = toggleProofs; +})(); diff --git a/theories/Core/Semantic/Domain.v b/theories/Core/Semantic/Domain.v index 5ee3ac7f..2298ae6a 100644 --- a/theories/Core/Semantic/Domain.v +++ b/theories/Core/Semantic/Domain.v @@ -50,7 +50,7 @@ Module Domain_Notations. Notation "'d{{{' x '}}}'" := x (at level 0, x custom domain at level 99, format "'d{{{' x '}}}'") : mcltt_scope. Notation "( x )" := x (in custom domain at level 0, x custom domain at level 60) : mcltt_scope. Notation "~ x" := x (in custom domain at level 0, x constr at level 0) : mcltt_scope. - Notation "x" := x (in custom domain at level 0, x global) : mcltt_scope. + Notation "x" := x (in custom domain at level 0, x ident) : mcltt_scope. Notation "'λ' ρ M" := (d_fn ρ M) (in custom domain at level 0, ρ custom domain at level 30, M custom exp at level 30) : mcltt_scope. Notation "f x .. y" := (d_app .. (d_app f x) .. y) (in custom domain at level 40, f custom domain, x custom domain at next level, y custom domain at next level) : mcltt_scope. Notation "'ℕ'" := d_nat (in custom domain) : mcltt_scope. diff --git a/theories/Core/Syntactic/Syntax.v b/theories/Core/Syntactic/Syntax.v index d2f031e1..826e25b4 100644 --- a/theories/Core/Syntactic/Syntax.v +++ b/theories/Core/Syntactic/Syntax.v @@ -125,7 +125,7 @@ Module Syntax_Notations. Notation "{{{ x }}}" := x (at level 0, x custom exp at level 99, format "'{{{' x '}}}'") : mcltt_scope. Notation "( x )" := x (in custom exp at level 0, x custom exp at level 60) : mcltt_scope. Notation "~ x" := x (in custom exp at level 0, x constr at level 0) : mcltt_scope. - Notation "x" := x (in custom exp at level 0, x global) : mcltt_scope. + Notation "x" := x (in custom exp at level 0, x ident) : mcltt_scope. Notation "e [ s ]" := (a_sub e s) (in custom exp at level 0, s custom exp at level 60) : mcltt_scope. Notation "'λ' A e" := (a_fn A e) (in custom exp at level 0, A custom exp at level 0, e custom exp at level 60) : mcltt_scope. Notation "f x .. y" := (a_app .. (a_app f x) .. y) (in custom exp at level 40, f custom exp, x custom exp at next level, y custom exp at next level) : mcltt_scope. @@ -149,7 +149,7 @@ Module Syntax_Notations. Notation "n{{{ x }}}" := x (at level 0, x custom nf at level 99, format "'n{{{' x '}}}'") : mcltt_scope. Notation "( x )" := x (in custom nf at level 0, x custom nf at level 60) : mcltt_scope. Notation "~ x" := x (in custom nf at level 0, x constr at level 0) : mcltt_scope. - Notation "x" := x (in custom nf at level 0, x global) : mcltt_scope. + Notation "x" := x (in custom nf at level 0, x ident) : mcltt_scope. Notation "'λ' A e" := (nf_fn A e) (in custom nf at level 0, A custom nf at level 0, e custom nf at level 60) : mcltt_scope. Notation "f x .. y" := (ne_app .. (ne_app f x) .. y) (in custom nf at level 40, f custom nf, x custom nf at next level, y custom nf at next level) : mcltt_scope. Notation "'ℕ'" := nf_nat (in custom nf) : mcltt_scope. diff --git a/theories/Makefile b/theories/Makefile index e34b6489..c7a0e827 100644 --- a/theories/Makefile +++ b/theories/Makefile @@ -21,15 +21,10 @@ MENHIR := menhir COQMAKEFILE := CoqMakefile.mk COQPROJECTFILE := _CoqProject -PARSERBASE := parser.ml -POSTPARSERBASE := type_checker.ml -PARSERFILE := ../driver/$(PARSERBASE) -POSTPARSERFILE := ../driver/$(POSTPARSERBASE) -FRONTENDDIR := Frontend -PARSEREXTRACTIONCOQFILE := $(FRONTENDDIR)/ParserExtraction.v -PARSEREXTRACTIONRESULTFILE := $(FRONTENDDIR)/$(PARSERBASE) -POSTPARSEREXTRACTIONCOQFILE := $(FRONTENDDIR)/PostParserExtraction.v -POSTPARSEREXTRACTIONRESULTFILE := $(FRONTENDDIR)/$(POSTPARSERBASE) +PARSERBASE := Parser.ml +POSTPARSERBASE := Entrypoint.ml +PARSERFILE := ../driver/extracted/$(PARSERBASE) +POSTPARSERFILE := ../driver/extracted/$(POSTPARSERBASE) COQPARSERFILE := $(patsubst %.vy,%.v,$(shell find ./ -name '*.vy')) COQFILES := $(sort $(shell find ./ -name '*.v') $(COQPARSERFILE)) @@ -65,3 +60,6 @@ $(COQPROJECTFILE): ; %: $(COQMAKEFILE) force @+$(MAKE) -f "$(COQMAKEFILE)" "$@" + +COQDOCJS_DIR:=../assets/ +include Makefile.doc diff --git a/theories/Makefile.doc b/theories/Makefile.doc new file mode 100644 index 00000000..a93fe5ae --- /dev/null +++ b/theories/Makefile.doc @@ -0,0 +1,19 @@ +COQDOCJS_DIR ?= coqdocjs +EXTRA_DIR = $(COQDOCJS_DIR)/extra +COQDOCFLAGS ?= \ + --toc --toc-depth 2 --html --interpolate \ + --index indexpage --no-lib-name --parse-comments \ + --with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html +export COQDOCFLAGS +COQMAKEFILE ?= Makefile.coq +COQDOCJS_LN ?= false + +coqdoc: $(COQMAKEFILE) + $(MAKE) -f $^ html +ifeq ($(COQDOCJS_LN),true) + ln -sf ../$(EXTRA_DIR)/resources html +else + cp -R $(EXTRA_DIR)/resources html +endif + +.PHONY: coqdoc