Commit d94c3df0 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Recognize Gappa 1.3.0 and update sessions to use it.

parent 62aa908c
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Gappa" version="1.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.4pl6" timelimit="60" steplimit="0" memlimit="1000"/>
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Gappa" version="1.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
......
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="1" name="Gappa" version="1.2.0" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="1" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../floats.why" expanded="true">
......
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="1" name="Gappa" version="1.2.0" timelimit="2" steplimit="0" memlimit="0"/>
<prover id="1" name="Gappa" version="1.3.0" timelimit="2" steplimit="0" memlimit="0"/>
<prover id="3" name="Spass" version="3.7" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="6" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
......
......@@ -6,7 +6,7 @@
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="7" name="Yices" version="1.0.38" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="8" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="9" name="Gappa" version="1.1.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="9" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="12" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="14" name="Z3" version="4.3.2" timelimit="3" steplimit="0" memlimit="0"/>
<file name="../real.why" expanded="true">
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Gappa" version="1.2.0" timelimit="2" steplimit="0" memlimit="0"/>
<prover id="0" name="Gappa" version="1.3.0" timelimit="2" steplimit="0" memlimit="0"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Gappa" version="1.2.0" timelimit="2" steplimit="0" memlimit="0"/>
<prover id="0" name="Gappa" version="1.3.0" timelimit="2" steplimit="0" memlimit="0"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../my_cosine.mlw" expanded="true">
......
......@@ -9,7 +9,7 @@
<prover id="12" name="Yices" version="1.0.38" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="13" name="Z3" version="3.2" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="14" name="Metis" version="2.3" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="15" name="Gappa" version="1.1.1" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="15" name="Gappa" version="1.3.0" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="16" name="Eprover" version="1.8-001" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="17" name="veriT" version="201310" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="18" name="iProver" version="0.8.1" timelimit="5" steplimit="0" memlimit="1000"/>
......
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="1" name="Gappa" version="1.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Vampire" version="0.6" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Gappa" version="1.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../gappa.why">
<theory name="TestGappa" sum="5bcac26c5f71946fa13de1d9eaef7fa5">
<goal name="Round_single_01">
......
......@@ -191,6 +191,8 @@ use_at_auto_level = 2
[ATP gappa]
name = "Gappa"
exec = "gappa"
exec = "gappa-1.3.0"
exec = "gappa-1.2.2"
exec = "gappa-1.2.0"
exec = "gappa-1.1.1"
exec = "gappa-1.1.0"
......@@ -199,7 +201,7 @@ exec = "gappa-0.16.1"
exec = "gappa-0.14.1"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "^1\.[0-2]\..+$"
version_ok = "^1\.[0-3]\..+$"
version_old = "^0\.1[1-8]\..+$"
command = "%e -Eprecision=70"
driver = "drivers/gappa.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