Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Janno
iris-coq
Commits
c0ca4709
Commit
c0ca4709
authored
Jun 19, 2018
by
Ralf Jung
Browse files
implement proper dependency tracking for test files
parent
33f0c279
Changes
1
Hide whitespace changes
Inline
Side-by-side
Makefile.coq.local
View file @
c0ca4709
# run tests
after real-all
post
-all
:
:
test
# run tests
with main build
real
-all
:
test
# the test suite
TESTFILES
=
$(
wildcard
tests/
*
.v
)
...
...
@@ -8,25 +8,32 @@ test: $(TESTFILES:.v=.vo)
.PHONY
:
test
COQ_TEST
=
$(COQTOP)
$(COQDEBUG)
-batch
-test-mode
REF_FILTER
=
egrep
-v
'(^Welcome to Coq|^Skipping rcfile loading.$$)'
# Can't use pipes because that discards error codes and dash provides no way to control that.
# Also egrep errors if it doesn't match anything, we have to ignore that.
# Oh Unix...
REF_FILTER
=
egrep
-v
'(^Welcome to Coq|^Skipping rcfile loading.$$)'
tests/.coqdeps.d
:
$(TESTFILES)
$(SHOW)
'COQDEP [tests]'
$(HIDE)$(COQDEP)
-dyndep
var
$(COQMF_COQLIBS_NOML)
$^
$(redir_if_ok)
-include
tests/.coqdeps.d
$(TESTFILES
:
.v=.vo):
%.vo: %.v $(VFILES:.v=.vo)
$(TESTFILES
:
.v=.vo):
$(SHOW)
COQTOP
[
test
]
$<
$(HIDE)TEST
=
"
$
$(
basename
-s .v
$<
)
"
&&
\
TMPFILE
=
"
$
$(mktemp)
"
&&
\
$(TIMER)
$(COQ_TEST)
$(TIMING_ARG)
$(COQFLAGS)
$(COQLIBS)
-load-vernac-source
$<
$(TIMING_EXTRA)
>
"
$$
TMPFILE"
&&
\
(
$(REF_FILTER)
<
"
$$
TMPFILE"
>
"
$$
TMPFILE.filtered"
||
true
)
&&
\
(
diff
-u
"tests/
$$
TEST.ref"
"
$$
TMPFILE.filtered"
||
rm
-f
"tests/
$$
TEST.vo"
"
$$
TMPFILE"
"
$$
TMPFILE.filtered"
)
&&
\
rm
"
$$
TMPFILE"
"
$$
TMPFILE.filtered"
rm
"
$$
TMPFILE"
"
$$
TMPFILE.filtered"
&&
\
touch
$@
# a target, for convenience sake, to create the .ref file with the current output
ref
:
$(TESTFILES:.v=.ref)
.PHONY
:
ref
# coqdep doesn't emit dependencies for these so we just depend on everything
tests/%.ref
:
tests/%.v $(VFILES:.v=.vo)
$(SHOW)
COQTOP
[
ref]
$<
$(HIDE)TEST
=
"
$
$(
basename
-s .v
$<
)
"
&&
\
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment