From 8456d27290d673c8a6f0600791a56ee2ebaf7a5b Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Thu, 8 Apr 2021 04:37:33 +0200
Subject: [PATCH] fix: Use coq_makefile instead of dune, temporarily

* Otherwise, with (coq.8.13.2 + coq-native):

  #=== ERROR while compiling coq-coqeal.1.0.5 ===================================#
  # [...]
  # File "./refinements/multipoly.v", line 1532, characters 0-67:
  # Warning: Duplicate clear of sz_m' [duplicate-clear,ssr]
  # File "./refinements/.coq-native/NCoqEAL_refinements_multipoly.native", line 66, characters 14-82:
  # Error: Unbound module NSsrMultinomials_mpoly
  # Error: Native compiler exited with status 2

* This fix is temporary: when multinomials will require Coq >= 8.12.1,
  one could then rely on https://github.com/ocaml/dune/pull/3210,
  which provides the `(mode native)` stanza.

* For details, see also: https://github.com/coq/ceps/pull/48
---
 Makefile                       | 22 ++++++++++++----------
 _CoqProject                    |  9 ++++++++-
 coq-mathcomp-multinomials.opam | 11 ++++++++++-
 3 files changed, 30 insertions(+), 12 deletions(-)

diff --git a/Makefile b/Makefile
index 4911acb..60c6f71 100644
--- a/Makefile
+++ b/Makefile
@@ -1,16 +1,18 @@
 # -*- Makefile -*-
 
-# --------------------------------------------------------------------
-DUNEOPTS ?=
-DUNE     := dune $(DUNEOPTS)
+all: Makefile.coq
+	+make -f Makefile.coq all
 
-# --------------------------------------------------------------------
-.PHONY: default build clean
+clean: Makefile.coq
+	+make -f Makefile.coq clean
+	rm -f Makefile.coq Makefile.coq.conf
 
-default: build
+_CoqProject:;
 
-build:
-	$(DUNE) build
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-clean:
-	$(DUNE) clean
+%: Makefile.coq
+	+make -f Makefile.coq $@
+
+.PHONY: all clean
diff --git a/_CoqProject b/_CoqProject
index d8781a0..6d21035 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,4 +3,11 @@
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -projection-no-head-constant
 
--R _build/default/src SsrMultinomials
+# -R _build/default/src SsrMultinomials
+-R src SsrMultinomials
+
+src/ssrcomplements.v
+src/monalg.v
+src/xfinmap.v
+src/mpoly.v
+src/freeg.v
diff --git a/coq-mathcomp-multinomials.opam b/coq-mathcomp-multinomials.opam
index 4a7ee7b..6634927 100644
--- a/coq-mathcomp-multinomials.opam
+++ b/coq-mathcomp-multinomials.opam
@@ -6,7 +6,16 @@ bug-reports: "https://github.com/math-comp/multinomials/issues"
 dev-repo: "git+https://github.com/math-comp/multinomials.git"
 license: "CeCILL-B"
 authors: ["Pierre-Yves Strub"]
-build: [ "dune" "build" "-p" name "-j" jobs ]
+# build: [ "dune" "build" "-p" name "-j" jobs ]
+
+build: [make "-j%{jobs}%"]
+run-test: [make "-C" "tests" "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "ocaml"
+  "coq" {= "dev"}
+]
+
 depends: [
   "coq"                    {(>= "8.10" & < "8.14~") | = "dev"}
   "dune"                   {>= "2.5"}