Makefile-coq.local

include Makefile.local.common

PROFILE?=
# Remove -undeclared-scope once we stop supporting 8.9
OTHERFLAGS += -w -notation-overridden,-undeclared-scope,-deprecated-hint-rewrite-without-locality,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths
ifneq ($(PROFILE),)
OTHERFLAGS += -profile-ltac
endif

COQ_VERSION_PREFIX = The Coq Proof Assistant, version
COQ_VERSION := $(firstword $(subst $(COQ_VERSION_PREFIX),,$(shell $(COQBIN)coqc --version 2>/dev/null)))

ifneq (,$(filter 8.11%,$(COQ_VERSION)))
EXPECTED_EXT:=.v811
COQ_VERSION_DESCRIPTION := Coq v8.11
else
ifneq (,$(filter 8.12%,$(COQ_VERSION)))
EXPECTED_EXT:=.v812
COQ_VERSION_DESCRIPTION := Coq v8.12
else
ifneq (,$(filter 8.13%,$(COQ_VERSION)))
EXPECTED_EXT:=.v813
COQ_VERSION_DESCRIPTION := Coq v8.13
else
ifneq (,$(filter 8.14%,$(COQ_VERSION)))
EXPECTED_EXT:=.v814
COQ_VERSION_DESCRIPTION := Coq v8.14
else
EXPECTED_EXT:=.v815
COQ_VERSION_DESCRIPTION := Coq v8.15
endif
endif
endif
endif

define make_version_rule
# $(1) - .v file name

make_version_rule_OLD_CONTENTS := $$(shell cat $(1) 2>/dev/null)
make_version_rule_NEW_CONTENTS := $$(shell cat $(1)$(EXPECTED_EXT) 2>/dev/null)

ifneq ($$(make_version_rule_OLD_CONTENTS),$$(make_version_rule_NEW_CONTENTS))
.PHONY: $(1)
$(1): $(1)$(EXPECTED_EXT)
	$$(SHOW)'CP $$< $$@ ($(COQ_VERSION_DESCRIPTION))'
	$$(HIDE)cp $$< $$@
else
$(1): $(1)$(EXPECTED_EXT)
	$$(SHOW)'TOUCH $$@ (contents up to date with $(COQ_VERSION_DESCRIPTION))'
	$$(HIDE)touch $$@
endif

endef

$(eval $(foreach f,$(VERSION_DEPENDENT_FILES),$(call make_version_rule,$(f))))

SORT_TACTICS := env LC_COLLATE=C sort
TACTICS_V_FILE := src/Util/Tactics.v
EXISTING_TACTICS_CONTENTS_SORTED:=$(shell cat $(TACTICS_V_FILE) 2>&1 | $(SORT_TACTICS))
NEW_TACTICS_CONTENTS_SORTED:=$(shell src/Util/make_tactics.sh | $(SORT_TACTICS))

ifneq ($(EXISTING_TACTICS_CONTENTS_SORTED),$(NEW_TACTICS_CONTENTS_SORTED))
.PHONY: $(TACTICS_V_FILE)
$(TACTICS_V_FILE):
	$(SHOW)'ECHO > $@'
	$(HIDE)src/Util/make_tactics.sh > $@
endif