Skip to content

Commit

Permalink
Build: Support TIMING and PROFILING like coq_makefile (#512)
Browse files Browse the repository at this point in the history
Should be useful to identify changes more precisely in the Coq benchmarking.
  • Loading branch information
SkySkimmer authored Jul 3, 2024
1 parent 8f5fd33 commit afb7fd2
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 0 deletions.
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,9 @@
*.vok
*.vos
*.glob
*.timing
*.prof.json
*.prof.json.gz
*.o
*.a
*.cmi
Expand Down
18 changes: 18 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,23 @@ COQCOPTS ?= \
cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality
flocq/IEEE754/Bits.vo: COQCOPTS += -w -opaque-let

ifneq (,$(TIMING))
# does this coq version support -time-file ? (Coq >= 8.18)
ifeq (,$(shell "$(COQBIN)coqc" -time-file /dev/null 2>&1))
COQCOPTS += -time-file $<.timing
endif
endif

ifneq (,$(PROFILING))
# does this coq version dupport -profile ? (Coq >= 8.19)
ifeq (,$(shell "$(COQBIN)coqc" -profile /dev/null 2>&1))
COQCOPTS += -profile $<.prof.json
PROFILE_ZIP = gzip -f $<.prof.json
else
endif
endif
PROFILE_ZIP ?= true

COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
COQDOC="$(COQBIN)coqdoc"
Expand Down Expand Up @@ -262,6 +279,7 @@ latexdoc:
@rm -f doc/$(*F).glob
@echo "COQC $*.v"
@$(COQC) -dump-glob doc/$(*F).glob $*.v
@$(PROFILE_ZIP)

%.v: %.vp tools/ndfun
@rm -f $*.v
Expand Down

0 comments on commit afb7fd2

Please sign in to comment.