Port to the [dune] build system.

.github/workflows/doc.yml

@@ -34,7 +34,7 @@ jobs:
         opam repo add coq-dev https://coq.inria.fr/opam/core-dev
         opam repo add extra-dev https://coq.inria.fr/opam/extra-dev
         opam update
-        opam install coq-serapi .
+        opam install coq-serapi . coq-core.8.19.1
         sudo apt-get update
         sudo apt-get install python3-pip -y
         pip3 install git+https://github.com/cpitclaudel/alectryon.git@c8ab1ec

.github/workflows/main.yml

@@ -28,11 +28,11 @@ jobs:
   build:
     runs-on: ubuntu-latest
     strategy:
+      fail-fast: false
       matrix:
-        coq_version:
-          - '8.19'
+        coq_version: [8.19.1, dev]
         ocaml_version:
-          - '4.14-flambda'
+          - '4.14.1-flambda'
     steps:
     - uses: actions/checkout@v2
     - uses: coq-community/docker-coq-action@v1

.gitignore

@@ -50,4 +50,6 @@ apps/coercion/src/coq_elpi_coercion_hook.ml
 apps/tc/src/coq_elpi_tc_hook.ml
 apps/cs/src/coq_elpi_cs_hook.ml
 
-*.timing
+*.timing
+_build
+tmp.out

.nix/config.nix

