Commit ddbfb32a authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Support for Isabelle2014 and Coq8.4pl4

parent 735bf89c
......@@ -11,7 +11,7 @@ using ``Edit'' action in \texttt{why3ide}.
\subsection{Installation}
You need version Isabelle2013-2. Former versions are not supported.
You need version Isabelle2014. Former versions are not supported.
Isabelle must be installed before compiling \why. After compilation
and installation of \why, you must manually add the path
......
......@@ -80,6 +80,10 @@ why3_vc Min_comm by simp
why3_vc Min_assoc by simp
why3_vc max_def by auto
why3_vc min_def by auto
why3_end
......
......@@ -414,6 +414,7 @@ compile_time_support = true
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.4pl4"
version_ok = "8.4pl3"
version_ok = "8.4pl2"
version_ok = "8.4pl1"
......@@ -441,7 +442,8 @@ name = "Isabelle"
exec = "isabelle"
version_switch = "version"
version_regexp = "Isabelle\\([^:]+\\)"
version_ok = "2013-2"
version_ok = "2014-RC4"
version_bad = "2013-2"
# not why3-cpulimit 0 %m because isabelle needs more memory at start-up
command = "%l/why3-cpulimit 0 0 -s %e why3 -b %f"
driver = "drivers/isabelle.drv"
......
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