Release changes 8.15 (#731)

* coqdocjs * coqdocjs * Release changes (#729) * Set version in opam files * Fix equations dependency * Fix build.yml * Fix opam files and add make-opam-files script * Update version bounds * Back to 8.16.dev versions * Opam make tests (#730) * Make test-suite and examples also installable from the opam package * Test the "with-test" targets of the opam file * Plugin-demo building * Missing MetaCoq prefix in test-suite/plugin * The opam files actually require bash * Missing includes for local build of examples/test-suite * Fix opam build * Fix configure.h Co-authored-by: Yannick Forster <[email protected]>
MetaCoq · Jul 5, 2022 · b9f10e4 · b9f10e4
1 parent f170ec6
commit b9f10e4
Show file tree

Hide file tree

Showing 25 changed files with 593 additions and 41 deletions.
diff --git 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
@@ -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
@@ -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/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
@@ -19,7 +19,7 @@ authors: ["Abhishek Anand <[email protected]>"
 ]
 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
@@ -19,7 +19,7 @@ authors: ["Abhishek Anand <[email protected]>"
 ]
 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
@@ -19,7 +19,7 @@ authors: ["Abhishek Anand <[email protected]>"
 ]
 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
@@ -19,16 +19,17 @@ authors: ["Abhishek Anand <[email protected]>"
 ]
 license: "MIT"
 build: [
-  ["sh" "./configure.sh"]
+  ["bash" "./configure.sh"]
   [make "-j" "%{jobs}%" "template-coq"]
 ]
 install: [
   [make "-C" "template-coq" "install"]
 ]
 depends: [
   "ocaml" {>= "4.07.1"}
-  "coq" { >= "8.15~" & < "8.16~" }
-  "coq-equations" { = "1.3+8.15" }
+  "stdlib-shims"
+  "coq" { >= "8.15" & < "8.16~" }
+  "coq-equations" { >= "1.3" }
 ]
 synopsis: "A quoting and unquoting library for Coq in Coq"
 description: """

diff --git a/coq-metacoq-translations.opam b/coq-metacoq-translations.opam
@@ -19,7 +19,7 @@ authors: ["Abhishek Anand <[email protected]>"
 ]
 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
@@ -26,7 +26,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
@@ -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
diff --git a/examples/_CoqProject.in 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
diff --git a/html/config.js 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
@@ -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;
+}