Fix makefile to make the equations.dev package work again

Makefile

@@ -1,52 +1,23 @@
 # One of these two files will have been generated
 
-.PHONY: all default makefiles clean-makefiles
+.PHONY: all
 
-all: Makefile.rocq
-	$(MAKE) -f Makefile.rocq
-	test -f Makefile.hott && $(MAKE) -f Makefile.hott || true
+all: 
+	dune build -p rocq-equations,rocq-equations-examples @install
 
-install: Makefile.rocq
-	$(MAKE) -f Makefile.rocq install
-	test -f Makefile.hott && $(MAKE) -f Makefile.hott install || true
+install:
+	dune install rocq-equations rocq-equations-examples
 
-makefiles: test-suite/Makefile examples/Makefile
+.PHONY: install
 
-clean-makefiles:
-	rm -f test-suite/Makefile examples/Makefile
-
-test-suite/Makefile: test-suite/_CoqProject
-	cd test-suite && rocq makefile -f _CoqProject -o Makefile
-
-examples/Makefile: examples/_CoqProject
-	cd examples && rocq makefile -f _CoqProject -o Makefile
-
-pre-all:: makefiles
-
-# Ensure we make the bytecode version as well
-post-all:: bytefiles
-
-clean-examples: makefiles
-	cd examples && $(MAKE) clean
-
-clean-test-suite: makefiles
-	cd test-suite && $(MAKE) clean
-
-test-suite: makefiles all
-	cd test-suite && $(MAKE)
+test-suite:
+	dune build -p rocq-equations-tests
 
 .PHONY: test-suite
 
-examples: examples/Makefile all
-	cd examples && $(MAKE)
-
-.PHONY: examples
-
-clean: clean-makefiles makefiles
-	$(MAKE) -f Makefile.rocq clean
-	test -f Makefile.hott && make -f Makefile.hott clean || true
-	$(MAKE) clean-examples clean-test-suite
-
+clean:
+	dune clean
+
 siteexamples: examples/*.glob
 	sh siteexamples.sh
 
@@ -61,25 +32,15 @@ toplevel: src/equations_plugin.cma bytefiles
 		-package rocq-runtime.toplevel,rocq-runtime.plugins.extraction \
 	  $< $(COQLIB)/toplevel/coqtop_bin.ml -o coqtop_equations
 
-dune:-
-	dune build
-
 ci-dune:
-	# opam install -j 2 -y coq-hott.dev
-	dune build
+	dune build -p rocq-equations,rocq-equations-examples,rocq-equations-tests
+	dune build -p rocq-equations,rocq-equations-examples @install
+	dune install rocq-equations rocq-equations-examples
 
 ci-hott:
 	opam install -j 2 -y coq-hott.dev
 	test -f Makefile.hott && $(MAKE) -f Makefile.hott all
 	$(MAKE) -f Makefile.hott install
 	$(MAKE) -f Makefile.hott uninstall
 
-ci-local:
-	$(MAKE) -f Makefile.rocq all 
-	$(MAKE) test-suite examples
-	$(MAKE) -f Makefile.rocq install
-	$(MAKE) -f Makefile.rocq uninstall
-
-ci: ci-local
-
-.PHONY: ci-dune ci-hott ci-local
+.PHONY: ci-dune ci-hott

dune-project

@@ -28,7 +28,7 @@
 (package
  (name rocq-equations-examples)
  (synopsis "Examples")
- (description "Do not install")
+ (description "Examples of use of Equations")
  (depends rocq-equations))
 
 (package

siteexamples.sh

@@ -1,14 +1,14 @@
 #/bin/sh
 
-cd examples
+cd _build/default/examples
 
 for i in *.v
 do
   coqdoc -s --no-lib-name -parse-comments --no-index --utf8 --interpolate --html \
       --external http://github.com/mattam82/Coq-Equations/tree/main Equations \
-      -Q ../theories Equations -R . Examples -d ../../equations-www/examples $i
+      -Q ../theories Equations -Q . Examples -d ../../../../equations-www/examples $i
 done
 
-cd ..
+cd ../../../../equations-www
 
-git checkout doc/examples/coqdoc.css
+git checkout examples/coqdoc.css