Skip to content

why3
why3
Commit 9f6d882f authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

ca commence a marchouiller avec Coq

parent 790abd8b
Hide whitespace changes
Inline Side-by-side
Showing with 309 additions and 174 deletions
drivers/coq.drv
View file @ 9f6d882f
......@@ -6,7 +6,8 @@ valid 0
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
prelude "(* generated by Why3's Coq driver *)"
prelude "(* This file is generated by Why3's Coq driver *)"
prelude "(* Beware! Only edit allowed sections below *)"
theory BuiltIn
......
prover-detection-data.conf
View file @ 9f6d882f
[ATP alt-ergo]
name = "Alt-Ergo"
command = "ergo"
command = "alt-ergo"
exec = "alt-ergo"
exec = "ergo"
version_switch = "-version"
version_regexp = ".*Ergo \\([^ ]*\\)"
version_ok = "0.92"
version_old = "0.8"
version_old = "0.9"
command = "why3-cpulimit %t %m %e %f"
driver = "drivers/alt_ergo.drv"
[ATP cvc3]
name = "CVC3"
command = "cvc3"
exec = "cvc3"
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ ]+\\)"
version_ok = "2.2"
version_old = "2.1"
command = "why3-cpulimit 0 %m %e -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3.drv"
[ATP eprover]
name = "Eprover"
exec = "eprover"
command = "why3-cpulimit 0 %m %e -s --print-statistics -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
driver = "drivers/tptp.drv"
[ATP gappa]
name = "Gappa"
command = "gappa"
exec = "gappa"
version_switch = "--version"
version_regexp = "Gappa \\([^ ]*\\)"
version_ok = "0.13.0"
......@@ -27,31 +37,45 @@ version_old = "0.12.0"
version_old = "0.12.1"
version_old = "0.12.2"
version_old = "0.12.3"
command = "why3-cpulimit %t %m %e %f 2>&1"
driver = "drivers/gappa.drv"
[ATP simplify]
name = "Simplify"
command = "Simplify"
command = "simplify"
command = "Simplify-1.5.4"
command = "Simplify-1.5.5"
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
version_switch = "-version"
version_regexp = "Simplify version \\([^ ,]+\\)"
version_ok = "1.5.4"
version_ok = "1.5.5"
command = "why3-cpulimit %t %m %e %f 2>&1"
driver = "drivers/simplify.drv"
[ATP spass]
name = "Spass"
exec = "SPASS"
version_switch = "-version (TODO)"
version_regexp = "SPASS version \\([^ ,]+\\) (TODO)"
command = "why3-cpulimit 0 %m %e -TPTP -PGiven=0 -PProblem=0 -DocProof -TimeLimit=%t %f 2>&1"
driver = "drivers/tptp.drv"
[ATP z3]
name = "Z3"
command = "z3"
command = "z3-2.2"
exec = "z3"
exec = "z3-2.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \r]+\\)"
version_ok = "2.2"
version_old = "2.1"
version_old = "1.3"
command = "why3-cpulimit %t %m %e -smt %f 2>&1"
driver = "drivers/z3.drv"
[ITP coq]
name = "Coq"
command = "coqc"
exec = "coqc"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ ]+\\)"
version_ok = "8.0"
......@@ -59,6 +83,8 @@ version_ok = "8.1"
version_ok = "8.2"
version_ok = "8.2pl1"
version_old = "7.4"
command = "%e %f"
driver = "drivers/coq.drv"
src/ide/gconfig.ml
View file @ 9f6d882f
......@@ -7,7 +7,8 @@ type prover_data =
prover_name : string;
prover_version : string;
command : string;
driver : Why.Driver.driver;
driver_name : string;
driver : Driver.driver;
}
type t =
......@@ -32,12 +33,14 @@ let default =
provers = [];
}
let conf_file = Filename.concat (Rc.get_home_dir ()) ".whyide.conf"
let conf_file = Filename.concat (Rc.get_home_dir ()) ".why.conf"
let save_prover fmt p =
fprintf fmt "[prover]@\n";
fprintf fmt "id = \"%s\"@\n" p.prover_id;
fprintf fmt "[prover %s]@\n" p.prover_id;
fprintf fmt "name = \"%s\"@\n" p.prover_name;
fprintf fmt "version = \"%s\"@\n" p.prover_version;
fprintf fmt "command = \"%s\"@\n" p.command;
fprintf fmt "driver = \"%s\"@\n" p.driver_name;
fprintf fmt "@."
let save_config config =
......@@ -69,42 +72,52 @@ let load_main c (key, value) =
let get_prover_data env config id ver =
let pi = Util.Mstr.find id config.Whyconf.provers in
let d = Why.Driver.load_driver env pi.Whyconf.driver in
{ prover_id = id ;
prover_name = pi.Whyconf.name;
prover_version = ver;
command = pi.Whyconf.command;
driver = d;
}
let get_prover_data env id name ver c d =
try
let dr = Driver.load_driver env d in
{ prover_id = id ;
prover_name = name;
prover_version = ver;
command = c;
driver_name = d;
driver = dr;
}
with _e ->
eprintf "Failed to load driver %s for prover %s. prover disabled@."
d name;
raise Not_found
let load_prover env whyconfig l =
let id = ref "?" in
let load_prover env id l =
let name = ref "?" in
let v = ref "?" in
let c = ref "?" in
let d = ref "?" in
List.iter
(fun (key, value) ->
match key with
| "id" -> id := Rc.string value
| "name" -> name := Rc.string value
| "version" -> v := Rc.string value
| "command" -> c := Rc.string value
| "driver" -> d := Rc.string value
| s ->
eprintf "Warning: ignore unknown key [%s] in prover data of whyide config file@." s)
l;
get_prover_data env whyconfig !id !v
get_prover_data env id !name !v !c !d
let load env whyconfig c (key, al) =
let load env c (key, al) =
match key with
| "main" :: _ -> List.iter (load_main c) al
| "prover" :: _ -> c.provers <- load_prover env whyconfig al :: c.provers
| "prover" :: id :: _ ->
c.provers <- load_prover env id al :: c.provers
| s :: _ ->
eprintf "Warning: ignored unknown section [%s] in whyide config file@." s
| [] -> assert false
let read_config env whyconfig =
let read_config env =
try
let rc = Rc.from_file conf_file in
let c = default in
List.iter (load env whyconfig c) rc;
List.iter (load env c) rc;
c
with
| Failure "lexing" ->
......@@ -300,32 +313,38 @@ type prover_autodetection_data =
{ kind : prover_kind;
prover_id : string;
mutable prover_name : string;
mutable commands : string list;
mutable execs : string list;
mutable version_switch : string;
mutable version_regexp : string;
mutable versions_ok : string list;
mutable versions_old : string list;
mutable command : string;
mutable driver : string;
}
let default k id =
{ kind = k;
prover_id = id;
prover_name = "";
commands = [];
execs = [];
version_switch = "";
version_regexp = "";
versions_ok = [];
versions_old = [];
command = "";
driver ="";
}
let load_prover d (key, value) =
match key with
| "name" -> d.prover_name <- Rc.string value
| "command" -> d.commands <- Rc.string value :: d.commands
| "exec" -> d.execs <- Rc.string value :: d.execs
| "version_switch" -> d.version_switch <- Rc.string value
| "version_regexp" -> d.version_regexp <- Rc.string value
| "version_ok" -> d.versions_ok <- Rc.string value :: d.versions_ok
| "version_old" -> d.versions_old <- Rc.string value :: d.versions_old
| "command" -> d.command <- Rc.string value
| "driver" -> d.driver <- Rc.string value
| s ->
eprintf "unknown key [%s] in autodetection data@." s;
exit 1
......@@ -363,7 +382,15 @@ let provers_found = ref 0
let prover_tips_info = ref false
let detect_prover env whyconfig acc data =
let make_command exec com =
let cmd_regexp = Str.regexp "%\\(.\\)" in
let replace s = match Str.matched_group 1 s with
| "e" -> exec
| c -> "%"^c
in
Str.global_substitute cmd_regexp replace com
let detect_prover env acc data =
List.fold_left
(fun acc com ->
let out = Filename.temp_file "out" "" in
......@@ -401,25 +428,24 @@ let detect_prover env whyconfig acc data =
eprintf "Warning: prover %s version %s is not known to be supported, use it at your own risk!@." nam ver
end;
incr provers_found;
get_prover_data env whyconfig data.prover_id ver :: acc
let c = make_command com data.command in
get_prover_data env data.prover_id data.prover_name ver
c data.driver :: acc
else
begin
prover_tips_info := true;
eprintf "Warning: found prover %s but name/version not recognized by regexp `%s'@." data.prover_name data.version_regexp;
eprintf "Answer was `%s'@." s;
(*
p.command <- cmd;
p.version <- "?";
*)
acc
end)
acc
data.commands
data.execs
let run_auto_detection env whyconfig gconfig =
let run_auto_detection env gconfig =
let l = read_auto_detection_data () in
let detect = List.fold_left (detect_prover env whyconfig) [] l in
let detect = List.fold_left (detect_prover env) [] l in
eprintf "%d provers detected.@." (List.length detect);
gconfig.provers <- detect
......
src/ide/gconfig.mli
View file @ 9f6d882f
......@@ -6,6 +6,7 @@ type prover_data =
prover_name : string;
prover_version : string;
command : string;
driver_name : string;
driver : Driver.driver;
}
......@@ -20,7 +21,7 @@ type t =
mutable provers : prover_data list;
}
val read_config : Env.env -> Whyconf.config -> t
val read_config : Env.env -> t
val save_config : t -> unit
......@@ -52,7 +53,7 @@ val show_legend_window : unit -> unit
val show_about_window : unit -> unit
val preferences : t -> unit
val run_auto_detection : Env.env -> Whyconf.config -> t -> unit
val run_auto_detection : Env.env -> t -> unit
(*
Local Variables:
......
src/ide/gmain.ml
View file @ 9f6d882f
......@@ -28,6 +28,7 @@ open Gconfig
(* loading Why configuration *)
(*****************************)
(*
let config =
try
Whyconf.read_config None
......@@ -41,15 +42,8 @@ let config =
let () = eprintf "Load path is: %a@."
(Pp.print_list Pp.comma Pp.string) config.loadpath
(*
let timelimit =
match config.timelimit with
| None -> 2
| Some n -> n
*)
(***************************)
(* parsing comand_line *)
(***************************)
......@@ -100,7 +94,7 @@ let source_text =
close_in ic;
buf
let env = Why.Env.create_env (Why.Lexer.retrieve config.loadpath)
let env = Why.Env.create_env (Why.Lexer.retrieve ["theories"])
(********************************)
(* loading WhyIDE configuration *)
......@@ -108,7 +102,7 @@ let env = Why.Env.create_env (Why.Lexer.retrieve config.loadpath)
let gconfig =
eprintf "reading IDE config file@.";
read_config env config
read_config env
......@@ -175,12 +169,16 @@ module Model = struct
type proof_attempt =
{ prover : prover_data;
proof_goal : goal;
proof_row : Gtk.tree_iter;
mutable status : Scheduler.proof_attempt_status;
mutable proof_obsolete : bool;
mutable time : float;
mutable output : string;
mutable edited_as : string;
}
type goal_parent =
and goal_parent =
| Theory of theory
| Transf of transf
......@@ -189,7 +187,7 @@ module Model = struct
task: Task.task;
goal_row : Gtk.tree_iter;
mutable proved : bool;
mutable external_proofs: proof_attempt list;
external_proofs: (string, proof_attempt) Hashtbl.t;
mutable transformations : transf list;
}
......@@ -337,6 +335,14 @@ let goals_model,filter_model,goals_view = Model.create ~packing:scrollview#add (
module Helpers = struct
let image_of_result = function
| Scheduler.Scheduled -> !image_scheduled
| Scheduler.Running -> !image_running
| Scheduler.Success -> !image_valid
| Scheduler.Timeout -> !image_timeout
| Scheduler.Unknown -> !image_unknown
| Scheduler.HighFailure -> !image_failure
open Model
let set_theory_proved t =
......@@ -346,8 +352,7 @@ module Helpers = struct
goals_model#set ~row ~column:Model.status_column !image_yes;
if !Model.toggle_hide_proved_goals then
goals_model#set ~row ~column:Model.visible_column false
let rec set_proved g =
let row = g.goal_row in
g.proved <- true;
......@@ -364,7 +369,13 @@ module Helpers = struct
begin
set_proved t.parent_goal;
end
let set_proof_status a s =
a.status <- s;
let row = a.proof_row in
goals_model#set ~row ~column:Model.status_column
(image_of_result s);
if s = Scheduler.Success then set_proved a.proof_goal
let add_theory th =
let tname = th.Theory.th_name.Ident.id_string in
......@@ -389,7 +400,7 @@ module Helpers = struct
let goal = { parent = Theory mth;
task = t ;
goal_row = row;
external_proofs = [];
external_proofs = Hashtbl.create 7;
transformations = [];
proved = false;
}
......@@ -414,14 +425,6 @@ let () =
let image_of_result = function
| Scheduler.Scheduled -> !image_scheduled
| Scheduler.Running -> !image_running
| Scheduler.Success -> !image_valid
| Scheduler.Timeout -> !image_timeout
| Scheduler.Unknown -> !image_unknown
| Scheduler.HighFailure -> !image_failure
let () =
begin
Scheduler.async := GtkThread.async;
......@@ -440,25 +443,35 @@ let () =
let rec prover_on_goal p g =
let row = g.Model.goal_row in
let name = p.prover_name in
let prover_row = goals_model#append ~parent:row () in
goals_model#set ~row:prover_row ~column:Model.icon_column !image_prover;
goals_model#set ~row:prover_row ~column:Model.name_column (name ^ " " ^ p.prover_version);
goals_model#set ~row:prover_row ~column:Model.visible_column true;
goals_view#expand_row (goals_model#get_path row);
let a = { Model.prover = p;
Model.status = Scheduler.Scheduled;
Model.time = 0.0;
Model.output = "" }
let id = p.prover_id in
let a =
try Hashtbl.find g.Model.external_proofs id
with Not_found ->
(* creating a new row *)
let name = p.prover_name in
let prover_row = goals_model#append ~parent:row () in
goals_model#set ~row:prover_row ~column:Model.icon_column !image_prover;
goals_model#set ~row:prover_row ~column:Model.name_column (name ^ " " ^ p.prover_version);
goals_model#set ~row:prover_row ~column:Model.visible_column true;
goals_view#expand_row (goals_model#get_path row);
let a = { Model.prover = p;
Model.proof_goal = g;
Model.proof_row = prover_row;
Model.status = Scheduler.Scheduled;
Model.proof_obsolete = false;
Model.time = 0.0;
Model.output = "";
Model.edited_as = "";
}
in
goals_model#set ~row:prover_row ~column:Model.index_column
(Model.Row_proof_attempt a);
Hashtbl.add g.Model.external_proofs id a;
a
in
goals_model#set ~row:prover_row ~column:Model.index_column
(Model.Row_proof_attempt a);
g.Model.external_proofs <- a :: g.Model.external_proofs;
let callback result time output =
a.Model.status <- result;
a.Model.output <- output;
goals_model#set ~row:prover_row ~column:Model.status_column
(image_of_result result);
Helpers.set_proof_status a result;
let t = if time > 0.0 then
begin
a.Model.time <- time;
......@@ -466,14 +479,15 @@ let rec prover_on_goal p g =
end
else ""
in
goals_model#set ~row:prover_row ~column:Model.time_column t;
if result = Scheduler.Success then
Helpers.set_proved g
goals_model#set ~row:a.Model.proof_row ~column:Model.time_column t
in
callback Scheduler.Scheduled 0.0 "";
let old = if a.Model.edited_as = "" then None else
(Some (open_in a.Model.edited_as))
in
Scheduler.schedule_proof_attempt
~debug:(gconfig.verbose > 0) ~timelimit:gconfig.time_limit ~memlimit:0
~prover:p.prover_id ~command:p.command ~driver:p.driver
?old ~command:p.command ~driver:p.driver
~callback
g.Model.task;
List.iter
......@@ -530,7 +544,7 @@ let split_unproved_goals () =
let goal = { Model.parent = Model.Transf tr;
Model.task = subtask ;
Model.goal_row = subtask_row;
Model.external_proofs = [];
Model.external_proofs = Hashtbl.create 7;
Model.transformations = [];
Model.proved = false;
}
......@@ -574,7 +588,7 @@ let (_ : GMenu.image_menu_item) =
let (_ : GMenu.image_menu_item) =
file_factory#add_image_item ~label:"_Detect provers" ~callback:
(fun () -> Gconfig.run_auto_detection env config gconfig)
(fun () -> Gconfig.run_auto_detection env gconfig)
()
let (_ : GMenu.image_menu_item) =
......@@ -695,20 +709,6 @@ let () =
()
in ()) gconfig.provers
(*
let (_ : GMenu.image_menu_item) =
tools_factory#add_image_item ~key:GdkKeysyms._A
~label:"Alt-Ergo on unproved goals"
~callback:(fun () -> prover_on_unproved_goals alt_ergo ())
()
let (_ : GMenu.image_menu_item) =
tools_factory#add_image_item ~key:GdkKeysyms._Z
~label:"Z3 on unproved goals"
~callback:(fun () -> prover_on_unproved_goals z3 ())
()
*)
let (_ : GMenu.image_menu_item) =
tools_factory#add_image_item
~label:"Split unproved goals"
......@@ -811,6 +811,51 @@ let select_row p =
| _ -> ()
*)
(*****************************)
(* method: edit current goal *)
(*****************************)
let edit_selected_row p =
let row = filter_model#get_iter p in
match filter_model#get ~row ~column:Model.index_column with
| Model.Row_goal _g ->
()
| Model.Row_theory _th ->
()
| Model.Row_proof_attempt a ->
eprintf "schudeling editing@.";
let file = "goal.v" in
a.Model.edited_as <- file;
let g = a.Model.proof_goal in
let t = g.Model.task in
let old_status = a.Model.status in
Helpers.set_proof_status a Scheduler.Running;
let callback () =
Helpers.set_proof_status a old_status;
in
Scheduler.edit_proof ~debug:false ~editor:"coqide"
~file
~driver:a.Model.prover.driver
~callback
t
| Model.Row_transformation _tr ->
()
let edit_current_proof () =
match goals_view#selection#get_selected_rows with
| [] -> ()
| [p] -> edit_selected_row p
| _ -> assert false (* multi-selection is disabled *)
let (_ : GMenu.image_menu_item) =
tools_factory#add_image_item
~label:"Edit current proof"
~callback:edit_current_proof
()
(***************)
(* source view *)
......@@ -848,6 +893,7 @@ let (_ : GtkSignal.id) =
begin fun () ->
match goals_view#selection#get_selected_rows with
| [p] -> select_row p
| [] -> ()
| _ -> assert false (* multi-selection is disabled *)
end
......
src/ide/scheduler.ml
View file @ 9f6d882f
......@@ -18,19 +18,24 @@ type proof_attempt_status =
(**** queues of events to process ****)
type attempt = bool * int * int * string * string * Driver.driver *
(proof_attempt_status -> float -> string -> unit) * Task.task
type callback = proof_attempt_status -> float -> string -> unit
type attempt = bool * int * int * in_channel option * string * Driver.driver *
callback * Task.task
(* queue of external proof attempts *)
let prover_attempts_queue : attempt Queue.t = Queue.create ()
(* queue of proof editing tasks *)
let proof_edition_queue : (bool * string * string * Driver.driver *
(unit -> unit) * Task.task) Queue.t = Queue.create ()
(* queue of transformations *)
let transf_queue :
((Task.task list -> unit) * 'a Trans.trans * Task.task) Queue.t
= Queue.create ()
(* queue of prover answers *)
let answers_queue : (attempt * proof_attempt_status * float * string) Queue.t
let answers_queue : (callback * proof_attempt_status * float * string) Queue.t
= Queue.create ()
(* number of running external proofs *)
......@@ -51,13 +56,15 @@ let event_handler () =
while
Queue.is_empty transf_queue &&
Queue.is_empty answers_queue &&
Queue.is_empty proof_edition_queue &&
(Queue.is_empty prover_attempts_queue ||
!running_proofs >= !maximum_running_proofs)
do
Condition.wait queue_condition queue_lock
done;
try
let (a,res,time,output) = Queue.pop answers_queue in
(* priority 1: collect answers from provers *)
let (callback,res,time,output) = Queue.pop answers_queue in
decr running_proofs;
Mutex.unlock queue_lock;
(*
......@@ -65,10 +72,10 @@ let event_handler () =
*)
(* TODO: update database *)
(* call GUI callback with argument [res] *)
let (_,_,_,_,_,_,callback,_) = a in
!async (fun () -> callback res time output) ()
with Queue.Empty ->
try
(* priority 2: apply transformations *)
let (callback,transf,task) = Queue.pop transf_queue in
Mutex.unlock queue_lock;
let subtasks : Task.task list = Trans.apply transf task in
......@@ -76,25 +83,52 @@ let event_handler () =
(* call GUI back given new subgoals *)
!async (fun () -> callback subtasks) ()
with Queue.Empty ->
try
(* priority 3: edit proofs *)
let (_debug,editor,file,driver,callback,goal) = Queue.pop proof_edition_queue in
Mutex.unlock queue_lock;
let backup = file ^ ".bak" in
let old =
if Sys.file_exists file
then
begin
Sys.rename file backup;
Some(open_in backup)
end
else None
in
let ch = open_out file in
let fmt = formatter_of_out_channel ch in
Driver.print_task ?old driver fmt goal;
Util.option_iter close_in old;
close_out ch;
let _ = Sys.command(editor ^ " " ^ file) in
(* when done, call GUI back *)
!async (fun () -> callback ()) ()
with Queue.Empty ->
(* priority low: start new external proof attempt *)
(* since answers_queue and transf_queue are empty,
we are sure that both
prover_attempts_queue is non empty and
running_proofs < maximum_running_proofs
*)
try
let a = Queue.pop prover_attempts_queue in
let (_debug,timelimit,memlimit,old,command,driver,callback,goal) =
Queue.pop prover_attempts_queue
in
incr running_proofs;
Mutex.unlock queue_lock;
(* build the prover task from goal in [a] *)
let (debug,timelimit,memlimit,_prover,command,driver,callback,goal) = a
in
!async (fun () -> callback Running 0.0 "") ();
try
let call_prover : unit -> Call_provers.prover_result =
(*
if debug then
Format.eprintf "Task for prover: %a@."
(Driver.print_task driver) goal;
Driver.prove_task ~command ~timelimit ~memlimit driver goal
*)