Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
CertiCompil
CompCert-KVX
Commits
e87f2457
Commit
e87f2457
authored
Nov 14, 2020
by
Xavier Leroy
Browse files
Support Coq 8.12.1
parent
dc270187
Changes
2
Hide whitespace changes
Inline
Side-by-side
Changelog
View file @
e87f2457
...
...
@@ -35,7 +35,7 @@ The clightgen tool:
logical assertions, which was never used and possibly confusing.
Coq and OCaml development:
- Compatibility with Coq 8.12.0, 8.11.2, 8.11.1.
- Compatibility with Coq
8.12.1,
8.12.0, 8.11.2, 8.11.1.
- Can use already-installed Flocq and MenhirLib libraries instead of their
local copies (options `-use-external-Flocq` and `-use-external-MenhirLib`
to the `configure` script).
...
...
configure
View file @
e87f2457
...
...
@@ -527,14 +527,14 @@ missingtools=false
echo
"Testing Coq... "
|
tr
-d
'\n'
coq_ver
=
$(
${
COQBIN
}
coqc
-v
2>/dev/null |
sed
-n
-e
's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p'
)
case
"
$coq_ver
"
in
8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0
)
8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0
|8.12.1
)
echo
"version
$coq_ver
-- good!"
;;
?
*
)
echo
"version
$coq_ver
-- UNSUPPORTED"
if
$ignore_coq_version
;
then
echo
"Warning: this version of Coq is unsupported, proceed at your own risks."
else
echo
"Error: CompCert requires a version of Coq between 8.8.0 and 8.12.
0
"
echo
"Error: CompCert requires a version of Coq between 8.8.0 and 8.12.
1
"
missingtools
=
true
fi
;;
""
)
...
...
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