diff options
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | lib/flags.mli | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 10 | ||||
| -rw-r--r-- | test-suite/Makefile | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
5 files changed, 20 insertions, 3 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 2bc217fa3..0356863ab 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -50,6 +50,8 @@ let compilation_mode = ref BuildVo type async_proofs = APoff | APonLazy | APon let async_proofs_mode = ref APoff +type cache = Force +let async_proofs_cache = ref None let async_proofs_n_workers = ref 1 let async_proofs_n_tacworkers = ref 2 let async_proofs_private_flags = ref None diff --git a/lib/flags.mli b/lib/flags.mli index 98f0acb95..f94d80ffc 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -17,6 +17,8 @@ val compilation_mode : compilation_mode ref type async_proofs = APoff | APonLazy | APon val async_proofs_mode : async_proofs ref +type cache = Force +val async_proofs_cache : cache option ref val async_proofs_n_workers : int ref val async_proofs_n_tacworkers : int ref val async_proofs_private_flags : string option ref diff --git a/stm/stm.ml b/stm/stm.ml index e5e156a4d..449f5897e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1362,6 +1362,9 @@ let known_state ?(redefine_qed=false) ~cache id = inject_non_pstate s ), cache in + let cache_step = + if !Flags.async_proofs_cache = Some Flags.Force then `Yes + else cache_step in if Flags.async_proofs_is_master () then Pp.feedback ~state_id:id Feedback.ProcessingInMaster; State.define ~cache:cache_step ~redefine:redefine_qed step id; @@ -1470,7 +1473,8 @@ end = struct let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun n (id,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - if n = 1 && !Flags.coqtop_ui then VtStm (VtBack oid, false), VtNow + if n = 1 && !Flags.coqtop_ui && not !Flags.batch_mode then + VtStm (VtBack oid, false), VtNow else VtStm (VtBack oid, true), VtLater | VernacUndoTo _ | VernacRestart as e -> @@ -1684,7 +1688,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); VCS.commit id (Alias oid); - Pp.msg_notice (pr_open_cur_subgoals ()); + if (!Flags.coqtop_ui && not !Flags.batch_mode) || + !Flags.print_emacs then + Pp.msg_notice (pr_open_cur_subgoals ()); Backtrack.record (); if w == VtNow then finish (); `Ok | VtStm (VtBack id, false), VtNow -> prerr_endline ("undo to state " ^ Stateid.to_string id); diff --git a/test-suite/Makefile b/test-suite/Makefile index 0f7abb78e..74e806138 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -33,7 +33,7 @@ LIB := .. coqtop := $(BIN)coqtop -boot -q -batch -R prerequisite TestSuite bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite -command := $(coqtop) -top Top -load-vernac-source +command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source coqc := $(coqtop) -compile coqdep := $(BIN)coqdep -coqlib $(LIB) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 3eee9658e..3525d93c6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -250,6 +250,11 @@ let get_async_proofs_mode opt = function | "lazy" -> Flags.APonLazy | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 +let get_cache opt = function + | "force" -> Some Flags.Force + | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 + + let set_worker_id opt s = assert (s <> "master"); Flags.async_proofs_worker_id := s @@ -373,6 +378,8 @@ let parse_args arglist = Flags.async_proofs_mode := get_async_proofs_mode opt (next()) |"-async-proofs-j" -> Flags.async_proofs_n_workers := (get_int opt (next ())) + |"-async-proofs-cache" -> + Flags.async_proofs_cache := get_cache opt (next ()) |"-async-proofs-tac-j" -> Flags.async_proofs_n_tacworkers := (get_int opt (next ())) |"-async-proofs-worker-priority" -> |