@@ -5,7 +5,31 @@
   bundles = {
 
     "coq-8.19".coqPackages = {
-      coq.override.version = "8.19+rc1";
+
+      hierarchy-builder.override.version = "master";
+      hierarchy-builder-shim.job = false;
+
+      mathcomp.override.version = "master";
+      mathcomp.job = true;
+
+      odd-order.override.version = "master";
+      odd-order.job = true;
+
+      mathcomp-analysis.override.version = "master";
+      mathcomp-analysis.job = true;
+
+      mathcomp-finmap.override.version = "master";
+      mathcomp-finmap.job = true;
+
+      mathcomp-classical.override.version = "master";
+      mathcomp-classical.job = true;
+
+      mathcomp-single-planB-src.job = false;
+      mathcomp-single-planB.job = false;
+      mathcomp-single.job = false;
+    };
+
+    "coq-master".coqPackages = {
 
       hierarchy-builder.override.version = "master";
       hierarchy-builder-shim.job = false;

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"dd771a5001cd955514f2462cad7cdd90377530e3"
+"5814f779562efc3e3c0f9bfeaea0468728e2e08b"

.nix/coq-overlays/coq-elpi/default.nix

@@ -61,10 +61,9 @@ in mkCoqDerivation {
   release."1.6.0".sha256      = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
   releaseRev = v: "v${v}";
 
-  buildFlags = [ "OCAMLWARN=" ];
-
   mlPlugin = true;
-  propagatedBuildInputs = [ coq.ocamlPackages.findlib elpi ];
+  useDune = true;
+  propagatedBuildInputs = [ coq.ocamlPackages.dune_3 coq.ocamlPackages.findlib  elpi coq.ocamlPackages.ppx_optcomp ];
 
   meta = {
     description = "Coq plugin embedding ELPI.";

Changelog.md

@@ -1,3 +1,16 @@
+# Unreleased
+
+Requires Elpi 1.19.2 and Coq 8.19 or Coq 8.20.
+
+### Build system
+- Change switch to dune
+
+### Apps/tc
+- Change supports higher order unification
+- Change syntax to register, enable and disable solver
+- Change solutions found in Elpi are eta-contracted
+
+
 # Changelog
 
 ## [2.1.1] - 15/05/2024

Makefile

@@ -1,156 +1,58 @@
-
-# detection of coq
-ifeq "$(COQBIN)" ""
-COQBIN := $(shell which coqc >/dev/null 2>&1 && dirname `which coqc`)
-endif
-ifeq "$(COQBIN)" ""
-$(error Coq not found, make sure it is installed in your PATH or set COQBIN)
-else
-$(info Using coq found in $(COQBIN), from COQBIN or PATH)
-endif
-export COQBIN := $(COQBIN)/
-
-# detection of elpi
-ifeq "$(ELPIDIR)" ""
-ELPIDIR=$(shell ocamlfind query elpi 2>/dev/null)
-endif
-ifeq "$(ELPIDIR)" ""
-$(error Elpi not found, make sure it is installed in your PATH or set ELPIDIR)
-endif
-export ELPIDIR
-
-DEPS=$(ELPIDIR)/elpi.cmxa $(ELPIDIR)/elpi.cma
-
-APPS=$(addprefix apps/, derive eltac NES locker coercion cs tc)
-
-ifeq "$(COQ_ELPI_ALREADY_INSTALLED)" ""
-DOCDEP=build
-else
-DOCDEP=
-endif
-
-ifndef DOCDIR
-DOCDIR=$(shell $(COQBIN)/coqc -where)/../../share/doc/coq-elpi
-endif
-
-ifndef COQDOCINSTALL
-COQDOCINSTALL=$(DESTDIR)$(DOCDIR)
-endif
-
-
 all:
-	$(MAKE) build-core
-	$(MAKE) test-core
-	$(MAKE) examples
-	$(MAKE) build-apps
-	$(MAKE) test-apps
+	@dune build
+.PHONY: all
 
-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-core:
+	@dune build theories
+.PHONY: build-core
 
-build-apps: build-core
-	@echo "########################## building APPS ############################"
-	@$(foreach app,$(APPS),$(MAKE) -C $(app) build &&) true
+build-apps:
+	@dune build $$(find apps -type d -name theories)
+.PHONY: build-apps
 
-build: build-core build-apps
+build:
+	@dune build @install
+.PHONY: build
 
-test-core: Makefile.test.coq $(DEPS) build-core
-	@echo "########################## testing plugin ##########################"
-	@$(MAKE) --no-print-directory -f Makefile.test.coq
+test-core:
+	@dune runtest tests
+.PHONY: test-core
 
-test-apps: build-apps
-	@echo "########################## testing APPS ############################"
-	@$(foreach app,$(APPS),$(MAKE) -C $(app) test &&) true
+test-apps:
+	@dune build $$(find apps -type d -name tests)
+.PHONY: test-apps
 
-test: test-core test-apps
+test:
+	@dune runtest
+	@dune build $$(find apps -type d -name tests)
+.PHONY: test
 
-examples: Makefile.examples.coq $(DEPS) build-core
-	@echo "############################ examples ############################"
-	@$(MAKE) --no-print-directory -f Makefile.examples.coq
+examples:
+	@dune build examples
+.PHONY: examples
 
-doc: $(DOCDEP)
+doc: build
 	@echo "########################## generating doc ##########################"
 	@mkdir -p doc
 	@$(foreach tut,$(wildcard examples/tutorial*$(ONLY)*.v),\
-		echo ALECTRYON $(tut) && ./etc/alectryon_elpi.py \
+		echo ALECTRYON $(tut) && OCAMLPATH=$(shell pwd)/_build/install/default/lib ./etc/alectryon_elpi.py \
 		    --frontend coq+rst \
 			--output-directory doc \
 		    --pygments-style vs \
-			-R theories elpi -Q src elpi \
+			-R $(shell pwd)/_build/install/default/lib/coq/user-contrib/elpi elpi \
 			$(tut) &&) true
 	@cp stlc.html doc/
 	@cp etc/tracer.png doc/
 
-.merlin: force
-	@rm -f .merlin
-	@$(MAKE) --no-print-directory -f Makefile.coq $@
-
-.PHONY: force build all test doc
-
-Makefile.coq Makefile.coq.conf: src/coq_elpi_builtins_HOAS.ml src/coq_elpi_builtins_arg_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.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_arg_HOAS.ml: elpi/coq-arg-HOAS.elpi Makefile.coq.local
-	echo "(* Automatically generated from $<, don't edit *)" > $@
-	echo "(* Regenerate via 'make $@' *)" >> $@
-	echo "let code = {|" >> $@
-	cat $< >> $@
-	echo "|}" >> $@
-src/coq_elpi_builtins_HOAS.ml: elpi/coq-HOAS.elpi Makefile.coq.local
-	echo "(* Automatically generated from $<, don't edit *)" > $@
-	echo "(* Regenerate via 'make $@' *)" >> $@
-	echo "let code = {|" >> $@
-	cat $< >> $@
-	echo "|}" >> $@
-
-src/coq_elpi_config.ml:
-	echo "let elpi_dir = \"$(abspath $(ELPIDIR))\";;" > $@
-
-clean: Makefile.coq Makefile.test.coq
-	@$(MAKE) -f Makefile.coq $@
-	@$(MAKE) -f Makefile.test.coq $@
-	@$(foreach app,$(APPS),$(MAKE) -C $(app) $@ &&) true
-
-include Makefile.coq.conf
-V_FILES_TO_INSTALL := \
-  $(filter-out theories/wip/%.v,\
-  $(COQMF_VFILES))
+clean:
+	@dune clean
+.PHONY: clean
 
 install:
-	@echo "########################## installing plugin ############################"
-	@$(MAKE) -f Makefile.coq $@ VFILES="$(V_FILES_TO_INSTALL)"
-	@if [ -x $(COQBIN)/coqtop.byte ]; then \
-		$(MAKE) -f Makefile.coq $@-byte VFILES="$(V_FILES_TO_INSTALL)"; \
-	fi
-	-cp etc/coq-elpi.lang $(COQMF_COQLIB)/ide/
-	@echo "########################## installing APPS ############################"
-	@$(foreach app,$(APPS),$(MAKE) -C $(app) $@ &&) true
-	@echo "########################## installing doc ############################"
-	-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-core Makefile.test.coq
-	@$(MAKE) --no-print-directory -f Makefile.test.coq $@
-examples/%.vo: force build-core Makefile.test.coq
-	@$(MAKE) --no-print-directory -f Makefile.test.coq $@
-
-SPACE=$(XXX) $(YYY)
-apps/%.vo: force
-	@$(MAKE) -C apps/$(word 1,$(subst /, ,$*)) \
-		$(subst $(SPACE),/,$(wordlist 2,99,$(subst /, ,$*))).vo
+	@dune build -p coq-elpi
+	@dune install coq-elpi
+.PHONY: install
 
 nix:
-	nix-shell --arg do-nothing true --run "updateNixToolBox & genNixActions"
+	nix-shell --arg do-nothing true --run "updateNixToolBox && genNixActions"
+.PHONY: nix