manager debugging

src/manager/db.ml

@@ -38,28 +38,39 @@ let current () =
 	      
 
 let default_busyfn (_db:Sqlite3.db) =
-  print_endline "WARNING: busy";
+  prerr_endline "Db.default_busyfn WARNING: busy";
   (* Thread.delay (Random.float 1.) *)
   ignore (Unix.select [] [] [] (Random.float 1.))
   
 let raise_sql_error x = raise (Sqlite3.Error (Rc.to_string x))
   
+(*
 let try_finally fn finalfn =
   try
     let r = fn () in
     finalfn ();
     r
   with e -> begin
-    Format.eprintf "WARNING: exception: %s@." (Printexc.to_string e);
+    prerr_string "Db.try_finally WARNING: exception: ";
+    prerr_endline (Printexc.to_string e);
+    prerr_endline "== exception backtrace ==";
+    Printexc.print_backtrace stderr;
+    prerr_endline "== end of backtrace ==";
     finalfn ();
     raise e
   end
+*)
   
 (* retry until a non-BUSY error code is returned *)
 let rec db_busy_retry db fn =
   match fn () with
-    | Rc.BUSY -> db.busyfn db.raw_db; db_busy_retry db fn
-    | x -> x
+    | Rc.BUSY -> 
+        prerr_endline "Db.db_busy_retry: BUSY";
+        db.busyfn db.raw_db; db_busy_retry db fn
+    | x -> 
+        prerr_string "Db.db_busy_retry: ";
+        prerr_endline (Rc.to_string x);
+        x
        
 (* make sure an OK is returned from the database *)
 let db_must_ok db fn =
@@ -80,19 +91,28 @@ let transaction db fn =
     | Immediate -> "IMMEDIATE" 
     | Exclusive -> "EXCLUSIVE" 
   in
-  try_finally 
-    (fun () ->
-       if db.in_transaction = 0 then 
-         db_must_ok db 
-           (fun () -> exec db.raw_db ("BEGIN " ^ m ^ " TRANSACTION"));
-       db.in_transaction <- db.in_transaction + 1;
-       fn ();
-    ) 
-    (fun () ->
-       if db.in_transaction = 1 then 
-         db_must_ok db (fun () -> exec db.raw_db "END TRANSACTION");
-       db.in_transaction <- db.in_transaction - 1
-    )
+  try 
+    db_must_ok db 
+      (fun () -> exec db.raw_db ("BEGIN " ^ m ^ " TRANSACTION"));
+    assert (db.in_transaction = 0);
+    db.in_transaction <- 1;
+    let res = fn () in
+    db_must_ok db (fun () -> exec db.raw_db "END TRANSACTION");
+    assert (db.in_transaction = 1);
+    db.in_transaction <- 0;
+    res
+  with
+      e ->
+        prerr_string "Db.transaction WARNING: exception: ";
+        prerr_endline (Printexc.to_string e);
+        prerr_endline "== exception backtrace ==";
+        Printexc.print_backtrace stderr;
+        prerr_endline "== end of backtrace ==";
+        db_must_ok db (fun () -> exec db.raw_db "END TRANSACTION");
+        assert (db.in_transaction = 1);
+        db.in_transaction <- 0;
+        raise e
+    
   
 (* iterate over a result set *)
 let step_fold db stmt iterfn =
@@ -600,6 +620,7 @@ module External_proof = struct
 
 
   let set_status db e stat =
+    try
       transaction db 
         (fun () ->
 	   let id = e.external_proof_id in
@@ -612,6 +633,10 @@ module External_proof = struct
            ]
            in
 	   db_must_done db (fun () -> Sqlite3.step stmt))
+    with e ->
+      Format.eprintf "External_proof.set_status raised an exception %s@."
+        (Printexc.to_string e)
+      
     
   let set_result_time db e t =
       transaction db 
@@ -1058,7 +1083,7 @@ let init_db ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
 
     | Some _ -> failwith "Db.init_db: already opened"
 
-let init_base f = init_db f
+let init_base f = init_db ~mode:Exclusive f
 
 let root_goals () = 
   let db = current () in
@@ -1098,10 +1123,10 @@ let try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver
   in
   if debug then Format.printf "setting attempt status to Scheduled@.";
   External_proof.set_status db attempt Scheduled;
-  if debug then Format.eprintf "Task : %a@." Why.Pretty.print_task g.task;
+  if false && debug then Format.eprintf "Task : %a@." Why.Pretty.print_task g.task;
   let callback = 
     try 
