Port to the [dune] build system.

The [_CoqProject] is still useful for editors, it was partially
generated using:
```
grep "^ (name" apps/**/dune | \
  grep -v src | \
  sed 's/apps\/\([a-zA-Z]*\)\/\([a-zA-Z]*\)\/dune: (name \([^)]*\))/-Q apps\/\1\/\2 elpi.apps.\1.\2\n-Q _build\/default\/apps\/\1\/\2 elpi.apps.\1.\2/' | sed 's/\.theories//'
```

Co-Authored-By: Rodolphe Lepigre <[email protected]>

Author: gares

.gitignore

@@ -49,3 +49,4 @@ apps/coercion/src/coq_elpi_coercion_hook.ml
 .filestoinstall
 apps/tc/src/coq_elpi_tc_hook.ml
 apps/cs/src/coq_elpi_cs_hook.ml
+_build

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
-
-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) build &&) true
-
-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) 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 ##########################"
-	@mkdir -p doc
-	@$(foreach tut,$(wildcard examples/tutorial*$(ONLY)*.v),\
-		echo ALECTRYON $(tut) && ./etc/alectryon_elpi.py \
-		    --frontend coq+rst \
-			--output-directory doc \
-		    --pygments-style vs \
-			-R theories elpi -Q src 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))
+	@dune build
+.PHONY: all
+
+build-core:
+	@dune build theories
+.PHONY: build-core
+
+build-apps:
+	@dune build $$(find apps -type d -name theories)
+.PHONY: build-apps
+
+build:
+	@dune build @install
+.PHONY: build
+
+test-core:
+	@dune build tests
+.PHONY: test-core
+
+test-apps:
+	@dune build $$(find apps -type d -name tests)
+.PHONY: test-apps
+
+test:
+	@dune build $$(find . -type d -name tests)
+.PHONY: test
+
+examples:
+	@dune build examples
+.PHONY: examples
+
+# FIXME
+#doc: $(DOCDEP)
+#	@echo "########################## generating doc ##########################"
+#	@mkdir -p doc
+#	@$(foreach tut,$(wildcard examples/tutorial*$(ONLY)*.v),\
+#		echo ALECTRYON $(tut) && ./etc/alectryon_elpi.py \
+#		    --frontend coq+rst \
+#			--output-directory doc \
+#		    --pygments-style vs \
+#			-R theories elpi -Q src elpi \
+#			$(tut) &&) true
+#	@cp stlc.html doc/
+#	@cp etc/tracer.png doc/
+
+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