diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 892463022..0bdc4760b 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -48,6 +48,10 @@ jobs: sudo chown -R coq:coq . # <-- opam exec -- ocamlfind list endGroup + before_install: | + startGroup "Print opam config" + opam config list; opam repo list; opam list + endGroup script: | startGroup "Build project" opam exec -- ./configure.sh --enable-${{matrix.target}} diff --git a/.gitignore b/.gitignore index 929b11a50..a2a268cfe 100644 --- a/.gitignore +++ b/.gitignore @@ -352,3 +352,13 @@ erasure/src/eEnvMap.ml erasure/src/eEnvMap.mli erasure/src/eGlobalEnv.mli erasure/src/eGlobalEnv.ml +Makefile.conf +test-suite/plugin-demo/src/META.coq-metacoq-demo-plugin +pcuic/src/META.coq-metacoq-pcuic +examples/_CoqProject +test-suite/_CoqProject +examples/metacoq-config +test-suite/metacoq-config +test-suite/plugin-demo/_CoqProject +test-suite/plugin-demo/_PluginProject +test-suite/plugin-demo/metacoq-config diff --git a/Makefile b/Makefile index 46150a69e..2af775929 100644 --- a/Makefile +++ b/Makefile @@ -19,7 +19,8 @@ uninstall: all $(MAKE) -C translations uninstall html: all - "coqdoc" -toc -utf8 -interpolate -l -html \ + "coqdoc" --multi-index -toc -utf8 -interpolate -html \ + --with-header ./html/resources/header.html --with-footer ./html/resources/footer.html \ -R template-coq/theories MetaCoq.Template \ -R pcuic/theories MetaCoq.PCUIC \ -R safechecker/theories MetaCoq.SafeChecker \ @@ -104,7 +105,7 @@ ci-quick: ci-opam: # Use -v so that regular output is produced - opam install -v -y . + opam install --with-test -v -y . opam remove -y coq-metacoq coq-metacoq-template checktodos: diff --git a/README.md b/README.md index 827c22e03..50d79f3b4 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,8 @@

