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
83a8c02a
Commit
83a8c02a
authored
Jun 14, 2018
by
Ralf Jung
Browse files
attempt to fix reftests for older versions of Coq
parent
339b0438
Changes
1
Hide whitespace changes
Inline
Side-by-side
Makefile.coq.local
View file @
83a8c02a
...
...
@@ -8,14 +8,20 @@ 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...
$(TESTFILES
:
.v=.vo): %.vo: %.v $(VFILES:.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"
&&
\
(
diff
-u
"tests/
$$
TEST.ref"
"
$$
TMPFILE"
||
(
rm
"tests/
$$
TEST.vo"
"
$$
TMPFILE"
&&
exit
1
))
&&
\
rm
"
$$
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"
# a target, for convenience sake, to create the .ref file with the current output
ref
:
$(TESTFILES:.v=.ref)
...
...
@@ -24,4 +30,6 @@ ref: $(TESTFILES:.v=.ref)
tests/%.ref
:
tests/%.v $(VFILES:.v=.vo)
$(SHOW)
COQTOP
[
ref]
$<
$(HIDE)TEST
=
"
$
$(
basename
-s .v
$<
)
"
&&
\
$(TIMER)
$(COQ_TEST)
$(TIMING_ARG)
$(COQFLAGS)
$(COQLIBS)
-load-vernac-source
$<
$(TIMING_EXTRA)
>
"tests/
$$
TEST.ref"
$(TIMER)
$(COQ_TEST)
$(TIMING_ARG)
$(COQFLAGS)
$(COQLIBS)
-load-vernac-source
$<
$(TIMING_EXTRA)
>
"tests/
$$
TEST.ref"
&&
\
(
$(REF_FILTER)
<
"tests/
$$
TEST.ref"
>
"tests/
$$
TEST.ref.filtered"
||
true
)
&&
\
mv
"tests/
$$
TEST.ref.filtered"
"tests/
$$
TEST.ref"
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