Adapt to why3find changes

README.md

@@ -24,14 +24,14 @@ Creusot IDE consists of two parts:
         # Say yes to install creusot-lsp
 
     Creusot LSP currently depends on development versions of Why3 and Why3find.
-    (Tested with Why3 commit `9c0548a62` and Why3find commit `1055ea5` + temporary [local patch](./why3find.patch))
+    (Tested with Why3 commit `9c0548a62` and Why3find commit `7f728e9` + temporary [local patch](./why3find.patch))
 
         git clone https://gitlab.inria.fr/why3/why3
         opam pin why3 why3#9c0548a62
 
         git clone https://git.frama-c.com/pub/why3find
         cd why3find
-        git checkout 1055ea5
+        git checkout 7f728e9
         git apply ../creusot-ide/why3find.patch
         git commit -am "patch"
         opam pin why3find .

server/lib/why3findUtil.ml

@@ -240,7 +240,7 @@ let load_plugins =
   fun env ->
     if !once then (
       once := false;
-      Why3.Whyconf.load_plugins @@ Why3.Whyconf.get_main env.Config.wconfig
+      Why3.Whyconf.load_plugins @@ Why3.Whyconf.get_main env.Config.wenv.config
     )
 
 let load_config =
@@ -268,11 +268,13 @@ let get_env () =
   env
 
 let rec path_goal_ theory (e : Why3.Env.env) (g : Session.goal) (q : ProofPath.tactic_path) breadcrumbs : Session.goal option =
+  let (let+) = Option.bind in
   match q with
   | [] -> Some g
   | (tactic, i) :: q ->
     let display_breadcrumbs () = Format.asprintf "%s:%a" theory ProofPath.pp_tactic_path (List.rev breadcrumbs) in
-    match Session.apply e tactic g with
+    let+ tactic' = Tactic.lookup e tactic in
+    match Session.apply e tactic' g with
     | None -> log Error "%s: Could not apply tactic %s" (display_breadcrumbs ()) tactic; None
     | Some gs ->
       match List.nth_opt gs i with
@@ -282,38 +284,18 @@ let rec path_goal_ theory (e : Why3.Env.env) (g : Session.goal) (q : ProofPath.t
 let path_goal ~theory (e : Why3.Env.env) (g : Session.goal) (q : ProofPath.tactic_path) : Session.goal option =
   path_goal_ theory e g q []
 
-module Wutil = struct
-  include Wutil
-  open Why3
-  (* modified from why3find without exit *)
-  let load_theories (env : Why3.Env.env) file =
-    let byloc a b =
-      match a.Theory.th_name.id_loc , b.Theory.th_name.id_loc with
-      | None,None -> 0
-      | Some _,None -> (-1)
-      | None,Some _ -> (+1)
-      | Some la, Some lb -> Why3.Loc.compare la lb
-    in
-    try
-      let tmap,format = Why3.Env.(read_file base_language env file) in
-      Some (Wstdlib.Mstr.bindings tmap |> List.map snd |> List.sort byloc , format)
-    with error ->
-      log Error "load_theories: %s" (Printexc.to_string error) ;
-      None
-end
-
 let get_goal (q : qualified_goal) : string option =
   try
     let session = true in
     let env = get_env () in
     let file = q.file in
     let dir, _lib = Wutil.filepath file in
     let (let+) = Option.bind in
-    let+ theories, format = Wutil.load_theories env.Config.wenv file in
+    let theories, format = Wutil.load_theories env.Config.wenv.env file in
     let s = Why3find.Session.create ~session ~dir ~file ~format theories in
     let+ theory = List.find_opt (fun t -> Session.name t = q.theory) (Session.theories s) in
     let+ goal = List.find_opt (fun g -> Session.goal_name g = q.goal_info.vc) (Session.split theory) in
-    let+ goal = path_goal ~theory:(Session.name theory) env.wenv goal q.goal_info.tactics in
+    let+ goal = path_goal ~theory:(Session.name theory) env.wenv.env goal q.goal_info.tactics in
     let task = Session.goal_task goal in
     Some (Format.asprintf "%a" Why3.Pretty.print_sequent task)
   with e -> log Error "get_goal: Failed to load why3: %s" (Printexc.to_string e); None

server/test/why3findtest.ml

@@ -7,11 +7,11 @@ let () =
   | [] -> Printf.eprintf "no package found in config \"why3find.json\", at least prelude is needed for creusot proofs\n"
   | _ -> ());
   let env = Config.create_env ~config () in
-  Why3.Whyconf.load_plugins @@ Why3.Whyconf.get_main env.wconfig;
+  Why3.Whyconf.load_plugins @@ Why3.Whyconf.get_main env.wenv.config;
   Why3.Loc.disable_warning @@ Why3.Loc.register_warning "axiom_abstract" Why3.Pp.empty_formatted;
   let file = Sys.argv.(1) in
   let dir, _lib = Wutil.filepath file in
-  let theories, format = Wutil.load_theories env.Config.wenv file in
+  let theories, format = Wutil.load_theories env.Config.wenv.env file in
   let s = Why3find.Session.create
     ~session
     ~dir
@@ -26,4 +26,4 @@ let () =
       let task = Session.goal_task goal in
       Printf.printf "  - TASK %s\n" (Session.task_name task);
       Printf.printf "    %s\n" (Session.task_expl task);
-      Format.printf "    task:\n%a@." Why3.Pretty.print_sequent task
+      Format.printf "    task:\n%a@." Why3.Pretty.print_sequent task