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 <yannick.forster@inria.fr>

Author: mattam82

.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}}

.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

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:

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

coq-metacoq-erasure.opam

@@ -19,7 +19,7 @@ authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
 ]
 license: "MIT"
 build: [
-  ["sh" "./configure.sh"]
+  ["bash" "./configure.sh"]
   [make "-j" "%{jobs}%" "-C" "erasure"]
 ]
 install: [

coq-metacoq-pcuic.opam

@@ -19,7 +19,7 @@ authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
 ]
 license: "MIT"
 build: [
-  ["sh" "./configure.sh"]
+  ["bash" "./configure.sh"]
   [make "-j" "%{jobs}%" "-C" "pcuic"]
 ]
 install: [

coq-metacoq-safechecker.opam

@@ -19,7 +19,7 @@ authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
 ]
 license: "MIT"
 build: [
-  ["sh" "./configure.sh"]
+  ["bash" "./configure.sh"]
   [make "-j" "%{jobs}%" "-C" "safechecker"]
 ]
 install: [

coq-metacoq-template.opam

@@ -19,16 +19,17 @@ authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
 ]
 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: """

coq-metacoq-translations.opam

@@ -19,7 +19,7 @@ authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
 ]
 license: "MIT"
 build: [
-  ["sh" "./configure.sh"]
+  ["bash" "./configure.sh"]
   [make "-j" "%{jobs}%" "-C" "translations"]
 ]
 install: [

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}
 ]