avoid silent failures in presence of detached theories

src/ide/why3ide.ml

@@ -1133,6 +1133,8 @@ let on_selected_row r =
           task_view#source_buffer#set_text "Unedited"
       | Controller_itp.JustEdited ->
           task_view#source_buffer#set_text "Just edited"
+      | Controller_itp.Detached ->
+          task_view#source_buffer#set_text "Detached"
       | Controller_itp.Interrupted ->
           task_view#source_buffer#set_text "Interrupted"
       | Controller_itp.Scheduled ->
@@ -1374,6 +1376,7 @@ let image_of_pa_status ~obsolete pa =
   | Controller_itp.Scheduled -> !image_scheduled
   | Controller_itp.Running -> !image_running
   | Controller_itp.InternalFailure _e -> !image_failure
+  | Controller_itp.Detached -> !image_undone (* TODO !image_detached *)
   | Controller_itp.Uninstalled _p -> !image_undone (* TODO !image_uninstalled *)
   | Controller_itp.Done r ->
     let pr_answer = r.Call_provers.pr_answer in
@@ -1465,6 +1468,7 @@ let set_status_and_time_column ?limit row =
         | C.Uninstalled _ -> "(uninstalled prover)"
         | C.Scheduled -> "(scheduled)"
         | C.Running -> "(running)"
+        | C.Detached -> "(detached)"
       in
       let t = match pa with
         | C.Scheduled | C.Running ->

src/session/controller_itp.ml

@@ -31,19 +31,21 @@ let () = Exn_printer.register
 
 (** State of a proof *)
 type proof_attempt_status =
-    | Unedited (** editor not yet run for interactive proof *)
-    | JustEdited (** edited but not run yet *)
-    | Interrupted (** external proof has never completed *)
-    | Scheduled (** external proof attempt is scheduled *)
-    | Running (** external proof attempt is in progress *)
-    | Done of Call_provers.prover_result (** external proof done *)
-    | InternalFailure of exn (** external proof aborted by internal error *)
-    | Uninstalled of Whyconf.prover (** prover is uninstalled *)
+  | Unedited (** editor not yet run for interactive proof *)
+  | JustEdited (** edited but not run yet *)
+  | Detached (** parent goal has no task, is detached *)
+  | Interrupted (** external proof has never completed *)
+  | Scheduled (** external proof attempt is scheduled *)
+  | Running (** external proof attempt is in progress *)
+  | Done of Call_provers.prover_result (** external proof done *)
+  | InternalFailure of exn (** external proof aborted by internal error *)
+  | Uninstalled of Whyconf.prover (** prover is uninstalled *)
 
 let print_status fmt st =
   match st with
   | Unedited          -> fprintf fmt "Unedited"
   | JustEdited        -> fprintf fmt "JustEdited"
+  | Detached          -> fprintf fmt "Detached"
   | Interrupted       -> fprintf fmt "Interrupted"
   | Scheduled         -> fprintf fmt "Scheduled"
   | Running           -> fprintf fmt "Running"
@@ -143,10 +145,7 @@ module PSession = struct
     | Session -> "", Hstr.fold (fun _ f -> n (File f)) (get_files s) []
     | File f ->
        (file_name f),
-       List.fold_right
-          (fun th -> n (Theory th))
-          (file_detached_theories f)
-          (List.fold_right (fun th -> n (Theory th)) (file_theories f) [])
+       List.fold_right (fun th -> n (Theory th)) (file_theories f) []
     | Theory th ->
        let id = theory_name th in
        let name = id.Ident.id_string in
@@ -313,13 +312,16 @@ let build_prover_call ?proof_script ~cntexample c id pr limit callback ores =
   let with_steps = Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
   let command =
     Whyconf.get_complete_command config_pr ~with_steps in
