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 <[email protected]> * Add Kenji to the authors Co-authored-by: Yannick Forster <[email protected]>
MetaCoq · Jul 5, 2022 · c1dae3e · c1dae3e
1 parent 5d2f136
commit c1dae3e
Show file tree

Hide file tree

Showing 27 changed files with 658 additions and 49 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/README.md b/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.

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
@@ -2,21 +2,25 @@ opam-version: "2.0"
 version: "8.14.dev"
 maintainer: "[email protected]"
 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 <[email protected]>"
+          "Danil Annenkov <[email protected]>"
           "Simon Boulier <[email protected]>"
           "Cyril Cohen <[email protected]>"
           "Yannick Forster <[email protected]>"
           "Fabian Kunze <[email protected]>"
+          "Meven Lennon-Bertrand <[email protected]>"
+          "Kenji Maillard <[email protected]>"
           "Gregory Malecha <[email protected]>"
+          "Jakob Botsch Nielsen <[email protected]>"
           "Matthieu Sozeau <[email protected]>"
           "Nicolas Tabareau <[email protected]>"
           "Théo Winterhalter <[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
@@ -2,21 +2,25 @@ opam-version: "2.0"
 version: "8.14.dev"
 maintainer: "[email protected]"
 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 <[email protected]>"
+          "Danil Annenkov <[email protected]>"
           "Simon Boulier <[email protected]>"
           "Cyril Cohen <[email protected]>"
           "Yannick Forster <[email protected]>"
           "Fabian Kunze <[email protected]>"
+          "Meven Lennon-Bertrand <[email protected]>"
+          "Kenji Maillard <[email protected]>"
           "Gregory Malecha <[email protected]>"
+          "Jakob Botsch Nielsen <[email protected]>"
           "Matthieu Sozeau <[email protected]>"
           "Nicolas Tabareau <[email protected]>"
           "Théo Winterhalter <[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
@@ -2,21 +2,25 @@ opam-version: "2.0"
 version: "8.14.dev"
 maintainer: "[email protected]"
 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 <[email protected]>"
+          "Danil Annenkov <[email protected]>"
           "Simon Boulier <[email protected]>"
           "Cyril Cohen <[email protected]>"
           "Yannick Forster <[email protected]>"
           "Fabian Kunze <[email protected]>"
+          "Meven Lennon-Bertrand <[email protected]>"
+          "Kenji Maillard <[email protected]>"
           "Gregory Malecha <[email protected]>"
+          "Jakob Botsch Nielsen <[email protected]>"
           "Matthieu Sozeau <[email protected]>"
           "Nicolas Tabareau <[email protected]>"
           "Théo Winterhalter <[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
@@ -2,28 +2,33 @@ opam-version: "2.0"
 version: "8.14.dev"
 maintainer: "[email protected]"
 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 <[email protected]>"
+          "Danil Annenkov <[email protected]>"
           "Simon Boulier <[email protected]>"
           "Cyril Cohen <[email protected]>"
           "Yannick Forster <[email protected]>"
           "Fabian Kunze <[email protected]>"
+          "Meven Lennon-Bertrand <[email protected]>"
+          "Kenji Maillard <[email protected]>"
           "Gregory Malecha <[email protected]>"
+          "Jakob Botsch Nielsen <[email protected]>"
           "Matthieu Sozeau <[email protected]>"
           "Nicolas Tabareau <[email protected]>"
           "Théo Winterhalter <[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"}
+  "stdlib-shims"
   "coq" { >= "8.14" & < "8.15~" }
   "coq-equations" { >= "1.3" }
 ]

diff --git a/coq-metacoq-translations.opam b/coq-metacoq-translations.opam
@@ -2,17 +2,25 @@ opam-version: "2.0"
 version: "8.14.dev"
 maintainer: "[email protected]"
 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 <[email protected]>"
+authors: ["Abhishek Anand <[email protected]>"
+          "Danil Annenkov <[email protected]>"
+          "Simon Boulier <[email protected]>"
           "Cyril Cohen <[email protected]>"
+          "Yannick Forster <[email protected]>"
+          "Fabian Kunze <[email protected]>"
+          "Meven Lennon-Bertrand <[email protected]>"
+          "Kenji Maillard <[email protected]>"
+          "Gregory Malecha <[email protected]>"
+          "Jakob Botsch Nielsen <[email protected]>"
           "Matthieu Sozeau <[email protected]>"
           "Nicolas Tabareau <[email protected]>"
           "Théo Winterhalter <[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
@@ -2,14 +2,18 @@ opam-version: "2.0"
 version: "8.14.dev"
 maintainer: "[email protected]"
 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 <[email protected]>"
+          "Danil Annenkov <[email protected]>"
           "Simon Boulier <[email protected]>"
           "Cyril Cohen <[email protected]>"
           "Yannick Forster <[email protected]>"
           "Fabian Kunze <[email protected]>"
+          "Meven Lennon-Bertrand <[email protected]>"
+          "Kenji Maillard <[email protected]>"
           "Gregory Malecha <[email protected]>"
+          "Jakob Botsch Nielsen <[email protected]>"
           "Matthieu Sozeau <[email protected]>"
           "Nicolas Tabareau <[email protected]>"
           "Théo Winterhalter <[email protected]>"
@@ -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
@@ -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