From 48dce31121a16460bc851a45cc3595600ded1bd2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois@bobot.eu> Date: Wed, 8 Dec 2010 21:26:19 +0100 Subject: [PATCH] rc file working add timelimit --- Makefile.in | 2 +- examples/programs/prgbench.rc | 15 ++++ src/bench/bench.ml | 120 +++++++++++++++++++++++++++++++- src/bench/bench.mli | 53 ++++++++++++++ src/bench/benchrc.ml | 79 ++++++++++----------- src/bench/benchrc.mli | 30 +++----- src/bench/whybench.ml | 126 +++++++++++++++------------------- src/ide/gmain.ml | 1 - src/ide/scheduler.ml | 4 +- src/ide/scheduler.mli | 4 +- src/util/rc.mll | 2 +- src/util/util.ml | 5 ++ src/util/util.mli | 4 ++ 13 files changed, 306 insertions(+), 139 deletions(-) create mode 100644 examples/programs/prgbench.rc diff --git a/Makefile.in b/Makefile.in index 81e68af3b4..df1c36a868 100644 --- a/Makefile.in +++ b/Makefile.in @@ -455,7 +455,7 @@ endif # BENCH ############### -BENCH_FILES = bench whybench benchrc +BENCH_FILES = bench benchrc whybench BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES)) diff --git a/examples/programs/prgbench.rc b/examples/programs/prgbench.rc new file mode 100644 index 0000000000..6d6e8e3a37 --- /dev/null +++ b/examples/programs/prgbench.rc @@ -0,0 +1,15 @@ +[tools fast] +prover = "alt-ergo" +prover = "cvc3" +timelimit = 5 + +[tools tptp] +prover = "spass" + +[probs funny] +file = "talk290.mlw" +transform = "split_goal" + +[bench fast_and_funny] +tools = fast +probs = funny \ No newline at end of file diff --git a/src/bench/bench.ml b/src/bench/bench.ml index 1e47fb5a6e..269f3232ce 100644 --- a/src/bench/bench.ml +++ b/src/bench/bench.ml @@ -75,10 +75,12 @@ struct c = Condition.create (); nb_task = 0} + let test s = s.nb_task = 0 let start s = Mutex.lock s.m; s.nb_task <- s.nb_task + 1; Mutex.unlock s.m let stop s = Mutex.lock s.m; s.nb_task <- s.nb_task - 1; - if s.nb_task = 0 then Condition.signal s.c; Mutex.unlock s.m - let wait s = Mutex.lock s.m; Condition.wait s.c s.m + if test s then Condition.signal s.c; Mutex.unlock s.m + let wait s = Mutex.lock s.m; + if not (test s) then Condition.wait s.c s.m let lock s = Mutex.lock s.m let unlock s = Mutex.unlock s.m end @@ -124,7 +126,8 @@ let general ?(callback=fun _ _ _ _ _ -> ()) iter add = MTask.unlock s | _ -> () in call s cb tool prob); - MTask.wait s + MTask.wait s; + MTask.unlock s let any ?callback toolprob = let l = ref [] in @@ -147,3 +150,114 @@ let all_array ?callback tools probs = Array.iteri (fun i t -> Array.iteri (fun j p -> f (i,j) t p) probs) tools) (fun (i,j) r -> m.(i).(j) <- r::m.(i).(j)); m + + +let all_list_tools ?callback tools probs = + let tools = List.map (fun t -> (t, ref [])) tools in + general ?callback (fun f -> + List.iter (fun (t,l) -> List.iter (fun p -> f l t p) probs) tools) + (fun l r -> l:=r::!l); + List.map (fun (t,l) -> (t.tval,!l)) tools + +type output = + (** on stdout *) + |Average + |Timeline + (** In a file *) + |Csv + +type ('a,'b) bench = + { + btools : 'a tool list; + bprobs : 'b prob list; + boutputs : output list; + } + +let run_bench ?callback bench = + all_list ?callback bench.btools bench.bprobs + +let run_benchs ?callback benchs = + let benchs = List.map (fun b -> (b,ref [])) benchs in + general ?callback (fun f -> + List.iter (fun (b,l) -> + List.iter (fun t -> List.iter (fun p -> f l t p) b.bprobs) + b.btools) benchs) + (fun l r -> l:=r::!l); + List.map (fun (b,l) -> (b,!l)) benchs + +let run_benchs_tools ?callback benchs = + let benchs = List.map (fun b -> + b, List.map (fun t -> t,ref []) b.btools) benchs in + general ?callback (fun f -> + List.iter (fun (b,l) -> + List.iter (fun (t,l) -> List.iter (fun p -> f l t p) b.bprobs) + l) benchs) + (fun l r -> l:=r::!l); + List.map (fun (b,l) -> b,List.map (fun (t,l) -> t.tval,!l) l) benchs + + +(** average *) + +(** valid * timeout * unknown * invalid *) +type nb_avg = int * float + +let add_nb_avg (nb,avg) time = + (succ nb, ((float nb) *. avg +. time) /. (float (succ nb))) +let empty_nb_avg = (0,0.) + +let print_nb_avg fmt (nb,avg) = Format.fprintf fmt "%i : %.2f" nb avg + +type tool_res = + { valid : nb_avg; + timeout : nb_avg; + unknown : nb_avg; + invalid : nb_avg; + failure : nb_avg} + +let empty_tool_res = + { valid = empty_nb_avg; + timeout = empty_nb_avg; + unknown = empty_nb_avg; + invalid = empty_nb_avg; + failure = empty_nb_avg; + } + + let print_tool_res fmt tool_res = + Format.fprintf fmt "(%a, %a, %a, %a, %a)" + print_nb_avg tool_res.valid + print_nb_avg tool_res.unknown + print_nb_avg tool_res.timeout + print_nb_avg tool_res.invalid + print_nb_avg tool_res.failure + + let compute_average l = + let fold tr res = + let r = res.result in + match r.pr_answer with + | Valid -> {tr with valid = add_nb_avg tr.valid r.pr_time} + | Timeout -> {tr with timeout = add_nb_avg tr.timeout r.pr_time} + | Invalid -> {tr with invalid = add_nb_avg tr.invalid r.pr_time} + | Unknown _ -> {tr with unknown = add_nb_avg tr.unknown r.pr_time} + | Failure _ | HighFailure -> + {tr with failure = add_nb_avg tr.failure r.pr_time} in + List.fold_left fold empty_tool_res l + + let filter_timeline l = + let l = List.filter (fun r -> r.result.pr_answer = Valid) l in + let compare_valid x y = + let c = compare x.result.pr_time y.result.pr_time in + if c <> 0 then c else compare x y in + let l = List.fast_sort compare_valid l in + l + + let compute_timeline min max step = + let rec aux acc cur next = function + | _ when next > max -> List.rev acc + | [] -> aux (cur::acc) cur (next+.step) [] + | {result={pr_time = t}}::_ as l when t >= next -> + aux (cur::acc) cur (next+.step) l + | _::l -> aux acc (cur+1) next l in + aux [] 0 min + + let max_time l = + List.fold_left (fun acc {result={pr_time = t}} -> max acc t) 0. l diff --git a/src/bench/bench.mli b/src/bench/bench.mli index e122931cf3..a9e085407f 100644 --- a/src/bench/bench.mli +++ b/src/bench/bench.mli @@ -64,3 +64,56 @@ val all_array : val any : ?callback:('a,'b) callback -> ('a tool * 'b prob) list -> ('a,'b) result list + + +val all_list_tools : + ?callback:('a,'b) callback -> + 'a tool list -> 'b prob list -> ('a * ('a,'b) result list) list + +type output = + (** on stdout *) + |Average + |Timeline + (** In a file *) + |Csv + +type ('a,'b) bench = + { + btools : 'a tool list; + bprobs : 'b prob list; + boutputs : output list; + } + +val run_bench : + ?callback:('a,'b) callback -> ('a,'b) bench -> ('a,'b) result list + + +val run_benchs : + ?callback:('a,'b) callback -> ('a,'b) bench list -> + (('a,'b) bench * ('a,'b) result list) list + +val run_benchs_tools : + ?callback:('a,'b) callback -> ('a,'b) bench list -> + (('a,'b) bench * ('a * ('a,'b) result list) list) list + + +type nb_avg = int * float + +val print_nb_avg : Format.formatter -> nb_avg -> unit + +type tool_res = + { valid : nb_avg; + timeout : nb_avg; + unknown : nb_avg; + invalid : nb_avg; + failure : nb_avg} + +val print_tool_res : Format.formatter -> tool_res -> unit + +val compute_average : ('a,'b) result list -> tool_res +val compute_timeline : + float -> float -> float -> ('a,'b) result list -> int list + +val filter_timeline : ('a,'b) result list -> ('a,'b) result list + +val max_time : ('a,'b) result list -> float diff --git a/src/bench/benchrc.ml b/src/bench/benchrc.ml index cac538e69b..50e5e2aa70 100644 --- a/src/bench/benchrc.ml +++ b/src/bench/benchrc.ml @@ -23,31 +23,25 @@ open Why open Util open Theory -type output = - (** on stdout *) - |Average - |Timeline - (** In a file *) - |Csv -type bench = - { - (* tool_name, prover_name *) - btools : (string * string) tool list; - (* prob_name, file_name, theory name *) - bprobs : (string * string * string) prob list; - boutputs : output list; - } +type id_tool = (string * string) +type id_prob = (string * string * string) -type benchrc = { tools : (string * string) tool list Mstr.t; - probs : (string * string * string) prob Mstr.t; - benchs : bench Mstr.t; +type benchrc = { tools : id_tool tool list Mstr.t; + probs : id_prob prob Mstr.t; + benchs : (id_tool,id_prob) bench Mstr.t } open Whyconf open Rc -let read_tools wc map (name,section) = +let absolute_filename dirname f = + if Filename.is_relative f then + Filename.concat dirname f + else + f + +let read_tools absf wc map (name,section) = (* loadpath *) let wc_main = get_main wc in let loadpath = get_stringl ~default:[] section "loadpath" in @@ -84,7 +78,7 @@ let read_tools wc map (name,section) = try let driver = get_string section "driver" in let command = get_string section "command" in - ("driver",driver,command) :: provers + ("driver",absf driver,command) :: provers with MissingField _ -> provers in let load_driver (n,d,c) = n,Driver.load_driver env d,c in let provers = List.map load_driver provers in @@ -100,7 +94,7 @@ let read_tools wc map (name,section) = } in Mstr.add name (List.map create_tool provers) map -let read_probs map (name,section) = +let read_probs absf map (name,section) = (* transformations *) let transforms = get_stringl ~default:[] section "transform" in let gen_trans env = @@ -117,50 +111,57 @@ let read_probs map (name,section) = let files = get_stringl ~default:[] section "file" in let gen env task = let fwhy () = - let read_one fname = - let cin = open_in fname in - let m = Env.read_channel ?format:format env fname cin in - close_in cin; - let ths = Mnm.bindings m in - List.rev_map (fun (n,th) -> ((name,fname,n),th)) ths - in - let map (name,th) = name,Task.split_theory th None task in - let fold acc (n,l) = - List.rev_append (List.rev_map (fun v -> (n,v)) l) acc in - files |> List.map read_one |> list_flatten_rev - |> List.rev_map map |> List.fold_left fold [] in + try + let read_one fname = + let cin = open_in (absf fname) in + let m = Env.read_channel ?format:format env fname cin in + close_in cin; + let ths = Mnm.bindings m in + List.rev_map (fun (n,th) -> ((name,fname,n),th)) ths + in + let map (name,th) = name,Task.split_theory th None task in + let fold acc (n,l) = + List.rev_append (List.rev_map (fun v -> (n,v)) l) acc in + files |> List.map read_one |> list_flatten_rev + |> List.rev_map map |> List.fold_left fold [] + with exn -> eprintf "%a@." Exn_printer.exn_printer exn; exit 1 + in Scheduler.do_why_sync fwhy () in Mstr.add name { ptask = gen; ptrans = gen_trans} map let read_bench mtools mprobs map (name,section) = let tools = get_stringl section "tools" in let lookup s = - try Mstr.find s mtools with Not_found -> eprintf "Undefined tools %s@." s; + try Mstr.find s mtools + with Not_found -> eprintf "Undefined tools %s@." s; exit 1 in let tools = list_flatten_rev (List.map lookup tools) in let probs = get_stringl section "probs" in let lookup s = - try Mstr.find s mprobs with Not_found -> eprintf "Undefined probs %s@." s; + try Mstr.find s mprobs + with Not_found -> eprintf "Undefined probs %s@." s; exit 1 in let probs = List.map lookup probs in - let outputs = get_stringl ~default:[] section "probs" in + let outputs = get_stringl ~default:[] section "outputs" in let check = function | "average" -> Average | "timeline" -> Timeline | "csv" -> Csv - | s -> eprintf "Unknown output %s" s; exit 1 in + | s -> eprintf "Unknown output %s@." s; exit 1 in let outputs = List.map check outputs in Mstr.add name { btools = tools; bprobs = probs; boutputs = outputs} map let read_file wc f = let rc = from_file f in + let absf = absolute_filename (Filename.dirname f) in let tools = get_family rc "tools" in - let tools = List.fold_left (read_tools wc) Mstr.empty tools in + let tools = List.fold_left (read_tools absf wc) Mstr.empty tools in let probs = get_family rc "probs" in - let probs = List.fold_left read_probs Mstr.empty probs in + let probs = List.fold_left (read_probs absf) Mstr.empty probs in let benchs = get_family rc "bench" in - let benchs = List.fold_left (read_bench tools probs) Mstr.empty benchs in + let benchs = List.fold_left (read_bench tools probs) + Mstr.empty benchs in {tools = tools; probs = probs; benchs = benchs} diff --git a/src/bench/benchrc.mli b/src/bench/benchrc.mli index bde6c7af18..cfd779464f 100644 --- a/src/bench/benchrc.mli +++ b/src/bench/benchrc.mli @@ -43,26 +43,16 @@ open Bench open Why open Util -type output = - (** on stdout *) - |Average - |Timeline - (** In a file *) - |Csv - - -type bench = - { - (* tool_name, prover_name *) - btools : (string * string) tool list; - (* prob_name, file_name, theory name *) - bprobs : (string * string * string) prob list; - boutputs : output list; - } - -type benchrc = { tools : (string * string) tool list Mstr.t; - probs : (string * string * string) prob Mstr.t; - benchs : bench Mstr.t + +type id_tool = (string * string) +(* tool_name, prover_name *) + +type id_prob = (string * string * string) +(* prob_name, file_name, theory name *) + +type benchrc = { tools : id_tool tool list Mstr.t; + probs : id_prob prob Mstr.t; + benchs : (id_tool,id_prob) bench Mstr.t } val read_file : Whyconf.config -> string -> benchrc diff --git a/src/bench/whybench.ml b/src/bench/whybench.ml index 6519b0a485..3044bc8328 100644 --- a/src/bench/whybench.ml +++ b/src/bench/whybench.ml @@ -97,6 +97,7 @@ let opt_output = ref None let opt_timelimit = ref None let opt_memlimit = ref None let opt_task = ref None +let opt_benchrc = ref [] let opt_print_theory = ref false let opt_print_namespace = ref false @@ -131,7 +132,9 @@ let option_list = Arg.align [ "-I", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath), " same as -L (obsolete)"; "-P", Arg.String (fun s -> opt_prover := s::!opt_prover), - "Add <prover> in the bench"; + "<prover> Add <prover> in the bench"; + "-B", Arg.String (fun s -> opt_benchrc := s::!opt_benchrc), + "<bench> Read one bench configuration file from <bench>"; "--prover", Arg.String (fun s -> opt_prover := s::!opt_prover), " same as -P"; "-F", Arg.String (fun s -> opt_parser := Some s), @@ -181,6 +184,7 @@ let option_list = Arg.align [ let tools = ref [] let probs = ref [] +let benchs = ref [] let () = try @@ -261,11 +265,6 @@ let () = end; if !opt_list then exit 0; - if Queue.is_empty opt_queue then begin - Arg.usage option_list usage_msg; - exit 1 - end; - (* Someting else using rc file intead of driver will be added later *) (* if !opt_prover <> None && !opt_driver <> None then begin *) (* eprintf "Options '-P'/'--prover' and \ *) @@ -273,9 +272,12 @@ let () = (* exit 1 *) (* end; *) - if !opt_prover = [] then begin - eprintf "At least one prover is required.@."; - exit 1 end; + if !opt_benchrc = [] && (!opt_prover = [] || Queue.is_empty opt_queue) then + begin + eprintf "At least one bench is required or one prover and one file.@."; + Arg.usage option_list usage_msg; + exit 1 + end; opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main); if !opt_timelimit = None then opt_timelimit := Some (Whyconf.timelimit main); @@ -291,7 +293,7 @@ let () = let prover = try Mstr.find s (get_provers config) with | Not_found -> eprintf "Prover %s not found.@." s; exit 1 in - { B.tval = s; + { B.tval = "cmdline",s; ttrans = Trans.identity; tdriver = load_driver env prover.driver; tcommand = prover.command; @@ -309,7 +311,6 @@ let () = in List.fold_left lookup Trans.identity_l !opt_trans in - let fold_prob acc = function | None, _ -> acc | Some f, _ -> @@ -325,7 +326,7 @@ let () = let th = Mnm.bindings m in let map (name,th) = name,Task.split_theory th None task in let fold acc (n,l) = - List.rev_append (List.map (fun v -> (n,v)) l) acc in + List.rev_append (List.map (fun v -> (("cmdline","",n),v)) l) acc in th |> List.map map |> List.fold_left fold [] in (* let gen = Env.Wenv.memoize 3 (fun env -> *) (* let memo = Trans.store (fun task -> gen env task) in *) @@ -334,83 +335,66 @@ let () = { B.ptask = gen; ptrans = fun _ -> transl; }::acc in - probs := Queue.fold fold_prob [] opt_queue + probs := Queue.fold fold_prob [] opt_queue; + + benchs := List.map (Benchrc.read_file config) !opt_benchrc with e when not (Debug.test_flag Debug.stack_trace) -> eprintf "%a@." Exn_printer.exn_printer e; exit 1 -(** valid * timeout * unknown * invalid *) -type nb_avg = int * float - -let add_nb_avg (nb,avg) time = - (succ nb, ((float nb) *. avg +. time) /. (float (succ nb))) -let empty_nb_avg = (0,0.) -let print_nb_avg fmt (nb,avg) = fprintf fmt "%i : %.2f" nb avg -type tool_res = - { valid : nb_avg; - timeout : nb_avg; - unknown : nb_avg; - invalid : nb_avg; - failure : nb_avg} - -let empty_tool_res = - { valid = empty_nb_avg; - timeout = empty_nb_avg; - unknown = empty_nb_avg; - invalid = empty_nb_avg; - failure = empty_nb_avg; - } - -let count_result = - let m = Mnm.empty in - let fold m res = - let tr = Mnm.find_default res.B.tool empty_tool_res m in - let r = res.B.result in - let tr = match r.C.pr_answer with - | C.Valid -> {tr with valid = add_nb_avg tr.valid r.C.pr_time} - | C.Timeout -> {tr with timeout = add_nb_avg tr.timeout r.C.pr_time} - | C.Invalid -> {tr with invalid = add_nb_avg tr.invalid r.C.pr_time} - | C.Unknown _ -> {tr with unknown = add_nb_avg tr.unknown r.C.pr_time} - | C.Failure _ | C.HighFailure -> - {tr with failure = add_nb_avg tr.failure r.C.pr_time} in - Mnm.add res.B.tool tr m in - List.fold_left fold m - let () = Scheduler.async := (fun f v -> ignore (Thread.create f v)) +let print_result l = + let tool_res = List.map (fun (t,l) -> t,B.compute_average l) l in + let print_tool_res ((_,tool_name),tool_res) = + printf "%a - %s@." B.print_tool_res tool_res tool_name in + printf "(v,t,u,f,i) - valid, unknown, timeout, invalid, failure@."; + List.iter print_tool_res tool_res + +let print_timeline l = + let l = List.map (fun (t,l) -> t,B.filter_timeline l) l in + let max = List.fold_left (fun acc (_,l) -> max acc (B.max_time l)) 0. l in + let step = max/.10. in + let tl = List.map (fun (t,l) -> t,B.compute_timeline 0. max step l) l in + let print_timeline ((_,tool_name),timeline) = + printf "@[%a - %s@]@." + (Pp.print_list Pp.comma (fun fmt -> fprintf fmt "%.3i")) + timeline tool_name in + printf "@[%a@]@." + (Pp.print_iter1 (fun f -> iterf f 0. max) + Pp.comma (fun fmt -> fprintf fmt "%.3f")) + step; + List.iter print_timeline tl + let () = let m = Mutex.create () in - let callback tool prob task i res = + let callback (_,tool) (_,_,prob) task i res = Mutex.lock m; printf "%s %a %i with %s : %a@." prob Pretty.print_pr (task_goal task) i tool Scheduler.print_pas res; Mutex.unlock m in - let l = B.all_list ~callback !tools !probs in - (* let print_result fmt res = *) - (* fprintf fmt "%s %a %i with %s : %a@." *) - (* res.B.prob Pretty.print_pr *) - (* (task_goal res.B.task) res.B.idtask res.B.tool *) - (* C.print_prover_result res.B.result in *) - (* eprintf "Done :@.%a@." *) - (* (Pp.print_list Pp.newline print_result) l *) - let tool_res = count_result l in - let print_tool_res tool_name tool_res = - printf "(%a, %a, %a, %a, %a) - %s@." - print_nb_avg tool_res.valid - print_nb_avg tool_res.unknown - print_nb_avg tool_res.timeout - print_nb_avg tool_res.invalid - print_nb_avg tool_res.failure - tool_name in - printf "(v,t,u,f,i) - valid, unknown, timeout, invalid, failure@."; - Mnm.iter print_tool_res tool_res + let l = B.all_list_tools ~callback !tools !probs in + print_result l; + let callback (_,tool) (_,file,prob) task i res = + Mutex.lock m; + printf "%s.%s %a %i with %s : %a@." + file prob Pretty.print_pr (task_goal task) i tool + Scheduler.print_pas res; + Mutex.unlock m + in + let benchs = + List.map (fun b -> List.map snd (Mstr.bindings b.Benchrc.benchs)) + !benchs in + let bl = B.run_benchs_tools ~callback (list_flatten_rev benchs) in + List.iter (fun (_,l) -> print_result l) bl; + List.iter (fun (_,l) -> print_timeline l) bl (* Local Variables: -compile-command: "unset LANG; make -C ../.. bin/whybench.byte" +compile-command: "unset LANG; make -j -C ../.. bin/whybench.byte" End: *) diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml index b5268ea3f3..b1c9c301f8 100644 --- a/src/ide/gmain.ml +++ b/src/ide/gmain.ml @@ -1001,7 +1001,6 @@ let redo_external_proof q g a = in Db.set_status a.Model.proof_db db_res time in - GtkThread.sync (callback Model.Scheduled 0.0) ""; let old = if a.Model.edited_as = "" then None else begin eprintf "Info: proving using edited file %s@." a.Model.edited_as; diff --git a/src/ide/scheduler.ml b/src/ide/scheduler.ml index 18fade88a2..2aa350d5c9 100644 --- a/src/ide/scheduler.ml +++ b/src/ide/scheduler.ml @@ -183,7 +183,6 @@ let event_handler () = !scheduled_proofs !maximum_running_proofs; Mutex.unlock queue_lock; (* build the prover task from goal in [a] *) - !async (fun () -> callback Scheduled) (); try let call_prover : unit -> unit -> Call_provers.prover_result = (* @@ -255,6 +254,7 @@ let (_scheduler_thread : Thread.t) = let schedule_proof_attempt ~debug ~timelimit ~memlimit ?old ~command ~driver ~callback goal = + !async (fun () -> callback Scheduled) (); Mutex.lock queue_lock; Queue.push (debug,timelimit,memlimit,old,command,driver,callback,goal) prover_attempts_queue; @@ -267,6 +267,8 @@ let create_proof_attempt ~debug ~timelimit ~memlimit ?old (debug,timelimit,memlimit,old,command,driver,callback,goal) let transfer_proof_attempts q = + Queue.iter (fun (_,_,_,_,_,_,callback,_) -> + !async (fun () -> callback Scheduled) ()) q; Mutex.lock queue_lock; Queue.transfer q prover_attempts_queue; Condition.signal queue_condition; diff --git a/src/ide/scheduler.mli b/src/ide/scheduler.mli index d8c82984b7..6eda959d57 100644 --- a/src/ide/scheduler.mli +++ b/src/ide/scheduler.mli @@ -76,8 +76,8 @@ val create_proof_attempt : debug:bool -> timelimit:int -> memlimit:int -> Task.task -> attempt val transfer_proof_attempts : attempt Queue.t -> unit -(** same as the iteration of {!schedule_proof_attempt} but runs in - constant time. The given queue is cleared. *) +(** same as the iteration of {!schedule_proof_attempt}. + The given queue is cleared. *) val schedule_some_proof_attempts : diff --git a/src/util/rc.mll b/src/util/rc.mll index 447faf2128..83c2af6e87 100644 --- a/src/util/rc.mll +++ b/src/util/rc.mll @@ -166,7 +166,7 @@ let get_value read ?default section key = let get_valueo read section key = try Some (get_value read section key) - with Not_found -> None + with MissingField _ -> None let get_valuel read ?default section key = try diff --git a/src/util/util.ml b/src/util/util.ml index d5d1f090a1..7bfbe50f5c 100644 --- a/src/util/util.ml +++ b/src/util/util.ml @@ -71,6 +71,11 @@ let rec foldi f acc min max = if min > max then acc else foldi f (f acc min) (succ min) max let rec mapi f = foldi (fun acc i -> f i::acc) [] +(* useful iterator on float *) +let rec iterf f min max step = + if min > max then () else + (f min; iterf f (min+.step) max step) + (* useful list combinators *) let rev_map_fold_left f acc l = diff --git a/src/util/util.mli b/src/util/util.mli index 1db119ebca..d1e5920e71 100644 --- a/src/util/util.mli +++ b/src/util/util.mli @@ -61,6 +61,10 @@ val option_map_fold : val foldi : ('a -> int -> 'a) -> 'a -> int -> int -> 'a val mapi : (int -> 'a) -> int -> int -> 'a list +(* useful float iterator *) +val iterf : (float -> unit) -> float -> float -> float -> unit +(** [iterf f min max step] *) + (* useful list combinators *) val rev_map_fold_left : -- GitLab