PCUIC PHOAS

.github/workflows/build.yml

@@ -3,16 +3,26 @@ name: MetaCoq CI
 on: [push, pull_request]
 
 jobs:
+  checktodos:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v2
+        with:
+          fetch-depth: 1
+
+      - name: Check for todos
+        run: ./checktodos.sh
+
   build:
     runs-on: ubuntu-latest
 
     strategy:
       matrix:
         coq_version: 
-          - '8.14'
+          - '8.16'
         ocaml_version:
-          - '4.07-flambda'
-          - '4.12-flambda'
+          - '4.14-flambda'
         target: [ local, opam, quick ]
       fail-fast: true
 
@@ -33,6 +43,12 @@ 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
+              opam pin -n coq-equations http://github.com/mattam82/Coq-Equations.git#8.16
+              opam install --confirm-level=unsafe-yes coq-equations.8.16.dev
+            endGroup
           script: |
             startGroup "Build project"
               opam exec -- ./configure.sh --enable-${{matrix.target}}

.gitignore

@@ -352,3 +352,6 @@ 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

.vscode/tasks.json

@@ -7,7 +7,11 @@
             "label": "make",
             "type": "shell",
             "command": "make",
-            "problemMatcher": []
+            "problemMatcher": [],
+            "group": {
+                "kind": "build",
+                "isDefault": true
+            },
         },
         {
             "label": "makevos",
@@ -17,8 +21,7 @@
             },
             "command": "opam exec -- make -f Makefile.pcuic vos",
             "group": {
-                "kind": "build",
-                "isDefault": true
+                "kind": "build"
             },
             "problemMatcher": []
         }

INSTALL.md

@@ -72,12 +72,12 @@ To setup a fresh `opam` installation, you might want to create a
 one yet. You need to use **opam 2** to obtain the right version of
 `Equations`.
 
-    # opam switch create coq.8.14 4.07.1
+    # opam switch create coq.8.16 --packages=ocaml-variants.4.13.1+options,ocaml-option-flambda
     # eval $(opam env)
 
-This creates the `coq.8.14` switch which initially contains only the
-basic `OCaml` `4.07.1` compiler, and puts you in the right environment
-(check with `ocamlc -v`).
+This creates the `coq.8.16` switch which initially contains only the
+basic `OCaml` `4.13.1` compiler with the `flambda` option enabled,
+and puts you in the right environment (check with `ocamlc -v`).
 
 Once in the right switch, you can install `Coq` and the `Equations` package using:
 

Makefile

@@ -1,8 +1,32 @@
-TIMED ?=
 
 all: template-coq pcuic safechecker erasure examples test-suite translations
 
-.PHONY: all template-coq pcuic erasure install html clean mrproper .merlin test-suite translations
+-include Makefile.conf
+
+ifeq '$(METACOQ_CONFIG)' 'local'
+  ifeq ($(shell which cygpath 2>/dev/null),)
+  OCAMLPATH := $(shell pwd)/template-coq/:$(OCAMLPATH)
+  else
+  OCAMLPATH := $(shell cygpath -m `pwd`)/template-coq/;$(OCAMLPATH)
+  endif
+  export OCAMLPATH
+endif
+
+all: printconf template-coq pcuic safechecker erasure examples
+
+.PHONY: printconf all template-coq pcuic erasure install html clean mrproper .merlin test-suite translations
+
+printconf:
+ifeq '$(METACOQ_CONFIG)' 'local'
+	@echo "Local configuration"
+else
+ifeq '$(METACOQ_CONFIG)' 'global'
+	@echo "Global configuration"
+else
+	@echo "Run ./configure.sh first"
+	@exit 1
+endif
+endif
 
 install: all translations
 	$(MAKE) -C template-coq install
@@ -95,7 +119,7 @@ ci-local-noclean:
 	./configure.sh local
 	$(MAKE) all test-suite TIMED=pretty-timed
 
-ci-local: ci-local-noclean
+ci-local: ci-local-noclean 
 	$(MAKE) clean
 
 ci-quick:
@@ -106,3 +130,6 @@ ci-opam:
 # Use -v so that regular output is produced
 	opam install -v -y .
 	opam remove -y coq-metacoq coq-metacoq-template
+
+checktodos:
+	sh checktodos.sh