[![Build status](https://github.com/MetaCoq/metacoq/actions/workflows/build.yml/badge.svg?branch=coq-8.14)](https://github.com/MetaCoq/metacoq/actions) [![MetaCoq Chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://coq.zulipchat.com) -[![Open in Visual Studio Code](https://open.vscode.dev/badges/open-in-vscode.svg)](https://open.vscode.dev/metacoq/metacoq) +[![Open in Visual Studio Code](https://img.shields.io/static/v1?logo=visualstudiocode&label=&message=Open%20in%20Visual%20Studio%20Code&labelColor=2c2c32&color=007acc&logoColor=007acc +)](https://open.vscode.dev/metacoq/metacoq) MetaCoq is a project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins @@ -250,14 +251,17 @@ alt="Yannick Forster" width="150px"/> src="https://github.com/MetaCoq/metacoq.github.io/raw/master/assets/meven-lennon-bertrand.jpeg" alt="Meven Lennon-Bertrand" width="150px"/>
+Gregory Malecha +alt="Jakob Botsch Nielsen" width="150px"/>

+alt="Matthieu Sozeau" width="150px"/> Nicolas Tabareau @@ -274,6 +278,7 @@ MetaCoq is developed by (left to right) Cyril Cohen, Yannick Forster, Meven Lennon-Bertrand, +Kenji Maillard, Gregory Malecha, Jakob Botsch Nielsen, Matthieu Sozeau, @@ -288,6 +293,7 @@ Copyright (c) 2015-2022 Abhishek Anand, Matthieu Sozeau Copyright (c) 2017-2022 Simon Boulier, Nicolas Tabareau, Cyril Cohen Copyright (c) 2018-2022 Danil Annenkov, Yannick Forster, Théo Winterhalter Copyright (c) 2020-2022 Jakob Botsch Nielsen, Meven Lennon-Bertrand +Copyright (c) 2022 Kenji Maillard ``` This software is distributed under the terms of the MIT license. diff --git a/configure.sh b/configure.sh index b4958ed29..b3cd7648e 100755 --- a/configure.sh +++ b/configure.sh @@ -21,6 +21,10 @@ then SAFECHECKER_DEPS="-R ../pcuic/theories MetaCoq.PCUIC" ERASURE_DEPS="-R ../safechecker/theories MetaCoq.SafeChecker" TRANSLATIONS_DEPS="" + EXAMPLES_DEPS="-I ../safechecker/src -I ../erasure/src -R ../erasure/theories MetaCoq.Erasure" + TEST_SUITE_DEPS="-I ../safechecker/src -I ../erasure/src -R ../erasure/theories MetaCoq.Erasure" + PLUGIN_DEMO_DEPS="-I ../../template-coq/build -R ../../template-coq/theories MetaCoq.Template -I ../../template-coq/" + echo "METACOQ_CONFIG = local" > Makefile.conf else echo "Building MetaCoq globally (default)" # The safechecker and erasure plugins depend on the extractable template-coq plugin @@ -30,17 +34,28 @@ then SAFECHECKER_DEPS="" ERASURE_DEPS="" TRANSLATIONS_DEPS="" + EXAMPLES_DEPS="" + TEST_SUITE_DEPS="" + PLUGIN_DEMO_DEPS="-I ${COQLIB}/user-contrib/MetaCoq/Template" + echo "METACOQ_CONFIG = global" > Makefile.conf fi echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > pcuic/metacoq-config echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > safechecker/metacoq-config echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > erasure/metacoq-config echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > translations/metacoq-config + echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > examples/metacoq-config + echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > test-suite/metacoq-config + echo "# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh" > test-suite/plugin-demo/metacoq-config echo ${PCUIC_DEPS} >> pcuic/metacoq-config echo ${PCUIC_DEPS} ${SAFECHECKER_DEPS} >> safechecker/metacoq-config echo ${PCUIC_DEPS} ${SAFECHECKER_DEPS} ${ERASURE_DEPS} >> erasure/metacoq-config echo ${PCUIC_DEPS} ${TRANSLATIONS_DEPS} >> translations/metacoq-config + echo ${PCUIC_DEPS} ${SAFECHECKER_DEPS} ${ERASURE_DEPS} ${TRANSLATIONS_DEPS} ${EXAMPLES_DEPS} >> examples/metacoq-config + echo ${PCUIC_DEPS} ${SAFECHECKER_DEPS} ${ERASURE_DEPS} ${TRANSLATIONS_DEPS} ${TEST_SUITE_DEPS} >> test-suite/metacoq-config + echo ${PLUGIN_DEMO_DEPS} >> test-suite/plugin-demo/metacoq-config + else echo "Error: coqc not found in path" fi diff --git a/coq-metacoq-erasure.opam b/coq-metacoq-erasure.opam index 88a9ead2e..fbcee6e11 100644 --- a/coq-metacoq-erasure.opam +++ b/coq-metacoq-erasure.opam @@ -2,21 +2,25 @@ opam-version: "2.0" version: "8.14.dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" bug-reports: "https://github.com/MetaCoq/metacoq/issues" authors: ["Abhishek Anand " + "Danil Annenkov " "Simon Boulier " "Cyril Cohen " "Yannick Forster " "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " "Gregory Malecha " + "Jakob Botsch Nielsen " "Matthieu Sozeau " "Nicolas Tabareau " "Théo Winterhalter " ] license: "MIT" build: [ - ["sh" "./configure.sh"] + ["bash" "./configure.sh"] [make "-j" "%{jobs}%" "-C" "erasure"] ] install: [ diff --git a/coq-metacoq-pcuic.opam b/coq-metacoq-pcuic.opam index 42bf1a8e7..79e5cc294 100644 --- a/coq-metacoq-pcuic.opam +++ b/coq-metacoq-pcuic.opam @@ -2,21 +2,25 @@ opam-version: "2.0" version: "8.14.dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" bug-reports: "https://github.com/MetaCoq/metacoq/issues" authors: ["Abhishek Anand " + "Danil Annenkov " "Simon Boulier " "Cyril Cohen " "Yannick Forster " "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " "Gregory Malecha " + "Jakob Botsch Nielsen " "Matthieu Sozeau " "Nicolas Tabareau " "Théo Winterhalter " ] license: "MIT" build: [ - ["sh" "./configure.sh"] + ["bash" "./configure.sh"] [make "-j" "%{jobs}%" "-C" "pcuic"] ] install: [ diff --git a/coq-metacoq-safechecker.opam b/coq-metacoq-safechecker.opam index 5105bdc62..7f14c2b92 100644 --- a/coq-metacoq-safechecker.opam +++ b/coq-metacoq-safechecker.opam @@ -2,21 +2,25 @@ opam-version: "2.0" version: "8.14.dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" bug-reports: "https://github.com/MetaCoq/metacoq/issues" authors: ["Abhishek Anand " + "Danil Annenkov " "Simon Boulier " "Cyril Cohen " "Yannick Forster " "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " "Gregory Malecha " + "Jakob Botsch Nielsen " "Matthieu Sozeau " "Nicolas Tabareau " "Théo Winterhalter " ] license: "MIT" build: [ - ["sh" "./configure.sh"] + ["bash" "./configure.sh"] [make "-j" "%{jobs}%" "-C" "safechecker"] ] install: [ diff --git a/coq-metacoq-template.opam b/coq-metacoq-template.opam index e62a818b2..20d2926c0 100644 --- a/coq-metacoq-template.opam +++ b/coq-metacoq-template.opam @@ -2,21 +2,25 @@ opam-version: "2.0" version: "8.14.dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#master" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" bug-reports: "https://github.com/MetaCoq/metacoq/issues" authors: ["Abhishek Anand " + "Danil Annenkov " "Simon Boulier " "Cyril Cohen " "Yannick Forster " "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " "Gregory Malecha " + "Jakob Botsch Nielsen " "Matthieu Sozeau " "Nicolas Tabareau " "Théo Winterhalter " ] license: "MIT" build: [ - ["sh" "./configure.sh"] + ["bash" "./configure.sh"] [make "-j" "%{jobs}%" "template-coq"] ] install: [ @@ -24,6 +28,7 @@ install: [ ] depends: [ "ocaml" {>= "4.07.1"} + "stdlib-shims" "coq" { >= "8.14" & < "8.15~" } "coq-equations" { >= "1.3" } ] diff --git a/coq-metacoq-translations.opam b/coq-metacoq-translations.opam index 3fcbaa469..d40935aea 100644 --- a/coq-metacoq-translations.opam +++ b/coq-metacoq-translations.opam @@ -2,17 +2,25 @@ opam-version: "2.0" version: "8.14.dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" bug-reports: "https://github.com/MetaCoq/metacoq/issues" -authors: ["Simon Boulier " +authors: ["Abhishek Anand " + "Danil Annenkov " + "Simon Boulier " "Cyril Cohen " + "Yannick Forster " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " "Matthieu Sozeau " "Nicolas Tabareau " "Théo Winterhalter " ] license: "MIT" build: [ - ["sh" "./configure.sh"] + ["bash" "./configure.sh"] [make "-j" "%{jobs}%" "-C" "translations"] ] install: [ diff --git a/coq-metacoq.opam b/coq-metacoq.opam index 8df96a6af..60cc1971d 100644 --- a/coq-metacoq.opam +++ b/coq-metacoq.opam @@ -2,14 +2,18 @@ opam-version: "2.0" version: "8.14.dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" bug-reports: "https://github.com/MetaCoq/metacoq/issues" authors: ["Abhishek Anand " + "Danil Annenkov " "Simon Boulier " "Cyril Cohen " "Yannick Forster " "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " "Gregory Malecha " + "Jakob Botsch Nielsen " "Matthieu Sozeau " "Nicolas Tabareau " "Théo Winterhalter " @@ -23,7 +27,7 @@ depends: [ "coq-metacoq-translations" {= version} ] build: [ - ["sh" "./configure.sh" ] {with-test} + ["bash" "./configure.sh" ] {with-test} [make "-C" "examples" ] {with-test} [make "-C" "test-suite" ] {with-test} ] diff --git a/examples/Makefile b/examples/Makefile index aef42de36..73691022f 100644 --- a/examples/Makefile +++ b/examples/Makefile @@ -3,9 +3,13 @@ all: examples examples: Makefile.coq $(MAKE) -f Makefile.coq TIMED=$(TIMED) -Makefile.coq: Makefile +Makefile.coq: Makefile _CoqProject coq_makefile -f _CoqProject -o Makefile.coq +_CoqProject: _CoqProject.in metacoq-config + cat metacoq-config > _CoqProject + cat _CoqProject.in >> _CoqProject + clean: Makefile.coq $(MAKE) -f Makefile.coq clean diff --git a/examples/_CoqProject b/examples/_CoqProject deleted file mode 100644 index a4603b8bf..000000000 --- a/examples/_CoqProject +++ /dev/null @@ -1,16 +0,0 @@ --I ../template-coq/build --I ../safechecker/src --I ../erasure/src --Q ../template-coq/theories MetaCoq.Template --Q ../pcuic/theories MetaCoq.PCUIC --Q ../safechecker/theories MetaCoq.SafeChecker --Q ../erasure/theories MetaCoq.Erasure --R . MetaCoq.Examples - -demo.v -constructor_tac.v -add_constructor.v -tauto.v -typing_correctness.v -metacoq_tour_prelude.v -metacoq_tour.v \ No newline at end of file diff --git a/examples/_CoqProject.in b/examples/_CoqProject.in new file mode 100644 index 000000000..c5492b0c2 --- /dev/null +++ b/examples/_CoqProject.in @@ -0,0 +1,9 @@ +-R . MetaCoq.Examples + +demo.v +constructor_tac.v +add_constructor.v +tauto.v +typing_correctness.v +metacoq_tour_prelude.v +metacoq_tour.v \ No newline at end of file diff --git a/html/config.js b/html/config.js new file mode 100644 index 000000000..211cbb228 --- /dev/null +++ b/html/config.js @@ -0,0 +1,72 @@ +var coqdocjs = coqdocjs || {}; + +coqdocjs.repl = { + "fun": "λ", + "forall": "∀", + "exists": "∃", + "~": "¬", + "/\\": "∧", + "\\/": "∨", + "->": "→", + "<-": "←", + "<->": "↔", + "=>": "⇒", + "<>": "≠", + "<=": "≤", + ">=": "≥", + "el": "∈", + "nel": "∉", + "<<=": "⊆", + "<<": "⊂", + "|-": "⊢", + "++": "⧺", + "===": "≡", + "=/=": "≢", + "=~=": "≅", + "==>": "⟹", + "lhd": "⊲", + "rhd": "⊳", + "nat": "ℕ", + "alpha": "α", + "beta": "β", + "gamma": "γ", + "delta": "δ", + "epsilon": "ε", + "eta": "η", + "iota": "ι", + "kappa": "κ", + "lambda": "λ", + "mu": "μ", + "nu": "ν", + "lia": "ω", + "phi": "ϕ", + "pi": "π", + "psi": "ψ", + "rho": "ρ", + "sigma": "σ", + "tau": "τ", + "theta": "θ", + "xi": "ξ", + "zeta": "ζ", + "Delta": "Δ", + "Gamma": "Γ", + "Pi": "Π", + "Sigma": "Σ", + "Lia": "Ω", + "Xi": "Ξ" +}; + +coqdocjs.subscr = { + "0" : "₀", + "1" : "₁", + "2" : "₂", + "3" : "₃", + "4" : "₄", + "5" : "₅", + "6" : "₆", + "7" : "₇", + "8" : "₈", + "9" : "₉", +}; + +coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="]; diff --git a/html/coqdoc.css b/html/coqdoc.css index dbc930f5e..48096e555 100644 --- a/html/coqdoc.css +++ b/html/coqdoc.css @@ -230,6 +230,10 @@ tr.infrulemiddle hr { color: rgb(40%,0%,40%); } +.id[title="binder"] { + color: rgb(40%,0%,40%); +} + .id[type="definition"] { color: rgb(0%,40%,0%); } @@ -327,3 +331,8 @@ ul.doclist { margin-top: 0em; margin-bottom: 0em; } + +.code :target { + border: 2px solid #D4D4D4; + background-color: #e5eecc; +} diff --git a/html/coqdocjs.css b/html/coqdocjs.css new file mode 100644 index 000000000..575fc3dd0 --- /dev/null +++ b/html/coqdocjs.css @@ -0,0 +1,224 @@ +/* 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; +} + +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; +} diff --git a/html/coqdocjs.js b/html/coqdocjs.js new file mode 100644 index 000000000..1a0b066d3 --- /dev/null +++ b/html/coqdocjs.js @@ -0,0 +1,184 @@ +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){return coqdocjs.subscr[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(s){ + return isVernacStart(["Proof"], s); +} + +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.textContent)) { + 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 modulename = "." + url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.')); + modulename = modulename.substring(modulename.lastIndexOf('.')+1); + if (modulename === "toc") {modulename = "Table of Contents";} + else if (modulename === "indexpage") {modulename = "Index";} + else {modulename = modulename + ".v";}; + document.title = modulename; +} + +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/html/resources/footer.html b/html/resources/footer.html new file mode 100644 index 000000000..d0f79a884 --- /dev/null +++ b/html/resources/footer.html @@ -0,0 +1,8 @@ + + + + + + diff --git a/html/resources/header.html b/html/resources/header.html new file mode 100644 index 000000000..cc81721b4 --- /dev/null +++ b/html/resources/header.html @@ -0,0 +1,27 @@ + + + + + + + + + + + + + +
+
diff --git a/make-opam-files.sh b/make-opam-files.sh new file mode 100755 index 000000000..be6bb62a5 --- /dev/null +++ b/make-opam-files.sh @@ -0,0 +1,23 @@ +#/usr/bin/env bash +echo "Target directory: " $1 +echo "Target version: " $2 +echo "Releases package: " $3 + +wget $3 +archive=`basename $3` +hash=`shasum -a 512 $archive | cut -f 1 -d " "` + +echo "Shasum = " $hash + +for f in *.opam; +do + opamf=${f/.opam/}; + target=$1/$opamf/$opamf.$2/opam; + echo $opamf; + mkdir $1/$opamf/$opamf.$2 + gsed -e "/^version:.*/d" $f > $target + echo url { >> $target + echo " src:" \"$3\" >> $target + echo " checksum:" \"sha512=$hash\" >> $target + echo } >> $target +done \ No newline at end of file diff --git a/test-suite/Makefile b/test-suite/Makefile index 93168ec11..a6cf61b73 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -5,9 +5,13 @@ all: bugs plugin-demo bugs: Makefile.coq $(MAKE) -f Makefile.coq TIMED=$(TIMED) -Makefile.coq: Makefile +Makefile.coq: Makefile _CoqProject coq_makefile -f _CoqProject -o Makefile.coq +_CoqProject: _CoqProject.in metacoq-config + cat metacoq-config > _CoqProject + cat _CoqProject.in >> _CoqProject + clean: Makefile.coq $(MAKE) -f Makefile.coq clean diff --git a/test-suite/_CoqProject b/test-suite/_CoqProject.in similarity index 69% rename from test-suite/_CoqProject rename to test-suite/_CoqProject.in index fb11b1fcd..cf3edbec7 100644 --- a/test-suite/_CoqProject +++ b/test-suite/_CoqProject.in @@ -1,10 +1,3 @@ --I ../template-coq/build --I ../safechecker/src --I ../erasure/src --Q ../template-coq/theories MetaCoq.Template --Q ../pcuic/theories MetaCoq.PCUIC --Q ../safechecker/theories MetaCoq.SafeChecker --Q ../erasure/theories MetaCoq.Erasure -R . MetaCoq.TestSuite # list obtained with `ls -1 *.v` diff --git a/test-suite/plugin-demo/Makefile b/test-suite/plugin-demo/Makefile index 42c55bbfd..3f53a81b6 100644 --- a/test-suite/plugin-demo/Makefile +++ b/test-suite/plugin-demo/Makefile @@ -10,6 +10,14 @@ Makefile.coq: _CoqProject Makefile.plugin: _PluginProject coq_makefile -f _PluginProject -o Makefile.plugin +_CoqProject: _CoqProject.in metacoq-config + cat metacoq-config > _CoqProject + cat _CoqProject.in >> _CoqProject + +_PluginProject: _PluginProject.in metacoq-config + cat metacoq-config > _PluginProject + cat _PluginProject.in >> _PluginProject + plugin: Makefile.plugin coq $(MAKE) -f Makefile.plugin diff --git a/test-suite/plugin-demo/_CoqProject b/test-suite/plugin-demo/_CoqProject.in similarity index 56% rename from test-suite/plugin-demo/_CoqProject rename to test-suite/plugin-demo/_CoqProject.in index 43ff5b807..d7dac400e 100644 --- a/test-suite/plugin-demo/_CoqProject +++ b/test-suite/plugin-demo/_CoqProject.in @@ -1,5 +1,3 @@ --R ../../template-coq/theories MetaCoq.Template --I ../../template-coq/build -R theories MetaCoq.ExtractedPluginDemo theories/Lens.v diff --git a/test-suite/plugin-demo/_PluginProject b/test-suite/plugin-demo/_PluginProject.in similarity index 76% rename from test-suite/plugin-demo/_PluginProject rename to test-suite/plugin-demo/_PluginProject.in index 29f6938f7..d72a39bd2 100644 --- a/test-suite/plugin-demo/_PluginProject +++ b/test-suite/plugin-demo/_PluginProject.in @@ -1,6 +1,3 @@ --R ../../template-coq/theories MetaCoq.Template --I ../../template-coq/build - -I src -I gen-src -R theories MetaCoq.ExtractedPluginDemo diff --git a/test-suite/plugin-demo/theories/Extraction.v b/test-suite/plugin-demo/theories/Extraction.v index 0179c5072..d173847b5 100644 --- a/test-suite/plugin-demo/theories/Extraction.v +++ b/test-suite/plugin-demo/theories/Extraction.v @@ -1,4 +1,4 @@ -Require Import Template.Extraction. +From MetaCoq Require Import Template.Extraction. Require Import Lens MyPlugin. Cd "gen-src".