-      if debug then 
+      if false && debug then 
         Format.eprintf "Task for prover: %a@." 
           (Why.Prover.print_task driver) g.task;
       Why.Prover.prove_task ~debug ~command ~timelimit ~memlimit driver g.task

src/manager/db.mli

@@ -103,9 +103,7 @@ val goal_name : goal -> string
   val parent : goal -> transf option
 *)
 
-(*
 val goal_task : goal -> Task.task
-*)
 val goal_task_checksum: goal -> string
 val external_proofs : goal -> external_proof list
   (** returns the set of external proof attempt for that goal *)

src/manager/gmanager.ml

@@ -169,6 +169,17 @@ let provers_data =
   in
   printf "@\n===============================@.";
   l 
+
+let alt_ergo = 
+  match
+    List.fold_left
+      (fun acc p ->
+         if Db.prover_name p.prover = "Alt-Ergo" then Some p else acc)
+      None provers_data
+  with
+    | None -> assert false
+    | Some p -> p
+
    
 let () = 
   printf "previously known goals:@\n";
@@ -220,29 +231,27 @@ module Ide_goals = struct
 
   let clear model = model#clear ()
 
-  let task_table = Ident.Hid.create 17
+  let goal_table = Ident.Hid.create 17
 
-  let get_task = Ident.Hid.find task_table
+  let get_goal id = fst (Ident.Hid.find goal_table id)
 
   let add_goals (model : GTree.tree_store) th =
+    let tname = th.Theory.th_name.Ident.id_string in
+    let parent = model#append () in
+    model#set ~row:parent ~column:name_column tname;
+    model#set ~row:parent ~column:id_column th.Theory.th_name;
     let tasks = Task.split_theory th None in
     List.iter
       (fun t->
-         let name = (Task.task_goal t).Decl.pr_name in
-         Ident.Hid.add task_table name t)
-      tasks;
-    let rec fill parent ns =
-      let add_s s symb = 
-	let row = model#append ~parent () in
-	model#set ~row ~column:name_column s;
-	model#set ~row ~column:id_column symb.Decl.pr_name;
-      in
-      Theory.Mnm.iter add_s ns.Theory.ns_pr;
-    in
-    let row = model#append () in
-    model#set ~row ~column:name_column th.Theory.th_name.Ident.id_string;
-    model#set ~row ~column:id_column th.Theory.th_name;
-    fill row th.Theory.th_export
+         let id = (Task.task_goal t).Decl.pr_name in
+         let name = id.Ident.id_string in
+         let g = Db.add_or_replace_task ~tname ~name t in
+	 let row = model#append ~parent () in
+         Ident.Hid.add goal_table id (g,row);
+	 model#set ~row ~column:name_column name;
+	 model#set ~row ~column:id_column id;
+      )
+      tasks
 
 end
 
@@ -265,8 +274,8 @@ let select_goals (goals_view:GTree.tree_store) (task_view:GSourceView2.source_vi
        let row = goals_view#get_iter p in
        let id = goals_view#get ~row ~column:Ide_goals.id_column in
        Format.eprintf "You clicked on %s@." id.Ident.id_string;
-       let t = Ide_goals.get_task id in
-       let task_text = Pp.string_of Pretty.print_task t in
+       let g = Ide_goals.get_goal id in
+       let task_text = Pp.string_of Pretty.print_task (Db.goal_task g) in
        task_view#source_buffer#set_text task_text;
        task_view#scroll_to_mark `INSERT
 
@@ -279,9 +288,26 @@ let select_goals (goals_view:GTree.tree_store) (task_view:GSourceView2.source_vi
     )
     selected_rows
 
+let count = ref 0
+
 let alt_ergo_on_all_goals () =
-  begin
-  end
+  Ident.Hid.iter
+    (fun id (g,_row) ->
+       Format.eprintf "running Alt-Ergo on goal %s@." id.Ident.id_string;
+       incr count;
+       let c = !count in
+       let callback result =
+         printf "Scheduled task #%d: status set to %a@." c
+           Db.print_status result
+       in
+       let p = alt_ergo in
+       Scheduler.schedule_proof_attempt
+         ~debug:true ~timelimit ~memlimit:0 
+         ~prover:p.prover ~command:p.command ~driver:p.driver 
+         ~callback
+         g
+    )
+    Ide_goals.goal_table
 
 let main () =
   let w = GWindow.window