From 7d0cc22041ed57ffdff46f0edd36b26dd4d5a083 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Wed, 29 Jan 2025 10:25:30 +0100
Subject: [PATCH] Fix makefile to make the equations.dev package work again

---
 Makefile            | 69 ++++++++++-----------------------------------
 Makefile.hott.local |  2 --
 Makefile.local      | 33 ----------------------
 Makefile.rocq.local |  2 --
 dune-project        |  2 +-
 siteexamples.sh     |  8 +++---
 6 files changed, 20 insertions(+), 96 deletions(-)
 delete mode 100644 Makefile.hott.local
 delete mode 100644 Makefile.local
 delete mode 100644 Makefile.rocq.local

diff --git a/Makefile b/Makefile
index 61267dd7..2ab62ba8 100644
--- a/Makefile
+++ b/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,12 +32,10 @@ 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
@@ -74,12 +43,4 @@ ci-hott:
 	$(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
diff --git a/Makefile.hott.local b/Makefile.hott.local
deleted file mode 100644
index 27b8a9d4..00000000
--- a/Makefile.hott.local
+++ /dev/null
@@ -1,2 +0,0 @@
-CAMLPKGS+=-package rocq-runtime.plugins.extraction,rocq-runtime.plugins.cc
-ci: all test-suite examples
diff --git a/Makefile.local b/Makefile.local
deleted file mode 100644
index 54ccea6f..00000000
--- a/Makefile.local
+++ /dev/null
@@ -1,33 +0,0 @@
-makefiles: test-suite/Makefile examples/Makefile
-
-test-suite/Makefile: test-suite/_CoqProject
-	cd test-suite && coq_makefile -f _CoqProject -o Makefile
-
-examples/Makefile: examples/_CoqProject
-	cd examples && coq_makefile -f _CoqProject -o Makefile
-
-pre-all:: makefiles
-
-# Ensure we make the bytecode version as well
-post-all:: bytefiles
-
-clean-examples:
-	cd examples && $(MAKE) clean
-
-clean-test-suite: makefiles
-	cd test-suite && $(MAKE) clean
-
-test-suite: makefiles
-	cd test-suite && $(MAKE)
-
-.PHONY: test-suite
-
-examples: examples/Makefile
-	cd examples && $(MAKE)
-
-.PHONY: examples
-
-clean:: makefiles clean-examples clean-test-suite
-
-siteexamples: examples/*.glob
-	sh siteexamples.sh
diff --git a/Makefile.rocq.local b/Makefile.rocq.local
deleted file mode 100644
index 27b8a9d4..00000000
--- a/Makefile.rocq.local
+++ /dev/null
@@ -1,2 +0,0 @@
-CAMLPKGS+=-package rocq-runtime.plugins.extraction,rocq-runtime.plugins.cc
-ci: all test-suite examples
diff --git a/dune-project b/dune-project
index 22584373..2c4b9fbd 100644
--- a/dune-project
+++ b/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
diff --git a/siteexamples.sh b/siteexamples.sh
index 84ab14d0..422a03b1 100644
--- a/siteexamples.sh
+++ b/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