Merge pull request LPCIC#368 from LPCIC/coq-8.16

master on 8.16

.github/workflows/doc.yml

@@ -22,7 +22,7 @@ jobs:
     - name: setup ocaml
       uses: avsm/setup-ocaml@v1
       with:
-        ocaml-version: 4.07.1
+        ocaml-version: 4.09.1
 
     - name: install deps
       run: |

.github/workflows/main.yml

@@ -16,9 +16,9 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.15'
+          - '8.16'
         ocaml_version:
-          - '4.07-flambda'
+          - '4.09-flambda'
           - '4.13-flambda'
     steps:
     - uses: actions/checkout@v2
@@ -28,5 +28,11 @@ jobs:
         coq_version: ${{ matrix.coq_version }}
         ocaml_version: ${{ matrix.ocaml_version }}
         export: 'OPAMWITHTEST'
+        install: |
+          startGroup "Install dependencies"
+            opam pin add -n -y -k path $PACKAGE $WORKDIR
+            opam update -y
+            opam install -y -j 2 $PACKAGE --deps-only
+          endGroup
       env:
         OPAMWITHTEST: 'true'

.nix/config.nix

@@ -31,21 +31,31 @@
 
   ## select an entry to build in the following `bundles` set
   ## defaults to "default"
-  default-bundle = "default";
+  default-bundle = "master";
 
   ## write one `bundles.name` attribute set per
   ## alternative configuration
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
-  bundles.default = {
 
-    ## You can override Coq and other Coq coqPackages
-    ## through the following attribute
-    coqPackages.coq.override.version = "8.15";
-    coqPackages.hierarchy-builder.override.version = "master";
-    coqPackages.graph-theory.override.version = "master";
-    coqPackages.mathcomp-analysis.override.version = "master";
-
+  bundles = {
+    master = {
+      coqPackages.coq.override.version = "master";
+      coqPackages.hierarchy-builder.override.version = "master";
+      coqPackages.graph-theory.override.version = "master";
+      coqPackages.mathcomp-analysis.override.version = "master";
+    };
+
+    "8.15" = {
+
+      ## You can override Coq and other Coq coqPackages
+      ## through the following attribute
+      coqPackages.coq.override.version = "8.15";
+      coqPackages.hierarchy-builder.override.version = "master";
+      coqPackages.graph-theory.override.version = "master";
+      coqPackages.mathcomp-analysis.override.version = "master";
+    };
+
     ## In some cases, light overrides are not available/enough
     ## in which case you can use either
     # coqPackages.<coq-pkg>.overrideAttrs = o: <overrides>;

Changelog.md

@@ -1,5 +1,20 @@
 # Changelog
 
+## Unreleased
+
+Requires Elpi 1.15.0 and Coq 8.16.
+
+### HOAS
+- Change arguments are passed after elaboration
+- New attribute `#[arguments(raw)]` to get arguments in raw format
+- Change raw inductive declaration using `|` to mark non-uniform
+  parameters is expected to not pass uniform parameters to the inductive
+  type (the same behavior applies to elaborated arguments)
+
+### Vernacular
+- New `Accumulate File <ident>` to be used in tandem with Coq 8.16
+  `From <path> Extra Dependency <file> as <ident>`
+
 ## [1.14.0] - 07-04-2022
 
 Requires Elpi 1.15.0 and Coq 8.15.

Makefile

@@ -29,24 +29,48 @@ else
 DOCDEP=
 endif
 
-DOCDIR=$(shell $(COQBIN)/coqc -where)/../../share/doc/coq-elpi/
+ifndef DOCDIR
+DOCDIR=$(shell $(COQBIN)/coqc -where)/../../share/doc/coq-elpi
+endif
+
+ifndef COQDOCINSTALL
+COQDOCINSTALL=$(DESTDIR)$(DOCDIR)
+endif
 
-all: build test
 
-build: Makefile.coq $(DEPS)
+all:
+	$(MAKE) build-core
+	$(MAKE) test-core
+	$(MAKE) examples
+	$(MAKE) build-apps
+	$(MAKE) test-apps
+
+build-core: Makefile.coq $(DEPS)
 	@echo "########################## building plugin ##########################"
 	@if [ -x $(COQBIN)/coqtop.byte ]; then \
 		$(MAKE) --no-print-directory -f Makefile.coq bytefiles; \
 	fi
 	@$(MAKE) --no-print-directory -f Makefile.coq opt
+
+build-apps: build-core
 	@echo "########################## building APPS ############################"
-	@$(foreach app,$(APPS),$(MAKE) -C $(app) $@ &&) true
+	@$(foreach app,$(APPS),$(MAKE) -C $(app) build &&) true
 
-test: Makefile.test.coq $(DEPS) build
+build: build-core build-apps
+
+test-core: Makefile.test.coq $(DEPS) build-core
 	@echo "########################## testing plugin ##########################"
 	@$(MAKE) --no-print-directory -f Makefile.test.coq
+
+test-apps: build-apps
 	@echo "########################## testing APPS ############################"
-	@$(foreach app,$(APPS),$(MAKE) -C $(app) $@ &&) true
+	@$(foreach app,$(APPS),$(MAKE) -C $(app) test &&) true
+
+test: test-core test-apps
+
+examples: Makefile.examples.coq $(DEPS) build-core
+	@echo "############################ examples ############################"
+	@$(MAKE) --no-print-directory -f Makefile.examples.coq
 
 doc: $(DOCDEP)
 	@echo "########################## generating doc ##########################"
@@ -69,8 +93,10 @@ doc: $(DOCDEP)
 Makefile.coq Makefile.coq.conf: src/coq_elpi_builtins_HOAS.ml src/coq_elpi_config.ml _CoqProject
 	@$(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq
 	@$(MAKE) --no-print-directory -f Makefile.coq .merlin
-Makefile.test.coq Makefile.test.coq.conf: _CoqProject
+Makefile.test.coq Makefile.test.coq.conf: _CoqProject.test
 	@$(COQBIN)/coq_makefile -f _CoqProject.test -o Makefile.test.coq
+Makefile.examples.coq Makefile.examples.coq.conf: _CoqProject.examples
+	@$(COQBIN)/coq_makefile -f _CoqProject.examples -o Makefile.examples.coq
 src/coq_elpi_builtins_HOAS.ml: elpi/coq-HOAS.elpi Makefile.coq.local
 	echo "(* Automatically generated from $<, don't edit *)" > $@
 	echo "let code = {|" >> $@
@@ -100,17 +126,17 @@ install:
 	@echo "########################## installing APPS ############################"
 	@$(foreach app,$(APPS),$(MAKE) -C $(app) $@ &&) true
 	@echo "########################## installing doc ############################"
-	-mkdir -p $(DESTDIR)$(DOCDIR)
-	-cp doc/* $(DESTDIR)$(DOCDIR)
+	-mkdir -p $(COQDOCINSTALL)
+	-cp doc/* $(COQDOCINSTALL)
 	@echo "########################## installed ############################"
 
 
 # compile just one file
 theories/%.vo: force
 	@$(MAKE) --no-print-directory -f Makefile.coq $@
-tests/%.vo: force build Makefile.test.coq
+tests/%.vo: force build-core Makefile.test.coq
 	@$(MAKE) --no-print-directory -f Makefile.test.coq $@
-examples/%.vo: force build Makefile.test.coq
+examples/%.vo: force build-core Makefile.test.coq
 	@$(MAKE) --no-print-directory -f Makefile.test.coq $@
 
 SPACE=$(XXX) $(YYY)

Makefile.coq.local

@@ -6,7 +6,6 @@ theories/elpi.vo: $(wildcard elpi/*.elpi)
 
 
 merlin-hook::
-	echo "PKG camlp5" >> .merlin
 	echo "S $(abspath $(ELPIDIR))" >> .merlin
 	echo "B $(abspath $(ELPIDIR))" >> .merlin
 	if [ "$(ELPIDIR)" != "elpi/findlib/elpi" ]; then\
@@ -18,5 +17,5 @@ install-extra::
 	install -m 0644 elpi-builtin.elpi "$(COQLIBINSTALL)/$$df";\
 	install -m 0644 coq-builtin.elpi "$(COQLIBINSTALL)/$$df";\
 	install -m 0644 elpi/coq-lib.elpi "$(COQLIBINSTALL)/$$df";\
-	install -m 0644 elpi/elpi-elaborator.elpi "$(COQLIBINSTALL)/$$df"
+	install -m 0644 elpi/elpi_elaborator.elpi "$(COQLIBINSTALL)/$$df"