Commit 378a2514 authored by François Bobot's avatar François Bobot

In the thread why I musn't call do_why_sync :)

parent 0b42a2ce
......@@ -111,23 +111,21 @@ let read_probs absf map (name,section) =
(* files *)
let files = get_stringl ~default:[] section "file" in
let gen env task =
let fwhy () =
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
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
with exn -> eprintf "%a@." Exn_printer.exn_printer exn; exit 1
in
Mstr.add name { ptask = gen; ptrans = gen_trans} map
let read_bench absf mtools mprobs map (name,section) =
......
......@@ -347,7 +347,7 @@ let do_why_sync funct argument =
let c = Condition.create () in
let r = ref None in
let cb res =
Mutex.lock m; r := Some res; Mutex.unlock m; Condition.signal c in
Mutex.lock m; r := Some res; Condition.signal c; Mutex.unlock m in
do_why ~callback:cb funct argument;
Mutex.lock m; Condition.wait c m;
Mutex.lock m; while !r = None do Condition.wait c m done;
Util.of_option !r
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