use why3 1.8.0 (#1176)

Deducteam · Jan 10, 2025 · bd5ff1c · bd5ff1c
1 parent 3d1786b
commit bd5ff1c
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 8 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -8,7 +8,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        ocaml-version: [5.3.0, 5.2.1, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1]
+        ocaml-version: [5.3.0, 5.2.1, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1]
     runs-on: ubuntu-latest
     steps:
       - name: checking out lambdapi repo ...

diff --git a/dune-project b/dune-project
@@ -27,7 +27,7 @@ provides commands to export Lambdapi files to other formats or
 systems: Dedukti, Coq, HRS, CPF.")
 
  (depends
-  (ocaml (>= 4.08.0))
+  (ocaml (>= 4.09.0))
   (menhir (>= 20200624))
   (sedlex (>= 3.2))
   (alcotest :with-test)
@@ -36,7 +36,7 @@ systems: Dedukti, Coq, HRS, CPF.")
   (timed (>= 1.0))
   (pratter (and (>= 3.0.0) (< 4)))
   (camlp-streams (>= 5.0))
-  (why3 (and (>= 1.6.0) (< 1.8~)))
+  (why3 (>= 1.8.0))
   (yojson (>= 1.6.0))
   (cmdliner (>= 1.1.0))
   (stdlib-shims (>= 0.1.0))

diff --git a/lambdapi.opam b/lambdapi.opam
@@ -20,7 +20,7 @@ bug-reports: "https://github.com/Deducteam/lambdapi/issues"
 dev-repo: "git+https://github.com/Deducteam/lambdapi.git"
 depends: [
   "dune" {>= "3.7"}
-  "ocaml" {>= "4.08.0"}
+  "ocaml" {>= "4.09.0"}
   "menhir" {>= "20200624"}
   "sedlex" {>= "3.2"}
   "alcotest" {with-test}
@@ -29,7 +29,7 @@ depends: [
   "timed" {>= "1.0"}
   "pratter" {>= "3.0.0" & < "4"}
   "camlp-streams" {>= "5.0"}
-  "why3" {>= "1.6.0" & < "1.8~"}
+  "why3" {>= "1.8.0"}
   "yojson" {>= "1.6.0"}
   "cmdliner" {>= "1.1.0"}
   "stdlib-shims" {>= "0.1.0"}

diff --git a/src/handle/why3_tactic.ml b/src/handle/why3_tactic.ml
@@ -227,10 +227,10 @@ let run_task : Why3.Task.task -> Pos.popt -> string -> bool =
   in
   (* Actually run the prover. *)
   let command = prover.Why3.Whyconf.command
-  and limit = {Why3.Call_provers.empty_limit
-              with limit_time = float_of_int!timeout} in
+  and limits = {Why3.Call_provers.empty_limits
+              with limit_time = float_of_int !timeout} in
   let call =
-    Why3.Driver.prove_task ~command ~config:why3_main ~limit driver tsk in
+    Why3.Driver.prove_task ~command ~config:why3_main ~limits driver tsk in
   Why3.Call_provers.((wait_on_call call).pr_answer = Valid)
 
 (** [handle ss pos prover_name gt] runs the Why3 prover corresponding to