From d6e4513b844dbd551164868819c3a6ac9baf6c45 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 18 Mar 2014 16:20:57 +0100 Subject: STM: make -async-proofs on work from coqc too --- library/declaremods.ml | 2 +- library/library.ml | 17 ++++------------- toplevel/stm.ml | 2 +- toplevel/vernac.ml | 1 + 4 files changed, 7 insertions(+), 15 deletions(-) diff --git a/library/declaremods.ml b/library/declaremods.ml index 2b917587c..bb623b7a1 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -874,8 +874,8 @@ let start_library dir = Lib.add_frozen_state () let end_library dir = - let prefix, lib_stack = Lib.end_compilation dir in let mp,cenv,ast = Global.export dir in + let prefix, lib_stack = Lib.end_compilation dir in assert (ModPath.equal mp (MPfile dir)); let substitute, keep, _ = Lib.classify_segment lib_stack in cenv,(substitute,keep),ast diff --git a/library/library.ml b/library/library.ml index b75329a22..fd391344c 100644 --- a/library/library.ml +++ b/library/library.ml @@ -373,8 +373,6 @@ module OpaqueTables = struct module FMap = Map.Make(Future.UUID) let f2t = ref FMap.empty - let get_opaque_nolib _ i = (!local_opaque_table).(i) - let get_opaque dp i = if DirPath.equal dp (Lib.library_dp ()) then (!local_opaque_table).(i) @@ -382,13 +380,11 @@ module OpaqueTables = struct let join_local_opaque dp i = if DirPath.equal dp (Lib.library_dp ()) then - Future.sink (!local_opaque_table).(i) + ignore(Future.force (!local_opaque_table).(i)) let join_local_univ dp i = if DirPath.equal dp (Lib.library_dp ()) then - Future.sink (!local_univ_table).(i) - - let get_univ_nolib _ i = Some (!local_univ_table).(i) + ignore(Future.join (!local_univ_table).(i)) let get_univ dp i = if DirPath.equal dp (Lib.library_dp ()) @@ -410,8 +406,8 @@ module OpaqueTables = struct local_discharge_table := t end; let c, u = Future.split2 ~greedy:true cu in - if Future.is_val u then ignore(Future.join u); - if Future.is_val c then ignore(Future.join c); + Future.sink u; + Future.sink c; (!local_opaque_table).(n) <- c; (!local_univ_table).(n) <- u; (!local_discharge_table).(n) <- d; @@ -737,11 +733,6 @@ let save_library_to ?todo dir f = f ^ "i", (fun x -> Some (d x)), (fun x -> Some (x,Univ.empty_constraint,false)), (fun x -> Some x) in Opaqueproof.reset_indirect_creator (); - (* HACK: end_library resets Lib and then joins the safe env. To join the - * env one needs to access the futures stored in the tables. Standard - * accessors use Lib. Hence *) - Opaqueproof.set_indirect_opaque_accessor OpaqueTables.get_opaque_nolib; - Opaqueproof.set_indirect_univ_accessor OpaqueTables.get_univ_nolib; let cenv, seg, ast = Declaremods.end_library dir in let opaque_table, univ_table, disch_table, f2t_map = OpaqueTables.dump () in diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 1f127b4a0..84bfaaa70 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -1144,7 +1144,7 @@ let delegate_policy_check time = (!Flags.async_proofs_mode = Flags.APonParallel 0 || !Flags.async_proofs_mode = Flags.APonLazy) && time >= 1.0 else if !Flags.compilation_mode = Flags.BuildVi then true - else !Flags.async_proofs_mode <> Flags.APoff + else !Flags.async_proofs_mode <> Flags.APoff && time >= 1.0 let collect_proof cur hd brkind id = prerr_endline ("Collecting proof ending at "^Stateid.to_string id); diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 27509fcc0..e887204c3 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -318,6 +318,7 @@ let compile verbosely f = match !Flags.compilation_mode with | BuildVo -> let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in + Stm.set_compilation_hints long_f_dot_v; Aux_file.start_aux_file_for long_f_dot_v; Dumpglob.start_dump_glob long_f_dot_v; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); -- cgit v1.2.3