-  let task = Session_itp.get_raw_task c.controller_session id in
-  let call =
-    Driver.prove_task ?old:proof_script ~cntexample:cntexample ~inplace:false ~command
-                      ~limit (*?name_table:table*) driver task
-  in
-  let pa = (c.controller_session,id,pr,proof_script,callback,false,call,ores) in
-  Queue.push pa prover_tasks_in_progress
+  try
+    let task = Session_itp.get_raw_task c.controller_session id in
+    let call =
+      Driver.prove_task ?old:proof_script ~cntexample:cntexample ~inplace:false ~command
+                        ~limit (*?name_table:table*) driver task
+    in
+    let pa = (c.controller_session,id,pr,proof_script,callback,false,call,ores) in
+    Queue.push pa prover_tasks_in_progress
+  with Not_found (* goal has no task, it is detached *) ->
+       callback Detached
 
 let update_observer () =
   let scheduled = Queue.length scheduled_proof_attempts in
@@ -492,7 +494,11 @@ let replay_proof_attempt ?proof_script c pr limit (parid: proofNodeID) id ~callb
   match find_prover notification c parid pr with
   | None -> callback id (Uninstalled pr)
   | Some pr ->
-     schedule_proof_attempt ?proof_script c parid pr ~counterexmp:false ~limit ~callback ~notification
+     try
+       let _ = get_raw_task c.controller_session parid in
+       schedule_proof_attempt ?proof_script c parid pr ~counterexmp:false ~limit ~callback ~notification
+     with Not_found ->
+       callback id Detached
 
 
 (* TODO to be simplified *)
@@ -683,7 +689,7 @@ let run_strategy_on_goal
               callback (STSgoto (g,pc+1));
               let run_next () = exec_strategy (pc+1) strat g; false in
               S.idle ~prio:0 run_next
-           | Unedited | JustEdited | Uninstalled _ ->
+           | Unedited | JustEdited | Detached | Uninstalled _ ->
                          (* should not happen *)
                          assert false
          in
@@ -890,6 +896,7 @@ let replay ?(obsolete_only=true) ?(use_steps=false)
     | Uninstalled _ ->
        decr count;
        r := (id, pr, limits, Prover_not_installed) :: !r;
+    | Detached -> decr count
   in
 
   let session = c.controller_session in
@@ -956,7 +963,7 @@ let bisect_proof_attempt ~notification c pa_id =
     | Interrupted ->
       Debug.dprintf debug "Bisecting interrupted.@."
     | Unedited | JustEdited -> assert false
-    | Uninstalled _ -> assert false
+    | Detached | Uninstalled _ -> assert false
     | InternalFailure exn ->
       (* Perhaps the test can be considered false in this case? *)
       Debug.dprintf debug "Bisecting interrupted by an error %a.@."
@@ -995,7 +1002,7 @@ let bisect_proof_attempt ~notification c pa_id =
             Exn_printer.exn_printer e end
  *)
            end
-      | Eliminate_definition.BSstep (rem,kont) ->
+      | Eliminate_definition.BSstep (_rem,kont) ->
 
          schedule_proof_attempt
            c goal_id prover
@@ -1006,12 +1013,12 @@ let bisect_proof_attempt ~notification c pa_id =
   in
   (* Run once the complete goal in order to verify its validity and
      update the proof attempt *)
-  let first_callback pa_id = function
+  let first_callback _pa_id = function
     (* this pa_id can be different from the first pa_id *)
     | Running | Scheduled -> ()
     | Interrupted ->
       Debug.dprintf debug "Bisecting interrupted.@."
-    | Unedited | JustEdited | Uninstalled _ -> assert false
+    | Unedited | JustEdited | Detached | Uninstalled _ -> assert false
     | InternalFailure exn ->
         Debug.dprintf debug "proof of the initial task interrupted by an error %a.@."
           Exn_printer.exn_printer exn
@@ -1022,9 +1029,9 @@ let bisect_proof_attempt ~notification c pa_id =
         let t = get_raw_task ses goal_id in
         let r = Eliminate_definition.bisect_step t in
         match r with
