Enable compilation with rocq makefile

Can be useful for instance to get timing informations.

Author: proux01

.gitignore

@@ -134,6 +134,8 @@ ide/coqide/index_urls.txt
 .lia.cache
 .nia.cache
 .nra.cache
+theories/Makefile.coq
+theories/Makefile.coq.conf
 
 # emacs save files
 *~

Makefile

@@ -1,17 +1,20 @@
 DUNE=dev/with-rocq-wrap.sh dune
 
-all:
+all install:
+	+$(MAKE) -C theories $@
+
+dune:
 	$(DUNE) build -p rocq-stdlib @install
 
-install:
+dune-install:
 	$(DUNE) install --root . rocq-stdlib
 
 build-% install-%:
 	+$(MAKE) -C theories $@
 
 # Make of individual .vo
 theories/%.vo:
-	$(DUNE) build $@
+	+$(MAKE) -C theories $*.vo
 
 refman-html:
 	$(DUNE) build --root . --no-buffer @refman-html

coq-stdlib.opam

@@ -9,25 +9,10 @@ license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/stdlib/issues"
+dev-repo: "git+https://github.com/coq/stdlib.git"
 depends: [
-  "dune" {>= "3.8"}
   "coq-core"
   "rocq-stdlib" {= version}
-  "odoc" {with-doc}
 ]
-dev-repo: "git+https://github.com/coq/stdlib.git"
 build: [
-  ["dune" "subst"] {dev}
-  [
-    "dev/with-rocq-wrap.sh"
-    "dune"
-    "build"
-    "-p"
-    name
-    "-j"
-    jobs
-    "@install"
-    "@runtest" {with-test}
-    "@doc" {with-doc}
-  ]
 ]

coq-stdlib.opam.template

@@ -1,15 +1,6 @@
+depends: [
+  "coq-core"
+  "rocq-stdlib" {= version}
+]
 build: [
-  ["dune" "subst"] {dev}
-  [
-    "dev/with-rocq-wrap.sh"
-    "dune"
-    "build"
-    "-p"
-    name
-    "-j"
-    jobs
-    "@install"
-    "@runtest" {with-test}
-    "@doc" {with-doc}
-  ]
 ]

rocq-stdlib.opam

@@ -22,25 +22,14 @@ license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/stdlib/issues"
+dev-repo: "git+https://github.com/coq/stdlib.git"
 depends: [
-  "dune" {>= "3.8"}
   "rocq-runtime"
-  "rocq-core" {= version}
-  "odoc" {with-doc}
+  "rocq-core" {>= "9.0"}
 ]
-dev-repo: "git+https://github.com/coq/stdlib.git"
 build: [
-  ["dune" "subst"] {dev}
-  [
-    "dev/with-rocq-wrap.sh"
-    "dune"
-    "build"
-    "-p"
-    name
-    "-j"
-    jobs
-    "@install"
-    "@runtest" {with-test}
-    "@doc" {with-doc}
-  ]
+  [make "-j" jobs]
+]
+install: [
+  [make "install"]
 ]

rocq-stdlib.opam.template

@@ -1,15 +1,10 @@
+depends: [
+  "rocq-runtime"
+  "rocq-core" {>= "9.0"}
+]
 build: [
-  ["dune" "subst"] {dev}
-  [
-    "dev/with-rocq-wrap.sh"
-    "dune"
-    "build"
-    "-p"
-    name
-    "-j"
-    jobs
-    "@install"
-    "@runtest" {with-test}
-    "@doc" {with-doc}
-  ]
+  [make "-j" jobs]
+]
+install: [
+  [make "install"]
 ]

theories/Makefile

@@ -3,6 +3,15 @@ ROCQMAKEFILE?=$(ROCQBIN)rocq makefile
 ROCQMAKEOPTIONS?=
 ROCQMAKEFILEOPTIONS?=
 
+all: Makefile.coq
+	+$(MAKE) -f $< $(ROCQMAKEOPTIONS)
+
+install: Makefile.coq
+	+$(MAKE) -f $< $(ROCQMAKEOPTIONS) install
+
+Makefile.coq: _CoqProject
+	$(ROCQMAKEFILE) $(ROCQMAKEFILEOPTIONS) -f $< $(shell find . -name "*.v") -o $@
+
 build-%: Makefile-%.coq
 	+$(MAKE) -f $< $(ROCQMAKEOPTIONS)
 
@@ -18,3 +27,6 @@ Makefile-%.coq: Make.%
 
 install-%: Makefile-%.coq
 	+$(MAKE) -f $< $(ROCQMAKEOPTIONS) install
+
+%.vo: Makefile.coq %.v
+	+$(MAKE) -f $< $(ROCQMAKEOPTIONS) $@