checksum

src/ide/db.ml

@@ -261,11 +261,7 @@ and goal = int64
 
 (** goal accessors *)
 
-let task_checksum _g = assert false
 let proved _g = assert false
-(*
-let external_proofs _g = Hprover.create 7 (* TODO !!! *)
-*)
 let transformations _g = assert false
 
 
@@ -858,6 +854,18 @@ module Goal = struct
       | [x] -> x
       | _ -> assert false
 
+  let task_checksum db g =
+    let sql="SELECT task_checksum FROM goals WHERE goals.goal_id=?"
+    in
+    let stmt = bind db sql [Sqlite3.Data.INT g] in
+    let of_stmt stmt = 
+      (stmt_column_string stmt 0 "Goal.task_checksum")
+    in
+    match step_fold db stmt of_stmt with
+      | [] -> raise Not_found
+      | [x] -> x
+      | _ -> assert false
+
   let of_theory db th =
     let sql="SELECT goal_id FROM goals \
        WHERE goals.goal_theory=?"
@@ -958,10 +966,12 @@ module Goal = struct
 end
 
 let goal_name g = Goal.name (current()) g
+let task_checksum g = Goal.task_checksum (current()) g
 
 let goals th = Goal.of_theory (current()) th
 
 
+
 (*
 
 let external_proofs g = 

src/ide/gdbmain.ml

@@ -309,7 +309,9 @@ let goals_model,filter_model,goals_view =
 
 let task_checksum t = 
   fprintf str_formatter "%a@." Pretty.print_task t;
-  Digest.to_hex (Digest.string (flush_str_formatter ()))
+  let s = flush_str_formatter () in
+  eprintf "task = %s@." s;
+  Digest.to_hex (Digest.string s)
 
 
 let info_window mt s =
@@ -385,8 +387,7 @@ module Helpers = struct
       end
     else "" 
     in
-    goals_model#set ~row:a.Model.proof_row ~column:Model.time_column t;
-    if s = Scheduler.Success then set_proved a.proof_goal              
+    goals_model#set ~row:a.Model.proof_row ~column:Model.time_column t
 
 
   let add_external_proof_row g p db_proof status time =
@@ -550,6 +551,12 @@ let () =
 		     eprintf "gname = %s, taskname = %s@." gname taskname;
 		     assert false;
 		   end;
+		 let sum = task_checksum t in
+		 let db_sum = Db.task_checksum db_goal in
+		 if sum <> db_sum then
+		   begin
+		     eprintf "bad checksum for %s: %s <> %s@." gname sum db_sum;
+		   end;		 
 		 let goal = Helpers.add_goal_row mth gname t db_goal in
                  let external_proofs = Db.external_proofs db_goal in
 		 Db.Hprover.iter
@@ -602,6 +609,7 @@ let redo_external_proof g a =
   let callback result time output =
     a.Model.output <- output;
     Helpers.set_proof_status a result time;
+    if result = Scheduler.Success then Helpers.set_proved a.Model.proof_goal;
     let db_res = match result with
       | Scheduler.Scheduled | Scheduler.Running -> Db.Undone
       | Scheduler.Success -> Db.Success

tests/test-claude.why

-
+(*
 theory TestInt
 
    use import int.Int
@@ -23,6 +23,8 @@ theory TestInt
 
 end
 
+*)
+
 theory TestDiv
 
    use import int.Int
@@ -30,6 +32,7 @@ theory TestDiv
 
    goal EDiv1: EuclideanDivision.div 1 2 = 0
 
+(*
    goal EDiv2: EuclideanDivision.div (-1) 2 = -1
 
    use int.ComputerDivision
@@ -37,9 +40,12 @@ theory TestDiv
    goal CDiv1: ComputerDivision.div 1 2 = 0
 
    goal CDiv2: ComputerDivision.div (-1) 2 = 0
+*)
 
 end
 
+(*
+
 theory TestReal
 
    use import real.Real
@@ -51,6 +57,7 @@ theory TestReal
    goal RealAbs1: forall x:real. 100.0 >= abs x >= 1.0 -> x*x >= 1.0
 
 end
+*)
 
 theory TestFloat
 
@@ -62,6 +69,8 @@ theory TestFloat
 end
 
 
+(*
+
 theory TestList
 
   use import int.Int
@@ -77,3 +86,4 @@ theory TestList
      end  
 
 end  
+*)