Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Tej Chajed
stdpp
Commits
4fb641ed
Commit
4fb641ed
authored
Jul 23, 2018
by
Ralf Jung
Browse files
mark Coq 8.9 as broken
parent
1b26babe
Changes
1
Hide whitespace changes
Inline
Side-by-side
Makefile.coq.local
View file @
4fb641ed
...
@@ -8,6 +8,7 @@ test: $(TESTFILES:.v=.vo)
...
@@ -8,6 +8,7 @@ test: $(TESTFILES:.v=.vo)
.PHONY
:
test
.PHONY
:
test
COQ_TEST
=
$(COQTOP)
$(COQDEBUG)
-batch
-test-mode
COQ_TEST
=
$(COQTOP)
$(COQDEBUG)
-batch
-test-mode
COQ_BROKEN
=
$(
shell
echo
"
$(COQ_VERSION)
"
| egrep
"^8
\.
9
\b
"
>
/dev/null
&&
echo
1
)
# Can't use pipes because that discards error codes and dash provides no way to control that.
# 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.
# Also egrep errors if it doesn't match anything, we have to ignore that.
...
@@ -20,13 +21,17 @@ tests/.coqdeps.d: $(TESTFILES)
...
@@ -20,13 +21,17 @@ tests/.coqdeps.d: $(TESTFILES)
-include
tests/.coqdeps.d
-include
tests/.coqdeps.d
$(TESTFILES
:
.v=.vo): %.vo: %.v $(if $(MAKE_REF)
,,
%.ref)
$(TESTFILES
:
.v=.vo): %.vo: %.v $(if $(MAKE_REF)
,,
%.ref)
$(SHOW)
$(
if
$(MAKE_REF)
,COQTEST
[
ref],
COQTEST
)
$<
$(SHOW)
$(
if
$(MAKE_REF)
,COQTEST
[
ref],
$(
if
$(COQ_BROKEN)
,COQTEST
[
ignored],COQTEST
)
)
$<
$(HIDE)TEST
=
"
$
$(
basename
-s .v
$<
)
"
&&
\
$(HIDE)TEST
=
"
$
$(
basename
-s .v
$<
)
"
&&
\
TMPFILE
=
"
$
$(mktemp)
"
&&
\
TMPFILE
=
"
$
$(mktemp)
"
&&
\
$(TIMER)
$(COQ_TEST)
$(COQFLAGS)
$(COQLIBS)
-load-vernac-source
$<
>
"
$$
TMPFILE"
&&
\
$(TIMER)
$(COQ_TEST)
$(COQFLAGS)
$(COQLIBS)
-load-vernac-source
$<
>
"
$$
TMPFILE"
&&
\
(
$(REF_FILTER)
<
"
$$
TMPFILE"
>
"
$$
TMPFILE.filtered"
||
true
)
&&
\
(
$(REF_FILTER)
<
"
$$
TMPFILE"
>
"
$$
TMPFILE.filtered"
||
true
)
&&
\
$(
if
$(MAKE_REF)
,
\
$(
if
$(MAKE_REF)
,
\
mv
"
$$
TMPFILE.filtered"
"tests/
$$
TEST.ref"
,
\
mv
"
$$
TMPFILE.filtered"
"tests/
$$
TEST.ref"
,
\
diff
-u
"tests/
$$
TEST.ref"
"
$$
TMPFILE.filtered"
)
&&
\
$(
if
$(COQ_BROKEN)
,
\
true
,
\
diff
-u
"tests/
$$
TEST.ref"
"
$$
TMPFILE.filtered"
\
)
\
)
&&
\
rm
-f
"
$$
TMPFILE"
"
$$
TMPFILE.filtered"
&&
\
rm
-f
"
$$
TMPFILE"
"
$$
TMPFILE.filtered"
&&
\
touch
$@
touch
$@
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a 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