-
Notifications
You must be signed in to change notification settings - Fork 19
/
Makefile.coq-versions-lite
62 lines (54 loc) · 2.2 KB
/
Makefile.coq-versions-lite
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
mkfile_path := $(abspath $(lastword $(MAKEFILE_LIST)))
PERF_ABS_DIR := $(patsubst %/,%,$(dir $(mkfile_path)))
include $(PERF_ABS_DIR)/Makefile.characters
COQ_VERSION_FILE = .coq-version
COQ_VERSION_SHORT_FILE = .coq-version-short
COQ_VERSION_COMPILATION_DATE_FILE = .coq-version-compilation-date
COQ_VERSION_SHORT_DATE_FILE = .coq-version-short-date
COQ_VERSION_CONFIG_FILE := .coq-version-config
COQ_VERSION_OCAML_VERSION_FILE := .coq-version-ocaml-version
COQ_VERSION_OCAML_CONFIG_FILE := .coq-version-ocaml-config
COQ_VERSION_PREFIX = The Coq Proof Assistant, version
COQ_VERSION_FULL := $(subst $(COQ_VERSION_PREFIX),,$(shell $(COQBIN)coqc --version 2>/dev/null))
COQ_VERSION := $(firstword $(COQ_VERSION_FULL))
COQ_VERSION_CONFIG_CMD = $(COQBIN)coqc -config 2>/dev/null
COQ_VERSION_DATE := $(subst $(OPEN_PAREN),,$(subst $(CLOSE_PAREN),,$(wordlist 2, 3, $(COQ_VERSION_FULL))))
COQ_VERSION_COMPILATION := $(subst $(JOINER)with,$(SPACE)with,$(subst $(SPACE),$(JOINER),$(wordlist 4, $(words $(COQ_VERSION_FULL)),$(COQ_VERSION_FULL))))
COQ_VERSION_COMPILATION_DATE := $(subst $(JOINER),$(SPACE),$(subst compiled$(JOINER)on$(JOINER),,$(firstword $(COQ_VERSION_COMPILATION))))
VERSION_FILES := $(COQ_VERSION_FILE) $(COQ_VERSION_SHORT_FILE) $(COQ_VERSION_SHORT_DATE_FILE) $(COQ_VERSION_COMPILATION_DATE_FILE) $(COQ_VERSION_OCAML_VERSION_FILE) $(COQ_VERSION_CONFIG_FILE) $(COQ_VERSION_OCAML_CONFIG_FILE)
MACHINE_FILE = .machine
MACHINE_EXTENDED_FILE = .machine-extended
COQ_EXTENDED_VERSION := $(shell (true | $(COQBIN)coqtop 2>/dev/null; $(COQBIN)coqc --version 2>/dev/null))
COQ_EXTENDED_VERSION_OLD := $(shell cat $(COQ_VERSION_FILE) 2>/dev/null)
HAS_LTAC2:=
IS_8_9_OR_NEWER:=
IS_8_10_OR_NEWER:=
IS_8_11_OR_NEWER:=
IS_8_12_OR_NEWER:=
ifneq (,$(filter 8.8%,$(COQ_VERSION)))
EXPECTED_EXT:=.v88
else
IS_8_9_OR_NEWER:=yes
ifneq (,$(filter 8.9%,$(COQ_VERSION)))
EXPECTED_EXT:=.v89
else
IS_8_10_OR_NEWER:=yes
ifneq (,$(filter 8.10%,$(COQ_VERSION)))
EXPECTED_EXT:=.v810
else
IS_8_11_OR_NEWER:=yes
HAS_LTAC2:=yes
ifneq (,$(filter 8.11%,$(COQ_VERSION)))
EXPECTED_EXT:=.v811
else
IS_8_12_OR_NEWER:=yes
EXPECTED_EXT:=.v812
endif
endif
endif
endif
COMPATIBILITY_FILES := \
Ltac2Compat/Init.v \
Ltac2Compat/Array.v \
Ltac2Compat/Constr.v \
# end of list