Commit c81ddd02 authored by MARCHE Claude's avatar MARCHE Claude

why-ide commence a marcher

parent 1ffa7c32
......@@ -284,8 +284,8 @@ $(MNGCMO) $(MNGCMX) $(addsuffix .cmx, $(MNGMAINS)) $(addsuffix .cmo, $(MNGMAINS)
src/manager/gmanager.cmo src/manager/gmanager.cmx: INCLUDES += -I +lablgtk2
ifeq (@enable_rust_prover@,yes)
byte: bin/manager-test.byte bin/why-rustprover.byte
opt: bin/manager-test.opt bin/why-rustprover.opt
byte: bin/manager-test.byte bin/why-ide.byte
opt: bin/manager-test.opt bin/why-ide.opt
endif
bin/manager-test.opt bin/manager-test.byte: INCLUDES = -thread -I +sqlite3
......@@ -299,15 +299,15 @@ bin/manager-test.byte: src/why.cma $(MNGCMO) src/manager/test.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma sqlite3.cma $^
bin/why-rustprover.opt bin/why-rustprover.byte: INCLUDES = -thread -I +sqlite3 -I +lablgtk2
bin/why-ide.opt bin/why-ide.byte: INCLUDES = -thread -I +sqlite3 -I +lablgtk2
bin/why-rustprover.opt: src/why.cmxa $(MNGCMX) src/manager/gmanager.cmx
bin/why-ide.opt: src/why.cmxa $(PGMCMX) $(MNGCMX) src/manager/gmanager.cmx
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx sqlite3.cmxa $^
$(STRIP) $@
bin/why-rustprover.byte: src/why.cma $(MNGCMO) src/manager/gmanager.cmo
bin/why-ide.byte: src/why.cma $(PGMCMO) $(MNGCMO) src/manager/gmanager.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
lablgtk.cma lablgtksourceview2.cma gtkThread.cmo sqlite3.cma $^
......@@ -327,56 +327,6 @@ clean::
rm -f bin/manager.byte bin/manager.opt
rm -f .depend.manager
#####################
# graphical interface
#####################
IDE_FILES = ide_main
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
IDEML = $(addsuffix .ml, $(IDEMODULES))
IDEMLI = $(addsuffix .mli, $(IDEMODULES))
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))
$(IDECMO) $(IDECMX): INCLUDES = -I src/ide -I +lablgtk2 -I +threads
# build targets
ifeq (@enable_ide@,yes)
byte: bin/whyide.byte
opt: bin/whyide.opt
endif
bin/whyide.opt bin/whyide.byte: INCLUDES = -I +lablgtk2 -I +threads
bin/whyide.opt: src/why.cmxa $(IDECMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^
$(STRIP) $@
bin/whyide.byte: src/why.cma $(IDECMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
lablgtk.cma lablgtksourceview2.cma gtkThread.cmo $^
# depend and clean targets
include .depend.ide
.depend.ide:
$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
depend: .depend.ide
clean::
rm -f src/ide/*.cm[iox] src/ide/*.o
rm -f src/ide/*.annot src/ide/*~
rm -f bin/whyide.byte bin/whyide.opt
rm -f .depend.ide
##############
# Coq plugin
......
......@@ -17,8 +17,10 @@
(* *)
(**************************************************************************)
open Why
open Sqlite3
type transaction_mode = | Deferred | Immediate | Exclusive
type handle = {
......@@ -239,14 +241,14 @@ type goal_origin =
type transf_data =
{ transf_name : string;
transf_action : Why.Task.task Why.Trans.tlist
transf_action : Task.task Trans.tlist
}
type goal = {
mutable goal_id : db_ident;
mutable goal_origin : goal_origin;
mutable task : Why.Task.task;
mutable task : Task.task;
mutable task_checksum: string;
mutable proved : bool;
(** invariant: g.proved == true iff
......@@ -1097,7 +1099,8 @@ let root_goals () =
exception AlreadyAttempted
let try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver
let try_prover ~(async:(unit->unit)->unit)
~debug ~timelimit ~memlimit ~prover ~command ~driver
(g : goal) : unit -> proof_attempt_status =
let db = current () in
let attempt =
......@@ -1123,8 +1126,8 @@ 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 false && debug then Format.eprintf "Task : %a@." Why.Pretty.print_task g.task;
let callback =
if false && debug then Format.eprintf "Task : %a@." Pretty.print_task g.task;
let callback : unit -> Call_provers.prover_result =
try
if false && debug then
Format.eprintf "Task for prover: %a@."
......@@ -1136,9 +1139,9 @@ let try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver
Format.eprintf "Db.try_prover: prove_task reports %a@."
Why.Driver.report e;
fun () -> raise Exit
| Why.Driver.Error e ->
| Driver.Error e ->
Format.eprintf "Db.try_prover: prove_task reports %a@."
Why.Driver.report e;
Driver.report e;
fun () -> raise Exit
*)
| e ->
......@@ -1148,30 +1151,33 @@ let try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver
in
fun () ->
if debug then Format.printf "setting attempt status to Running@.";
External_proof.set_status db attempt Running;
async (fun () -> External_proof.set_status db attempt Running);
try
let r = callback () in
if debug then Format.eprintf "prover result: %a@." Why.Call_provers.print_prover_result r;
External_proof.set_result_time db attempt r.Why.Call_provers.pr_time;
match r.Why.Call_provers.pr_answer with
| Why.Call_provers.Valid ->
External_proof.set_status db attempt Success;
g.proved <- true;
Goal.set_proved db g true;
(* TODO: update "proved" status of goal parents if any *)
if debug then Format.eprintf "prover result: %a@." Call_provers.print_prover_result r;
async
(fun () ->
External_proof.set_result_time db attempt r.Call_provers.pr_time);
match r.Call_provers.pr_answer with
| Call_provers.Valid ->
async (fun () ->
External_proof.set_status db attempt Success;
g.proved <- true;
Goal.set_proved db g true;
(* TODO: update "proved" status of goal parents if any *));
Success
| Why.Call_provers.Timeout ->
External_proof.set_status db attempt Timeout;
| Call_provers.Timeout ->
async (fun () -> External_proof.set_status db attempt Timeout);
Timeout
| Why.Call_provers.Invalid | Why.Call_provers.Unknown _ ->
External_proof.set_status db attempt Unknown;
| Call_provers.Invalid | Call_provers.Unknown _ ->
async (fun () -> External_proof.set_status db attempt Unknown);
Unknown
| Why.Call_provers.Failure _ | Why.Call_provers.HighFailure ->
External_proof.set_status db attempt HighFailure;
| Call_provers.Failure _ | Call_provers.HighFailure ->
async (fun () -> External_proof.set_status db attempt HighFailure);
HighFailure
with Exit ->
if debug then Format.eprintf "prover callback aborted because of an exception raised during elaboration@.";
External_proof.set_status db attempt HighFailure;
async (fun () -> External_proof.set_status db attempt HighFailure);
HighFailure
......@@ -1180,7 +1186,7 @@ let try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver
let add_transformation (_g : goal) (_t : transf) : unit =
assert false (* TODO *)
let add_or_replace_task ~tname ~name (t : Why.Task.task) : goal =
let add_or_replace_task ~tname ~name (t : Task.task) : goal =
(* TODO: replace if already exists *)
let g = {
goal_id = 0L;
......
......@@ -147,6 +147,7 @@ val root_goals : unit -> goal list
exception AlreadyAttempted
val try_prover :
async:((unit->unit)->unit) ->
debug:bool -> timelimit:int -> memlimit:int -> prover:prover ->
command:string -> driver:Driver.driver -> goal ->
(unit -> proof_attempt_status)
......
......@@ -62,8 +62,10 @@ let set_file f = match !file with
| Some _ ->
raise (Arg.Bad "only one file")
| None ->
(*
if not (Filename.check_suffix f ".why") then
raise (Arg.Bad ("don't know what to do with " ^ f));
*)
if not (Sys.file_exists f) then begin
Format.eprintf "%s %s: no such file@." pname f;
exit 1
......@@ -172,16 +174,20 @@ let provers_data =
printf "@\n===============================@.";
l
let alt_ergo =
let find_prover s =
match
List.fold_left
(fun acc p ->
if Db.prover_name p.prover = "Alt-Ergo" then Some p else acc)
if Db.prover_name p.prover = s then Some p else acc)
None provers_data
with
| None -> assert false
| Some p -> p
let alt_ergo = find_prover "Alt-Ergo"
let z3 = find_prover "Z3"
let () =
printf "previously known goals:@\n";
......@@ -213,22 +219,35 @@ module Ide_goals = struct
let cols = new GTree.column_list
let name_column = cols#add Gobject.Data.string
let id_column = cols#add Gobject.Data.caml
let status_column = cols#add GtkStock.conv
let renderer = GTree.cell_renderer_text [`XALIGN 0.]
let vcolumn =
let icon_renderer = GTree.cell_renderer_pixbuf [ `STOCK_SIZE `BUTTON ]
let view_name_column =
GTree.view_column ~title:"Theories/Goals"
~renderer:(renderer, ["text", name_column]) ()
let () =
vcolumn#set_resizable true;
vcolumn#set_max_width 400
view_name_column#set_resizable true;
view_name_column#set_max_width 400
let view_status_column =
GTree.view_column ~title:"Status"
~renderer:(icon_renderer, ["stock_id", status_column]) ()
let () =
view_status_column#set_resizable false;
view_status_column#set_visible true
let create ~packing () =
let model = GTree.tree_store cols in
let view = GTree.view ~model ~packing () in
let _ = view#selection#set_mode `SINGLE in
let _ = view#set_rules_hint true in
ignore (view#append_column vcolumn);
ignore (view#append_column view_name_column);
ignore (view#append_column view_status_column);
model,view
let clear model = model#clear ()
......@@ -242,6 +261,7 @@ module Ide_goals = struct
let parent = model#append () in
model#set ~row:parent ~column:name_column tname;
model#set ~row:parent ~column:id_column th.Theory.th_name;
(* model#set ~row:parent ~column:status_column `REMOVE; *)
let tasks = Task.split_theory th None in
List.iter
(fun t->
......@@ -252,6 +272,7 @@ module Ide_goals = struct
Ident.Hid.add goal_table id (g,row);
model#set ~row ~column:name_column name;
model#set ~row ~column:id_column id;
model#set ~row ~column:status_column `REMOVE;
)
tasks
......@@ -290,20 +311,33 @@ let select_goals (goals_view:GTree.tree_store) (task_view:GSourceView2.source_vi
)
selected_rows
let stock_of_result = function
| Db.Scheduled -> `ADD
| Db.Running -> `EXECUTE
| Db.Success -> `YES
| Db.Timeout -> `CUT
| Db.Unknown -> `DIALOG_QUESTION
| Db.HighFailure -> `PREFERENCES
let count = ref 0
let alt_ergo_on_all_goals () =
let async f = GtkThread.async f ()
let prover_on_all_goals ~(model:GTree.tree_store) p () =
Ident.Hid.iter
(fun id (g,_row) ->
Format.eprintf "running Alt-Ergo on goal %s@." id.Ident.id_string;
(fun id (g,row) ->
Format.eprintf "running %s on goal %s@." (Db.prover_name p.prover)
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
Db.print_status result;
model#set ~row ~column:Ide_goals.status_column (stock_of_result result);
in
let p = alt_ergo in
Scheduler.schedule_proof_attempt
~async
~debug:true ~timelimit ~memlimit:0
~prover:p.prover ~command:p.command ~driver:p.driver
~callback
......@@ -332,10 +366,6 @@ let main () =
in
let tools_menu = factory#add_submenu "_Tools" in
let tools_factory = new GMenu.factory tools_menu ~accel_group in
let _ =
tools_factory#add_image_item ~label:"Alt-Ergo on all goals"
~callback:alt_ergo_on_all_goals ()
in
(* horizontal paned *)
let hp = GPack.paned `HORIZONTAL ~border_width:3 ~packing:vbox#add () in
......@@ -349,6 +379,18 @@ let main () =
let goals_model,goals_view = Ide_goals.create ~packing:scrollview#add () in
Theory.Mnm.iter (fun _ th -> Ide_goals.add_goals goals_model th) theories;
let _ =
tools_factory#add_image_item ~key:GdkKeysyms._A
~label:"Alt-Ergo on all goals"
~callback:(fun () ->
prover_on_all_goals ~model:goals_model alt_ergo ()(*;
prover_on_all_goals ~model:goals_model z3 ()*)) ()
in
let _ =
tools_factory#add_image_item ~key:GdkKeysyms._E
~label:"Expand all" ~callback:(fun () -> goals_view#expand_all ()) ()
in
(* horizontal paned *)
let vp = GPack.paned `VERTICAL ~border_width:3 ~packing:hp#add () in
......@@ -408,6 +450,6 @@ let () =
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why-rustprover.byte"
compile-command: "unset LANG; make -C ../.. bin/why-ide.byte"
End:
*)
......@@ -9,12 +9,12 @@ let attempts = Queue.create ()
let running_proofs = ref 0
let maximum_running_proofs = ref 2
let schedule_proof_attempt ~debug ~timelimit ~memlimit ~prover
let schedule_proof_attempt ~async ~debug ~timelimit ~memlimit ~prover
~command ~driver ~callback
goal =
let prepare_goal =
try
Db.try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver goal;
Db.try_prover ~async ~debug ~timelimit ~memlimit ~prover ~command ~driver goal;
with Db.AlreadyAttempted ->
raise Exit
in
......
......@@ -21,6 +21,7 @@
open Why
val schedule_proof_attempt :
async:((unit->unit)->unit) ->
debug:bool -> timelimit:int -> memlimit:int -> prover:Db.prover ->
command:string -> driver:Driver.driver ->
callback:(Db.proof_attempt_status -> unit) -> Db.goal -> unit
......
[main]
library = "theories"
timelimit = 2
timelimit = 10
[prover alt-ergo]
name = "Alt-Ergo"
......
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