forked from math-comp/multinomials
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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 ocaml/dune#3210, which provides the `(mode native)` stanza. * For details, see also: coq/ceps#48
- Loading branch information
Showing
3 changed files
with
30 additions
and
12 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters