/
Makefile.variables
99 lines (76 loc) · 3.14 KB
/
Makefile.variables
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
PERF_LIB:=Rewriter.Rewriter.Examples.PerfTesting
mkfile_path := $(abspath $(lastword $(MAKEFILE_LIST)))
PERF_ABS_DIR := $(patsubst %/,%,$(dir $(mkfile_path)))
PERF_DIR := $(patsubst $(abspath .)/%,%,$(PERF_ABS_DIR))
include $(PERF_ABS_DIR)/Makefile.variables.kinds
SIZES:=$(subst |,,$(shell grep -o 'Inductive size := [^\.]*' $(PERF_ABS_DIR)/Harness.v | sed s'/Inductive size := //g'))
NO_LIMIT_PERF?=
PERF_MAX_KB?=10000000 # 10 GB
PERF_MAX_SEC?=
TIMEOUT_CMD?=
TIMEOUT_SHOW?=
PERF_SET_LIMITS?=
ifneq (,$(NO_LIMIT_PERF))
ifneq (,$(PERF_MAX_SEC))
TIMEOUT_CMD:=$(PERF_MAX_SEC)
PERF_T_ARG:=-t $(PERF_MAX_SEC) # trailing space important
else
PERF_T_ARG:=
endif
# apparently ulimit -m doesn't work anymore https://superuser.com/a/1497437/59575 / https://thirld.com/blog/2012/02/09/things-to-remember-when-using-ulimit/
PERF_SET_LIMITS = ulimit -S -m $(PERF_MAX_KB); ulimit -S -v $(PERF_MAX_KB);
TIMEOUT_SHOW:=TIMEOUT -m $(PERF_MAX_KB) $(PERF_T_ARG)
endif
get_TESTS = $(subst time_solve_goal,,$(shell grep -o 'time_solve_goal[0-9]\+' $(PERF_ABS_DIR)/$(1).v | sort -h | uniq))
ALL_PERF_LOGS := $(foreach size,$(SIZES),\
$(foreach kind,$(ALL_VKINDS),\
$(foreach test,$(call get_TESTS,$(kind)),\
$(PERF_DIR)/$(kind)/_$(test)_$(size).log))) \
\
$(foreach size,$(SIZES),\
$(foreach kind,$(SH_KINDS),\
$(PERF_DIR)/$(kind)/_$(size).log))
ALL_PERF_VFILES := $(ALL_PERF_LOGS:.log=.v)
define makekind
$(eval $(1)_PERF_LOGS := $(filter $(PERF_DIR)/$(1)/%.log,$(ALL_PERF_LOGS)))
$(eval $(1)_PERF_VFILES := $($(1)_PERF_LOGS:.log=.v))
$$($(1)_PERF_VFILES) : $(PERF_DIR)/$(1)/_%.v : $(PERF_DIR)/Template.v.in
$$(SHOW)'SED $$(<:$(PERF_DIR)/%=%) > $$(@:$(PERF_DIR)/%=%)'
$$(HIDE)mkdir -p $$(dir $$@)
$$(HIDE)sed 's/@EXAMPLE@/$(1)/g; s/@ARGS@/$$(subst _, ,$$*)/g' $$< > $$@
$$($(1)_PERF_LOGS) : %.log : %.v $(PERF_DIR)/$(1).vo
.PHONY: perf-$(1)
perf-$(1):: $($(1)_PERF_LOGS)
endef
define makekind_sh
$(eval $(1)_PERF_LOGS := $(filter $(PERF_DIR)/$(1)/%.log,$(ALL_PERF_LOGS)))
$(eval $(1)_PERF_VFILES := $($(1)_PERF_LOGS:.log=.v))
$$($(1)_PERF_VFILES) : $(PERF_DIR)/$(1)/_%.v : $(PERF_DIR)/$(1).sh
$$(SHOW)'BASH $$< $$(subst _, ,$$*) > $$@'
$$(HIDE)mkdir -p $$(dir $$@)
$$(HIDE)bash $$< $$(subst _, ,$$*) > $$@
$$($(1)_PERF_LOGS) : %.log : %.v
.PHONY: perf-$(1)
perf-$(1):: $($(1)_PERF_LOGS)
endef
define makekind_special
$(eval $(1)_PERF_LOGS := $(filter $(PERF_DIR)/$(1)/%.log,$(ALL_PERF_LOGS)))
$(eval $(1)_PERF_VFILES := $($(1)_PERF_LOGS:.log=.v))
$$($(1)_PERF_VFILES) : $(PERF_DIR)/$(1)/_%.v : $(PERF_DIR)/Template_$(1).v.in
$$(SHOW)'SED $$< > $$@'
$$(HIDE)mkdir -p $$(dir $$@)
$$(HIDE)sed 's/@EXAMPLE@/$(1)/g; s/@ARGS@/$$(subst _, ,$$*)/g' $$< > $$@
$$($(1)_PERF_LOGS) : %.log : %.v $(PERF_DIR)/$(1).vo
.PHONY: perf-$(1)
perf-$(1):: $($(1)_PERF_LOGS)
endef
define makesize
$(eval $(1)_PERF_LOGS := $(filter %_$(1).log,$(ALL_PERF_LOGS)))
$(eval $(1)_PERF_VFILES := $(filter %_$(1).v,$(ALL_PERF_VFILES)))
.PHONY: perf-$(1)
perf-$(1):: $($(1)_PERF_LOGS)
.PHONY: install-perf-$(1)
install-perf-$(1)::
+$(MAKE) -f Makefile.coq --no-print-directory install VFILES='$$($(1)_PERF_VFILES)'
+$(MAKE) -f Makefile.coq --no-print-directory install FILESTOINSTALL='$$($(1)_PERF_LOGS) $$(wildcard *.txt)'
endef