-        | Eliminate_definition.BSdone res ->
+        | Eliminate_definition.BSdone _res ->
           Debug.dprintf debug "Task can't be reduced.@."
-        | Eliminate_definition.BSstep (rem,kont) ->
+        | Eliminate_definition.BSstep (_rem,kont) ->
           set_timelimit res;
           schedule_proof_attempt
             c goal_id prover

src/session/controller_itp.mli

@@ -19,6 +19,7 @@ open Session_itp
 type proof_attempt_status =
     | Unedited (** editor not yet run for interactive proof *)
     | JustEdited (** edited but not run yet *)
+    | Detached (** parent goal has no task, is detached *)
     | Interrupted (** external proof has never completed *)
     | Scheduled (** external proof attempt is scheduled *)
     | Running (** external proof attempt is in progress *)

src/session/json_util.ml

@@ -83,6 +83,8 @@ let convert_proof_attempt (pas: proof_attempt_status) =
       convert_record ["proof_attempt", String "Interrupted"]
   | Scheduled ->
       convert_record ["proof_attempt", String "Scheduled"]
+  | Detached ->
+      convert_record ["proof_attempt", String "Detached"]
   | Running ->
       convert_record ["proof_attempt", String "Running"]
   | Done pr ->

src/session/session_itp.ml

@@ -21,6 +21,8 @@ let debug = Debug.register_info_flag "session_itp"
     ~desc:"Pring@ debugging@ messages@ about@ Why3@ session@ \
            creation,@ reading@ and@ writing."
 
+let debug_merge = Debug.lookup_flag "session_pairing"
+
 let debug_stack_trace = Debug.lookup_flag "stack_trace"
 
 type transID = int
@@ -37,6 +39,7 @@ type theory = {
   theory_name                   : Ident.ident;
   theory_goals                  : proofNodeID list;
   theory_parent_name            : string;
+  theory_is_detached            : bool;
   mutable theory_detached_goals : proofNodeID list;
   mutable theory_checksum       : Termcode.checksum option;
 }
@@ -79,13 +82,11 @@ type file = {
   file_name              : string;
   file_format            : string option;
   mutable file_theories          : theory list;
-  mutable file_detached_theories : theory list;
 }
 
 let file_name f = f.file_name
 let file_format f = f.file_format
 let file_theories f = f.file_theories
-let file_detached_theories f = f.file_detached_theories
 
 type any =
   | AFile of file
@@ -278,13 +279,14 @@ let get_detached_trans (_s: session) (_id: proofNodeID) =
 let is_detached (s: session) (a: any) =
   match a with
   | AFile _file -> false
-  | ATh th     ->
-     let parent_name = th.theory_parent_name in
+  | ATh th     -> th.theory_is_detached
+                  (*
+      let parent_name = th.theory_parent_name in
      begin
        try let parent = Hstr.find s.session_files parent_name in
            List.exists (fun x -> x = th) parent.file_detached_theories
        with Not_found -> true
-     end
+     end*)
   | ATn tn     ->
     let pn_id = get_trans_parent s tn in
     let _pn = get_proofNode s pn_id in
@@ -1122,6 +1124,7 @@ let load_theory session parent_name old_provers acc th =
         | _ -> goals) [] th.Xml.elements) in
     let mth = { theory_name = thname;
                 theory_checksum = checksum;
+                theory_is_detached = false;
                 theory_goals = goals;
                 theory_parent_name = parent_name;
                 theory_detached_goals = [] } in
@@ -1145,7 +1148,7 @@ let load_file session old_provers f =
     let mf = { file_name = fn;
                file_format = fmt;
                file_theories = ft;
-               file_detached_theories = [] } in
+             } in
     Hstr.add session.session_files fn mf;
     old_provers
   | "prover" ->
