-
Notifications
You must be signed in to change notification settings - Fork 7
/
Makefile.variables.kinds
117 lines (97 loc) · 2.59 KB
/
Makefile.variables.kinds
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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
mkfile_path := $(abspath $(lastword $(MAKEFILE_LIST)))
PERF_ABS_DIR := $(patsubst %/,%,$(dir $(mkfile_path)))
include $(PERF_ABS_DIR)/Makefile.coq-versions-lite
KINDS := \
pattern \
n_polymorphic_universes \
repeat_setoid_rewrite_under_binders \
repeat_setoid_rewrite_under_binders_noop \
rewrite_strat_under_binders \
rewrite_repeated_app_autorewrite \
rewrite_repeated_app_autorewrite_noop \
rewrite_repeated_app_ssrrewrite \
rewrite_repeated_app_ssrrewrite_noop \
rewrite_repeated_app_rewrite_strat \
rewrite_repeated_app_fast_rewrite \
rewrite_repeated_app_fast_rewrite_no_abstract \
destruct_large_context \
Reify/BaselineStats \
Reify/CanonicalStructures \
Reify/LtacVariants \
Reify/OCaml \
Reify/Parametricity \
Reify/TypeClasses \
# end of list
LTAC2_KINDS := \
rewrite_repeated_app_fast_rewrite_ltac2 \
Reify/Ltac2 \
# end of list
VERSION_8_9_OR_NEWER_KINDS := \
typeclass_reification_let_in_HOAS \
typeclass_reification_let_in_PHOAS \
# end of list
Q_DECIMAL_NOTATION_KINDS := \
rewrite_lift_lets_map \
rewrite_plus_0_tree \
sieve_of_eratosthenes \
rewrite_under_lets_plus_0 \
# end of list
VERSION_8_10_OR_NEWER_KINDS := \
$(Q_DECIMAL_NOTATION_KINDS) \
# end of list
ZIFY_POST_HOOK_EUCLIDEAN_KINDS := \
zify_large_context \
# end of list
VERSION_8_11_OR_NEWER_KINDS := \
$(ZIFY_POST_HOOK_EUCLIDEAN_KINDS) \
# end of list
QUOTE_KINDS := \
Reify/QuoteFlat \
# end of list
DISABLED_FILES?=
DISABLED_KINDS?=
ifneq (,$(IS_8_9_OR_NEWER))
KINDS += $(VERSION_8_9_OR_NEWER_KINDS)
else
DISABLED_FILES += $(addsuffix .v,$(VERSION_8_9_OR_NEWER_KINDS))
DISABLED_KINDS += $(VERSION_8_9_OR_NEWER_KINDS)
endif
ifeq (,$(USES_ML4))
DISABLED_FILES += %.ml4
endif
ifeq (,$(USES_MLG))
DISABLED_FILES += %.mlg
endif
ifneq (,$(IS_8_10_OR_NEWER))
KINDS += $(VERSION_8_10_OR_NEWER_KINDS)
else
DISABLED_FILES += $(addsuffix .v,$(VERSION_8_10_OR_NEWER_KINDS))
DISABLED_KINDS += $(VERSION_8_10_OR_NEWER_KINDS)
endif
ifneq (,$(IS_8_11_OR_NEWER))
KINDS += $(VERSION_8_11_OR_NEWER_KINDS)
else
DISABLED_FILES += $(addsuffix .v,$(VERSION_8_11_OR_NEWER_KINDS))
DISABLED_KINDS += $(VERSION_8_11_OR_NEWER_KINDS)
endif
ifneq (,$(HAS_LTAC2))
KINDS += $(LTAC2_KINDS)
else
DISABLED_FILES += $(addsuffix .v,$(LTAC2_KINDS)) \
rewrite_repeated_app_common_ltac2.v \
Reify/Ltac2Reify.v \
Ltac2/Util/% \
# end of list
DISABLED_KINDS += $(LTAC2_KINDS)
endif
ifneq (,$(HAS_QUOTE_PLUGIN))
KINDS += $(QUOTE_KINDS)
else
DISABLED_FILES += $(addsuffix .v,$(QUOTE_KINDS)) \
# end of list
DISABLED_KINDS += $(QUOTE_KINDS)
endif
SH_KINDS :=
SPECIAL_KINDS :=
ALL_VKINDS := $(KINDS) $(SPECIAL_KINDS)
ALL_KINDS := $(ALL_VKINDS) $(SH_KINDS)