Update detection and drivers for Coq 8.4 and Gappa 1.0.

drivers/gappa.drv

@@ -7,7 +7,7 @@ printer "gappa"
 filename "%f-%t-%g.gappa"
 
 valid 0
-unknown "no contradiction was found\\|some enclosures were not satisfied" ""
+unknown "no contradiction was found\\|some enclosures were not satisfied\\|some properties were not satisfied" ""
 time "why3cpulimit time : %s s"
 fail "Error: \\(.*\\)" "\\1"
 

examples/bitvectors/double_of_int/why3session.xml

@@ -24,7 +24,7 @@
  <prover
   id="5"
   name="Gappa"
-  version="0.16.6"/>
+  version="1.0.0"/>
  <prover
   id="6"
   name="Z3"

examples/bitvectors/power2/why3session.xml

@@ -20,7 +20,7 @@
  <prover
   id="4"
   name="Gappa"
-  version="0.16.6"/>
+  version="1.0.0"/>
  <prover
   id="5"
   name="Z3"

examples/bts/12475/why3session.xml

@@ -12,7 +12,7 @@
  <prover
   id="2"
   name="Gappa"
-  version="0.16.6"/>
+  version="1.0.0"/>
  <prover
   id="3"
   name="Z3"

examples/check-builtin/floats/why3session.xml

@@ -12,7 +12,7 @@
  <prover
   id="2"
   name="Gappa"
-  version="0.16.6"/>
+  version="1.0.0"/>
  <prover
   id="3"
   name="Z3"

examples/check-builtin/intreal/why3session.xml

@@ -16,7 +16,7 @@
  <prover
   id="3"
   name="Gappa"
-  version="0.16.6"/>
+  version="1.0.0"/>
  <prover
   id="4"
   name="Spass"

examples/check-builtin/real/why3session.xml

@@ -16,7 +16,7 @@
  <prover
   id="3"
   name="Gappa"
-  version="0.16.6"/>
+  version="1.0.0"/>
  <prover
   id="4"
   name="Yices"

examples/logic/my_cosine/why3session.xml

@@ -12,7 +12,7 @@
  <prover
   id="2"
   name="Gappa"
-  version="0.16.6"/>
+  version="1.0.0"/>
  <file
   name="../my_cosine.why"
   verified="true"

examples/logic/ns_clone/why3session.xml

@@ -12,7 +12,7 @@
  <prover
   id="2"
   name="Gappa"
-  version="0.16.6"/>
+  version="1.0.0"/>
  <prover
   id="3"
   name="Spass"

examples/my_cosine/why3session.xml

@@ -8,7 +8,7 @@
  <prover
   id="1"
   name="Gappa"
-  version="0.16.6"/>
+  version="1.0.0"/>
  <file
   name="../my_cosine.mlw"
   verified="true"

examples/tests-provers/gappa/why3session.xml

@@ -4,7 +4,7 @@
  <prover
   id="0"
   name="Gappa"
-  version="0.16.6"/>
+  version="1.0.0"/>
  <file
   name="../gappa.why"
   verified="true"

examples/vacid_0_binary_heaps/proofs/why3session.xml

@@ -28,7 +28,7 @@
  <prover
   id="6"
   name="Gappa"
-  version="0.16.6"/>
+  version="1.0.0"/>
  <prover
   id="7"
   name="Spass"
@@ -4502,14 +4502,6 @@
        archived="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof
-       prover="6"
-       timelimit="10"
-       memlimit="0"
-       obsolete="false"
-       archived="false">
-       <result status="valid" time="0.01"/>
-      </proof>
       <proof
        prover="7"
        timelimit="10"
@@ -4578,14 +4570,6 @@
        archived="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof
-       prover="6"
-       timelimit="10"
-       memlimit="0"
-       obsolete="false"
-       archived="false">
-       <result status="valid" time="0.00"/>
-      </proof>
       <proof
        prover="7"
        timelimit="10"

share/provers-detection-data.conf.in

@@ -168,8 +168,8 @@ exec = "gappa-0.13.0"
 exec = "gappa-0.12.3"
 version_switch = "--version"
 version_regexp = "Gappa \\([^ \n]*\\)"
-version_ok = "^0\.16\.[0-6]$"
-version_ok = "^0\.1[4-5]\..+$"
+version_ok = "^1\.0\..+$"
+version_ok = "^0\.1[4-8]\..+$"
 version_old = "^0\.1[1-3]\..+$"
 command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
 driver = "drivers/gappa.drv"
@@ -403,6 +403,9 @@ name = "Coq"
 exec = "coqtop -batch"
 version_switch = "-v"
 version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
+version_ok = "8.4pl2"
+version_ok = "8.4pl1"
+version_ok = "8.4"
 version_ok = "8.3pl4"
 version_ok = "8.3pl3"
 version_ok = "8.3pl2"