-
Notifications
You must be signed in to change notification settings - Fork 21
/
Makefile
89 lines (71 loc) · 3.5 KB
/
Makefile
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
.SUFFIXES:
MOD_NAME:=Rewriter
SRC_DIR:=src/Rewriter
PLUGINS_DIR:=$(SRC_DIR)/Util/plugins
PROFILE?=
VERBOSE?=
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
PYTHON3 := python3
STRICT_DEPS?=
EXTERNAL_PERF_DEPENDENCIES?=
.PHONY: clean
# Makefile.coq from Coq 8.9 is incompatible with Coq >= 8.10, so we invoke clean a different way, and force a remake of Makefile.coq
ifeq ($(MAKECMDGOALS),clean)
clean::
$(MAKE) -B Makefile.coq
$(MAKE) -f Makefile.coq clean
else
include Makefile.local.common
include Makefile.coq
endif
clean::
rm -f _CoqProject Makefile.coq Makefile-old.conf $(COQ_VERSION_FILE)
ifneq ($(COQ_EXTENDED_VERSION),$(COQ_EXTENDED_VERSION_OLD))
$(COQ_VERSION_FILE)::
$(SHOW)'echo $$COQ_VERSION_INFO ($(COQ_VERSION)) > $@'
ifneq (,$(strip $(COQ_EXTENDED_VERSION_OLD)))
@echo 'Replacing $(COQ_EXTENDED_VERSION_OLD)'
@echo ' with $(COQ_EXTENDED_VERSION)'
endif
$(HIDE)echo '$(COQ_EXTENDED_VERSION)' > $@
else
ifeq (,$(wildcard $(COQ_VERSION_FILE)))
$(COQ_VERSION_FILE)::
@echo 'Error: Invalid empty COQ_EXTENDED_VERSION:'
$(COQ_VERSION_COQC_CMD) || true
$(COQ_VERSION_COQTOP_CMD) || true
$(HIDE)exit 1
endif
endif
_CoqProject: _CoqProject.in
sed 's?@META@?$(META_FILE_FRAGMENT)?g' $< > $@
# This target is used to update the _CoqProject file.
# But it only works if we have git
ifneq (,$(wildcard .git/))
SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g'
EXISTING_COQPROJECT_CONTENTS_SORTED:=$(shell cat _CoqProject.in 2>&1 | $(SORT_COQPROJECT))
WARNINGS_PLUS := +implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+deprecated-hint-constr,+fragile-hint-constr,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+undeclared-scope,+deprecated-typeclasses-transparency-without-locality,+future-coercion-class-field
WARNINGS := $(WARNINGS_PLUS),unsupported-attributes
COQPROJECT_CMD:=(echo @META@; echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-I $(PLUGINS_DIR)'; echo '-arg -w -arg $(WARNINGS)'; echo '-arg -native-compiler -arg ondemand'; (git ls-files '$(SRC_DIR)/*.v' '$(SRC_DIR)/*.mlg' '$(SRC_DIR)/*.mllib' '$(SRC_DIR)/*.ml' '$(SRC_DIR)/*.mli' | $(SORT_COQPROJECT)); (echo '$(COMPATIBILITY_FILES)' | tr ' ' '\n'))
NEW_COQPROJECT_CONTENTS_SORTED:=$(shell $(COQPROJECT_CMD) | $(SORT_COQPROJECT))
ifneq ($(EXISTING_COQPROJECT_CONTENTS_SORTED),$(NEW_COQPROJECT_CONTENTS_SORTED))
.PHONY: _CoqProject.in
_CoqProject.in:
$(SHOW)'ECHO > $@'
$(HIDE)$(COQPROJECT_CMD) > $@
endif
endif
.DEFAULT_GOAL := all
# Setting this will make things unpleasant on a clean build, but also helps enormously with diagnosing errors
EXTRA_SED_FOR_DEPS:=
ifneq (,$(STRICT_DEPS))
EXTRA_SED_FOR_DEPS:=| sed s'/-include $$(ALLDFILES)/include $$(ALLDFILES)/g'
endif
# We must work around COQBUG(https://github.com/coq/coq/issues/10907) and fix the conf target
Makefile.coq Makefile-old.conf: Makefile _CoqProject $(COQ_VERSION_FILE)
$(SHOW)'COQ_MAKEFILE -f _CoqProject > Makefile.coq'
$(HIDE)(($(COQBIN)coq_makefile -f _CoqProject -o Makefile-old && cat Makefile-old | sed s'/Makefile-old.conf:/Makefile-old-old.conf:/g' | sed 's/Makefile-old.local/Makefile.local/g; s/^-\?include Makefile.local-late$$//g' $(EXTRA_SED_FOR_DEPS)); echo; echo 'include Makefile.local-late') > Makefile.coq && rm Makefile-old
Makefile.coq: | Makefile-old.conf
clean::
rm -f Makefile.coq