Merge pull request #90 from math-comp/ci

Fix CI by reverting to coq_makefile

Author: pi8027

.github/workflows/ci.yml

@@ -18,8 +18,6 @@ jobs:
           - mathcomp/mathcomp:2.2.0-coq-8.17
           - mathcomp/mathcomp:2.2.0-coq-8.18
           - mathcomp/mathcomp:2.2.0-coq-8.19
-          - mathcomp/mathcomp-dev:coq-8.16
-          - mathcomp/mathcomp-dev:coq-8.17
           - mathcomp/mathcomp-dev:coq-8.18
           - mathcomp/mathcomp-dev:coq-8.19
           - mathcomp/mathcomp-dev:coq-dev

Makefile

@@ -1,19 +1,25 @@
-# -*- Makefile -*-
+# KNOWNTARGETS will not be passed along to CoqMakefile
+KNOWNTARGETS := Makefile.coq
+# KNOWNFILES will not get implicit targets from the final rule, and so
+# depending on them won't invoke the submake
+# Warning: These files get declared as PHONY, so any targets depending
+# on them always get rebuilt
+KNOWNFILES   := Makefile _CoqProject
 
-# --------------------------------------------------------------------
-DUNEOPTS ?=
-DUNE     := dune $(DUNEOPTS)
+.DEFAULT_GOAL := invoke-coqmakefile
 
-# --------------------------------------------------------------------
-.PHONY: default build clean
+Makefile.coq: Makefile _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-default: build
+invoke-coqmakefile: Makefile.coq
+	$(MAKE) --no-print-directory -f Makefile.coq $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
 
-build:
-	$(DUNE) build
+.PHONY: invoke-coqmakefile $(KNOWNFILES)
 
-install:
-	$(DUNE) install
+####################################################################
+##                      Your targets here                         ##
+####################################################################
 
-clean:
-	$(DUNE) clean
+# This should be the last rule, to handle any targets not declared above
+%: invoke-coqmakefile
+	@true

_CoqProject

@@ -1,6 +1,11 @@
+src/freeg.v
+src/monalg.v
+src/mpoly.v
+src/ssrcomplements.v
+src/xfinmap.v
+
+-R src mathcomp.multinomials
 -arg -w -arg -ambiguous-paths
 -arg -w -arg -notation-overridden
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -projection-no-head-constant
-
--R _build/default/src mathcomp.multinomials

coq-mathcomp-multinomials.opam

@@ -5,12 +5,10 @@ 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: [make "-j%{jobs}%"]
+install: [make "install"]
 depends: [
   "coq"                    {(>= "8.16" & < "8.20~") | = "dev"}
-  "dune"                   {>= "3.8"}
   "coq-mathcomp-ssreflect" {(>= "2.0" & < "2.3~") | = "dev"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-bigenough" {(>= "1.0" & < "1.1~") | = "dev"}