@@ -1395,6 +1398,7 @@ let save_detached_theory parent_name old_s detached_theory s =
     (* List.map (fun _ -> gen_proofNodeID s) detached_theory.theory_goals in *)
   { theory_name = detached_theory.theory_name;
     theory_checksum = None;
+    theory_is_detached = true;
     theory_goals = goalsID;
     theory_parent_name = parent_name;
     theory_detached_goals = [] }
@@ -1566,6 +1570,7 @@ let make_theory_section ?merge (s:session) parent_name (th:Theory.theory)
   let goalsID = List.map (fun _ -> gen_proofNodeID s) tasks in
   let theory = { theory_name = th.Theory.th_name;
                  theory_checksum = None;
+                 theory_is_detached = false;
                  theory_goals = goalsID;
                  theory_parent_name = parent_name;
                  theory_detached_goals = [] } in
@@ -1592,8 +1597,7 @@ let add_file_section (s:session) (fn:string)
   else
     let f = { file_name = fn;
               file_format = format;
-              file_theories = [];
-              file_detached_theories = [] }
+              file_theories = [] }
     in
     Hstr.add s.session_files fn f;
     let theories = List.map (make_theory_section s fn) theories in
@@ -1605,6 +1609,7 @@ let add_file_section (s:session) (fn:string)
 let merge_file_section ~use_shapes ~old_ses ~old_theories ~env
     (s:session) (fn:string) (theories:Theory.theory list) format
     : unit =
+  Debug.dprintf debug_merge "[Session_itp.merge_file_section] fn = %s@." fn;
   let f = add_file_section s fn [] format in
   let fn = f.file_name in
   let theories,detached =
@@ -1613,15 +1618,18 @@ let merge_file_section ~use_shapes ~old_ses ~old_theories ~env
       (fun th -> Hstr.add old_th_table th.theory_name.Ident.id_string th)
       old_theories;
     let add_theory (th: Theory.theory) =
+      (* look for a theory with same name *)
+      let theory_name = th.Theory.th_name.Ident.id_string in
       try
-        (* look for a theory with same name *)
-        let theory_name = th.Theory.th_name.Ident.id_string in
         (* if we found one, we remove it from the table and merge it *)
         let old_th = Hstr.find old_th_table theory_name in
+        Debug.dprintf debug_merge "[Session_itp.merge_file_section] theory found: %s@." theory_name;
         Hstr.remove old_th_table theory_name;
         make_theory_section ~merge:(old_ses,old_th,env,use_shapes) s fn th
       with Not_found ->
         (* if no theory was found we make a new theory section *)
+        found_detached := true;
+        Debug.dprintf debug_merge "[Session_itp.merge_file_section] theory NOT FOUND in old session: %s@." theory_name;
         make_theory_section s fn th
     in
     let theories = List.map add_theory theories in
@@ -1632,8 +1640,7 @@ let merge_file_section ~use_shapes ~old_ses ~old_theories ~env
                      old_th_table [] in
     theories, detached
   in
-  f.file_theories <- theories;
-  f.file_detached_theories <- detached;
+  f.file_theories <- theories @ detached;
   update_file_node (fun _ -> ()) s f
 
 

src/session/session_itp.mli

@@ -62,7 +62,6 @@ val get_shape_version : session -> int
 val file_name : file -> string
 val file_format : file -> string option
 val file_theories : file -> theory list
-val file_detached_theories : file -> theory list
 
 (** Theory *)
 val theory_name : theory -> Ident.ident

src/tools/why3replay.ml

@@ -378,7 +378,7 @@ let () =
     in
  *)
     if found_obs then eprintf "[Warning] session is obsolete@.";
-    if found_detached then eprintf "[Warning] found detached goals ot theories or transformations@.";
+    if found_detached then eprintf "[Warning] found detached goals or theories or transformations@.";
     add_to_check_no_smoke found_detached found_obs cont;
     Debug.dprintf debug "[Replay] starting scheduler@.";
     Unix_scheduler.Unix_scheduler.main_loop ~prompt:"" (fun _ -> ());