Release changes 8.14 (#732)

* Fix opam files and add make-opam-files script

* Update authors

* 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>

* Add Kenji to the authors

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:

README.md

@@ -5,7 +5,8 @@
 </p>
 
 [![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"/><br/>
 <img
+src="https://github.com/MetaCoq/metacoq.github.io/raw/master/assets/kenji-maillard.jpg"
+alt="Kenji Maillard" width="150px"/>
+<img
 src="https://github.com/MetaCoq/metacoq.github.io/raw/master/assets/gregory-malecha.jpg"
 alt="Gregory Malecha" width="150px"/>
 <img
 src="https://github.com/MetaCoq/metacoq.github.io/raw/master/assets/jakob-botsch-nielsen.png"
-alt="Jakob Botsch Nielsen" width="150px"/>
+alt="Jakob Botsch Nielsen" width="150px"/><br/>
 <img
 src="https://github.com/MetaCoq/metacoq.github.io/raw/master/assets/matthieu-sozeau.png"
-alt="Matthieu Sozeau" width="150px"/><br/>
+alt="Matthieu Sozeau" width="150px"/>
 <img
 src="https://github.com/MetaCoq/metacoq.github.io/raw/master/assets/nicolas-tabareau.jpg"
 alt="Nicolas Tabareau" width="150px"/>
@@ -274,6 +278,7 @@ MetaCoq is developed by (left to right)
 <a href="https://github.com/CohenCyril">Cyril Cohen</a>,
 <a href="https://github.com/yforster">Yannick Forster</a>,
 <a href="https://www.meven.ac">Meven Lennon-Bertrand</a>,
+<a href="https://github.com/kyoDralliam">Kenji Maillard</a>,
 <a href="https://github.com/gmalecha">Gregory Malecha</a>,
 <a href="https://github.com/jakobbotsch">Jakob Botsch Nielsen</a>,
 <a href="https://github.com/mattam82">Matthieu Sozeau</a>,
@@ -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.

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

@@ -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 <aa755@cs.cornell.edu>"
+          "Danil Annenkov <danil.v.annenkov@gmail.com>"
           "Simon Boulier <simon.boulier@inria.fr>"
           "Cyril Cohen <cyril.cohen@inria.fr>"
           "Yannick Forster <forster@ps.uni-saarland.de>"
           "Fabian Kunze <fkunze@fakusb.de>"
+          "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
+          "Kenji Maillard <kenji.maillard@inria.fr>"
           "Gregory Malecha <gmalecha@gmail.com>"
+          "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>"
           "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
           "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
           "Théo Winterhalter <theo.winterhalter@inria.fr>"
 ]
 license: "MIT"
 build: [
-  ["sh" "./configure.sh"]
+  ["bash" "./configure.sh"]
   [make "-j" "%{jobs}%" "-C" "erasure"]
 ]
 install: [

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 <aa755@cs.cornell.edu>"
+          "Danil Annenkov <danil.v.annenkov@gmail.com>"
           "Simon Boulier <simon.boulier@inria.fr>"
           "Cyril Cohen <cyril.cohen@inria.fr>"
           "Yannick Forster <forster@ps.uni-saarland.de>"
           "Fabian Kunze <fkunze@fakusb.de>"
+          "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
+          "Kenji Maillard <kenji.maillard@inria.fr>"
           "Gregory Malecha <gmalecha@gmail.com>"
+          "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>"
           "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
           "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
           "Théo Winterhalter <theo.winterhalter@inria.fr>"
 ]
 license: "MIT"
 build: [
-  ["sh" "./configure.sh"]
+  ["bash" "./configure.sh"]
   [make "-j" "%{jobs}%" "-C" "pcuic"]
 ]
 install: [

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 <aa755@cs.cornell.edu>"
+          "Danil Annenkov <danil.v.annenkov@gmail.com>"
           "Simon Boulier <simon.boulier@inria.fr>"
           "Cyril Cohen <cyril.cohen@inria.fr>"
           "Yannick Forster <forster@ps.uni-saarland.de>"
           "Fabian Kunze <fkunze@fakusb.de>"
+          "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
+          "Kenji Maillard <kenji.maillard@inria.fr>"
           "Gregory Malecha <gmalecha@gmail.com>"
+          "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>"
           "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
           "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
           "Théo Winterhalter <theo.winterhalter@inria.fr>"
 ]
 license: "MIT"
 build: [
-  ["sh" "./configure.sh"]
+  ["bash" "./configure.sh"]
   [make "-j" "%{jobs}%" "-C" "safechecker"]
 ]
 install: [

coq-metacoq-template.opam

@@ -2,28 +2,33 @@ 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 <aa755@cs.cornell.edu>"
+          "Danil Annenkov <danil.v.annenkov@gmail.com>"
           "Simon Boulier <simon.boulier@inria.fr>"
           "Cyril Cohen <cyril.cohen@inria.fr>"
           "Yannick Forster <forster@ps.uni-saarland.de>"
           "Fabian Kunze <fkunze@fakusb.de>"
+          "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
+          "Kenji Maillard <kenji.maillard@inria.fr>"
           "Gregory Malecha <gmalecha@gmail.com>"
+          "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>"
           "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
           "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
           "Théo Winterhalter <theo.winterhalter@inria.fr>"
 ]
 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"}
+  "stdlib-shims"
   "coq" { >= "8.14" & < "8.15~" }
   "coq-equations" { >= "1.3" }
 ]

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 <simon.boulier@inria.fr>"
+authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
+          "Danil Annenkov <danil.v.annenkov@gmail.com>"
+          "Simon Boulier <simon.boulier@inria.fr>"
           "Cyril Cohen <cyril.cohen@inria.fr>"
+          "Yannick Forster <forster@ps.uni-saarland.de>"
+          "Fabian Kunze <fkunze@fakusb.de>"
+          "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
+          "Kenji Maillard <kenji.maillard@inria.fr>"
+          "Gregory Malecha <gmalecha@gmail.com>"
+          "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>"
           "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
           "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
           "Théo Winterhalter <theo.winterhalter@inria.fr>"
 ]
 license: "MIT"
 build: [
-  ["sh" "./configure.sh"]
+  ["bash" "./configure.sh"]
   [make "-j" "%{jobs}%" "-C" "translations"]
 ]
 install: [