Commit 5f0df6ba authored by Guillaume Melquiond's avatar Guillaume Melquiond

Drop support for Coq 8.4.

Generated statements were actually ill-formed, since Coq 8.4 sometimes
interprets "A -> B <-> C" as "(A -> B) <-> C". (This bug was fixed in 8.5.)
We could print additional parentheses to work around the issue, but it is
about time we drop support for Coq 8.4 anyway.
parent 9bd7c976
......@@ -53,6 +53,7 @@ Tools
Provers
* deprecated the `why3` Coq tactic
* dropped support for Coq 8.4 :x:
Version 0.88.3, January 11, 2018
--------------------------------
......@@ -125,10 +126,10 @@ Plugins
Provers
* support for Isabelle 2017 (released Oct 2017)
* discarded support for Isabelle 2016 (2016-1 still supported) :x:
* dropped support for Isabelle 2016 (2016-1 still supported) :x:
* support for Coq 8.6.1 (released Jul 25, 2017)
* tentative support for Coq 8.7
* discarded tactic support for Coq 8.4 (proofs still supported) :x:
* dropped tactic support for Coq 8.4 (proofs still supported) :x:
* support for CVC4 1.5 (released Jul 10, 2017)
* support for E 2.0 (released Jul 4, 2017)
* support for E 1.9.1 (release Aug 31, 2016)
......@@ -144,7 +145,7 @@ Provers
* support for Alt-Ergo 1.30 (released Nov 21, 2016)
* support for Coq 8.6 (released Dec 8, 2016)
* support for Gappa 1.3 (released Jul 20, 2016)
* discarded support for Isabelle 2015 :x:
* dropped support for Isabelle 2015 :x:
* support for Isabelle 2016-1 (released Dec 2016)
* support for Z3 4.5.0 (released Nov 8, 2016)
......@@ -194,13 +195,13 @@ Encoding
format is direct :x:
Provers
* discarded support for Alt-Ergo versions older than 0.95.2 :x:
* dropped support for Alt-Ergo versions older than 0.95.2 :x:
* support for Alt-Ergo 1.01 (released Feb 16, 2016) and
non-free versions 1.10 and 1.20
* support for Coq 8.4pl6 (released Apr 9, 2015)
* support for Coq 8.5 (released Jan 21, 2016)
* support for Gappa 1.2.0 (released May 19, 2015)
* discarded support for Isabelle 2014 :x:
* dropped support for Isabelle 2014 :x:
* support for Isabelle 2015 (released May 25, 2015) and
Isabelle 2016 (released Feb 17, 2016)
* support for Z3 4.4.0 (released Apr 29, 2015) and
......@@ -378,7 +379,7 @@ Provers
* new version of prover: Coq 8.4pl3
* new version of prover: Gappa 1.1.0
* new version of prover: E prover 1.8
* Coq 8.3 is no longer supported :x:
* dropped support for Coq 8.3 :x:
* improved support for Isabelle2013-2
* fixed Coq printer (former Coq proofs may have to be updated, with
extra qualification of imported symbols) :x:
......
......@@ -667,40 +667,25 @@ if test "$enable_coq_support" = yes; then
COQLIB=`$COQC -where | sed -e 's|\\\|/|g' -e 's| |\\ |g'`
AC_MSG_CHECKING(Coq version)
COQVERSION=[`$COQC -v | sed -n -e 's|.*version *\([^ ]*\) .*$|\1|p'`]
AC_MSG_RESULT($COQVERSION)
#Even if the name of the variable is CAMLP4 the value can be camlp5
COQCAMLP=[`$COQC -config | sed -n -e 's/CAMLP[45]O=\(.*\)$/\1/p'`]
COQCAMLPLIB=[`$COQC -config | sed -n -e 's/CAMLP[45]LIB=\(.*\)$/\1/p'`]
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
case $COQVERSION in
8.4*)
coq_compat_version="COQ84"
COQPPLIBS="$COQLIB/parsing/grammar.cma"
AC_MSG_RESULT($COQVERSION)
if test "$enable_coq_tactic" = yes; then
enable_coq_tactic=no
reason_coq_tactic=" (coq >= 8.5 not found)"
fi
;;
8.5*)
coq_compat_version="COQ85"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
8.6*)
coq_compat_version="COQ86"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
8.7*)
coq_compat_version="COQ87"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
8.8*)
coq_compat_version="COQ88"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
if test "$enable_coq_tactic" = yes; then
enable_coq_tactic=no
reason_coq_tactic=" (coq <= 8.7 not found)"
......@@ -708,8 +693,8 @@ if test "$enable_coq_support" = yes; then
;;
*)
enable_coq_support=no
AC_MSG_WARN(You need Coq 8.4 or later; Coq discarded)
reason_coq_support=" (version is $COQVERSION but need version 8.4 or later)"
AC_MSG_WARN(You need Coq 8.5 or later; Coq discarded)
reason_coq_support=" (version is $COQVERSION but need version 8.5 or later)"
;;
esac
fi
......
......@@ -555,7 +555,6 @@ version_ok = "7.0"
command = "%e -noprompt"
driver = "mathematica"
# Coq 8.6: do not limit memory
[ITP coq]
name = "Coq"
support_library = "%l/coq/version"
......@@ -570,7 +569,6 @@ command = "%e -I %l/coq-tactic -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
driver = "coq"
editor = "coqide"
# Coq 8.5: do not limit memory
[ITP coq]
name = "Coq"
support_library = "%l/coq/version"
......@@ -585,18 +583,6 @@ command = "%e -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
driver = "coq"
editor = "coqide"
[ITP coq]
name = "Coq"
support_library = "%l/coq/version"
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "^8\.4pl[1-6]$"
version_ok = "8.4"
command = "%e -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
driver = "coq"
editor = "coqide"
[ITP pvs]
name = "PVS"
support_library = "%l/pvs/version"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment