Skip to content

Commit

Permalink
fix: Use coq_makefile instead of dune, temporarily
Browse files Browse the repository at this point in the history
* Otherwise, with Coq 8.13:

  #=== 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 ocaml/dune#3210,
  which provides the `(mode native)` stanza.

* For details, see also: coq/ceps#48
  • Loading branch information
erikmd committed Apr 8, 2021
1 parent c45cebe commit 010afe3
Show file tree
Hide file tree
Showing 3 changed files with 30 additions and 12 deletions.
22 changes: 12 additions & 10 deletions Makefile
Original file line number Diff line number Diff line change
@@ -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
9 changes: 8 additions & 1 deletion _CoqProject
Original file line number Diff line number Diff line change
Expand Up @@ -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
11 changes: 10 additions & 1 deletion coq-mathcomp-multinomials.opam
Original file line number Diff line number Diff line change
Expand Up @@ -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"}
Expand Down

0 comments on commit 010afe3

Please sign in to comment.