Opam make tests

.gitignore

@@ -355,3 +355,10 @@ 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

@@ -130,7 +130,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,25 +21,38 @@ then
         SAFECHECKER_DEPS="-R ../pcuic/theories MetaCoq.PCUIC"
         ERASURE_DEPS="-R ../safechecker/theories MetaCoq.SafeChecker"
         TRANSLATIONS_DEPS=""
+        EXAMPLES_DEPS="-R ../erasure/theories MetaCoq.Erasure"
+        TEST_SUITE_DEPS="-R ../erasure/theories MetaCoq.Erasure"
+        PLUGIN_DEMO_DEPS="-R ../../template-coq/theories MetaCoq.Template -I ../../template-coq/"
         echo "METACOQ_CONFIG = local" > Makefile.conf
     else
         echo "Building MetaCoq globally (default)"
         PCUIC_DEPS=""
         SAFECHECKER_DEPS=""
         ERASURE_DEPS=""
         TRANSLATIONS_DEPS=""
+        EXAMPLES_DEPS=""
+        TEST_SUITE_DEPS=""
+        PLUGIN_DEMO_DEPS=""
         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 <[email protected]>"
 ]
 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 <[email protected]>"
 ]
 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 <[email protected]>"
 ]
 license: "MIT"
 build: [
-  ["sh" "./configure.sh"]
+  ["bash" "./configure.sh"]
   [make "-j" "%{jobs}%" "-C" "safechecker"]
 ]
 install: [

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: [

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

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
 

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

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
 

test-suite/_CoqProject → test-suite/_CoqProject.in

@@ -1,7 +1,3 @@
--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`

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
 

test-suite/plugin-demo/_CoqProject → test-suite/plugin-demo/_CoqProject.in

@@ -1,7 +1,4 @@
 META.coq-metacoq-demo-plugin
--R ../../template-coq/theories MetaCoq.Template
--I ../../template-coq/build
--I ../../template-coq/
 -R theories MetaCoq.ExtractedPluginDemo
 
 theories/Lens.v

test-suite/plugin-demo/_PluginProject → test-suite/plugin-demo/_PluginProject.in

@@ -1,6 +1,4 @@
 -generate-meta-for-package coq-metacoq-demo-plugin
--R ../../template-coq/theories MetaCoq.Template
--I ../../template-coq/
 
 -I src
 -I gen-src

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.
 
 Set Warnings "-extraction-opaque-accessed".