Commit 4b70dbb2 authored by MARCHE Claude's avatar MARCHE Claude

edited file name

parent fad927e8
......@@ -160,7 +160,6 @@ Theorem WP_my_cosine : forall (x:single),
((Rabs (value x)) <= (1 / 32)%R)%R ->
((Rabs (((1)%R - (((value x) * (value x))%R * (05 / 10)%R)%R)%R - (cos (value x)))%R) <= (1 / 16777216)%R)%R.
(* YOU MAY EDIT THE PROOF BELOW *)
intros x Hx.
Require Import Interval_tactic.
interval with (i_bisect_diff (value x)).
Qed.
......
......@@ -486,14 +486,15 @@ module External_proof = struct
let init db =
let sql =
(* timelimit INTEGER, memlimit INTEGER,
edited_as TEXT, *)
*)
"CREATE TABLE IF NOT EXISTS external_proofs \
(external_proof_id INTEGER PRIMARY KEY AUTOINCREMENT,\
goal_id INTEGER,\
prover_id INTEGER, \
status INTEGER,\
obsolete INTEGER,\
time REAL);"
time REAL,\
edited_as TEXT);"
in
db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)
......@@ -510,7 +511,7 @@ module External_proof = struct
let add db (g : goal) (p: prover_id) =
transaction db
(fun () ->
let sql = "INSERT INTO external_proofs VALUES(NULL,?,?,0,0,0.0)" in
let sql = "INSERT INTO external_proofs VALUES(NULL,?,?,0,0,0.0,\"\")" in
let stmt = bind db sql [
Sqlite3.Data.INT g;
Sqlite3.Data.INT p.prover_id;
......@@ -557,6 +558,19 @@ module External_proof = struct
in
db_must_done db (fun () -> Sqlite3.step stmt))
let set_edited_as db e f =
transaction db
(fun () ->
let sql =
"UPDATE external_proofs SET edited_as=? WHERE external_proof_id=?"
in
let stmt = bind db sql [
Sqlite3.Data.TEXT f;
Sqlite3.Data.INT e;
]
in
db_must_done db (fun () -> Sqlite3.step stmt))
let of_goal db g =
let sql="SELECT prover_id,external_proof_id FROM external_proofs \
WHERE external_proofs.goal_id=?"
......@@ -572,7 +586,7 @@ module External_proof = struct
res
let status_and_time db p =
let sql="SELECT status,time,obsolete FROM external_proofs \
let sql="SELECT status,time,obsolete,edited_as FROM external_proofs \
WHERE external_proofs.external_proof_id=?"
in
let stmt = bind db sql [Sqlite3.Data.INT p] in
......@@ -580,7 +594,8 @@ module External_proof = struct
let status = stmt_column_INT stmt 0 "External_proof.status_and_time" in
let t = stmt_column_FLOAT stmt 1 "External_proof.status_and_time" in
let o = stmt_column_bool stmt 2 "External_proof.status_and_time" in
(status_from_int64 status, t, o)
let e = stmt_column_string stmt 3 "External_proof.status_and_time" in
(status_from_int64 status, t, o, e)
in
match step_fold db stmt of_stmt with
| [] -> raise Not_found
......@@ -898,7 +913,8 @@ let set_status a r t =
let set_obsolete a =
External_proof.set_obsolete (current()) a
let set_edited_as _ = assert false
let set_edited_as a f =
External_proof.set_edited_as (current()) a f
let add_transformation g tr_id = Transf.add (current()) g tr_id
......@@ -913,6 +929,6 @@ let add_file f = Main.add (current()) f
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/whydb.byte"
compile-command: "unset LANG; make -C ../.. bin/whyide.byte"
End:
*)
......@@ -80,8 +80,9 @@ val prover : proof_attempt -> prover_id
(*
val proof_goal : proof_attempt -> goal
*)
val status_and_time : proof_attempt -> proof_status * float * bool
(* returns status, time and the obsolete flag *)
val status_and_time :
proof_attempt -> proof_status * float * bool * string
(** returns (status, time, obsolete flag, edited file name) *)
val edited_as : proof_attempt -> string
......@@ -213,3 +214,9 @@ val add_file : string -> file
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/whyide.byte"
End:
*)
......@@ -1625,15 +1625,15 @@ let edit_selected_row p =
let ext = String.sub file i (String.length file - i) in
let i = ref 1 in
while Sys.file_exists
(name ^ "_" ^ (string_of_int !i) ^ ext) do
incr i
(name ^ "_" ^ (string_of_int !i) ^ ext) do
incr i
done;
let file = name ^ "_" ^ (string_of_int !i) ^ ext in
a.Model.edited_as <- file;
Db.set_edited_as a.Model.proof_db file;
file
| f -> f
in
| f -> f
in
let old_status = a.Model.status in
Helpers.set_proof_status ~obsolete:false a Scheduler.Running 0.0;
let callback () =
......
......@@ -18,11 +18,9 @@ theory TestInt
goal Test6: 2+3 = 5 and (forall x:int. x*x >= 0)
goal Test7: 0 = 2 /\ 2 = 3 /\ 4 = 5 /\ 6 = 7
goal Test7: 0 = 2 and 2 = 3 and 4 = 5 and 6 = 7
(*
goal Test8: 3+3=7
*)
goal Test8: 2+2=4 and 3+3=6
end
......@@ -53,7 +51,7 @@ theory TestList
(*
goal Test1:
match x with
| Nil -> 1 = 0 /\ 2 = 3
| Nil -> 1 = 0 and 2 = 3
| Cons _ Nil -> 4 = 5 and 6 = 7
| Cons _ _ -> 8 = 9 /\ 10 = 11
end
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment