diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 49 | ||||
| -rw-r--r-- | stm/stm.mli | 5 |
2 files changed, 25 insertions, 29 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 3324df3066..c078dbae56 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -44,7 +44,6 @@ module AsyncOpts = struct async_proofs_mode : async_proofs; async_proofs_private_flags : string option; - async_proofs_full : bool; async_proofs_never_reopen_branch : bool; async_proofs_tac_error_resilience : tac_error_filter; @@ -61,7 +60,6 @@ module AsyncOpts = struct async_proofs_mode = APoff; async_proofs_private_flags = None; - async_proofs_full = false; async_proofs_never_reopen_branch = false; async_proofs_tac_error_resilience = `Only [ "curly" ]; @@ -1442,11 +1440,14 @@ end = struct (* {{{ *) let perspective = ref [] let set_perspective l = perspective := l + let is_inside_perspective st = true + (* This code is now disabled. If an IDE needs this feature, make it accessible again. + List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) st + *) + let task_match age t = match age, t with - | Fresh, BuildProof { t_states } -> - not !cur_opt.async_proofs_full || - List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states + | Fresh, BuildProof { t_states } -> is_inside_perspective t_states | Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l | _ -> false @@ -1482,8 +1483,7 @@ end = struct (* {{{ *) feedback (InProgress ~-1); t_assign (`Val pl); record_pb_time ?loc:t_loc t_name time; - if !cur_opt.async_proofs_full || t_drop - then `Stay(t_states,[States t_states]) + if t_drop then `Stay(t_states,[States t_states]) else `End | Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } -> @@ -2126,8 +2126,7 @@ end = struct (* {{{ *) TaskQueue.enqueue_task (Option.get !queue) QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch - let init () = queue := Some (TaskQueue.create - (if !cur_opt.async_proofs_full then 1 else 0)) + let init () = queue := Some (TaskQueue.create 0) end (* }}} *) @@ -2150,7 +2149,6 @@ let async_policy () = let delegate name = get_hint_bp_time name >= !cur_opt.async_proofs_delegation_threshold || VCS.is_vio_doc () - || !cur_opt.async_proofs_full let collect_proof keep cur hd brkind id = stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); @@ -2257,8 +2255,7 @@ let collect_proof keep cur hd brkind id = else let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc - else if (is_vtkeep keep) && - (not(State.is_cached_and_valid id) || !cur_opt.async_proofs_full) + else if (is_vtkeep keep) && (not(State.is_cached_and_valid id)) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -2646,13 +2643,14 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = name by looking at the load path! *) List.iter Mltop.add_coq_path iload_path; + Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; + begin match doc_type with | Interactive ln -> let dp = match ln with | TopLogical dp -> dp | TopPhysical f -> dirpath_of_file f in - Safe_typing.allow_delayed_constants := true; Declaremods.start_library dp | VoDoc f -> @@ -2663,7 +2661,6 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = set_compilation_hints f | VioDoc f -> - Safe_typing.allow_delayed_constants := true; let ldir = dirpath_of_file f in check_coq_overwriting ldir; let () = Flags.verbosely Declaremods.start_library ldir in @@ -2842,12 +2839,12 @@ let process_back_meta_command ~newtip ~head oid aast w = Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok let allow_nested_proofs = ref false -let _ = Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "Nested Proofs Allowed"; - Goptions.optkey = Vernac_classifier.stm_allow_nested_proofs_option_name; - Goptions.optread = (fun () -> !allow_nested_proofs); - Goptions.optwrite = (fun b -> allow_nested_proofs := b) } +let () = Goptions.(declare_bool_option + { optdepr = false; + optname = "Nested Proofs Allowed"; + optkey = Vernac_classifier.stm_allow_nested_proofs_option_name; + optread = (fun () -> !allow_nested_proofs); + optwrite = (fun b -> allow_nested_proofs := b) }) let process_transaction ~doc ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = @@ -2869,11 +2866,10 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtQuery, w -> let id = VCS.new_node ~id:newtip () in let queue = - if !cur_opt.async_proofs_full then `QueryQueue (ref false) - else if VCS.is_vio_doc () && - VCS.((get_branch head).kind = `Master) && - may_pierce_opaque (Vernacprop.under_control x.expr) - then `SkipQueue + if VCS.is_vio_doc () && + VCS.((get_branch head).kind = `Master) && + may_pierce_opaque (Vernacprop.under_control x.expr) + then `SkipQueue else `MainQueue in VCS.commit id (mkTransCmd x [] false queue); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok @@ -3206,8 +3202,7 @@ let edit_at ~doc id = VCS.delete_boxes_of id; VCS.gc (); VCS.print (); - if not !cur_opt.async_proofs_full then - Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in try diff --git a/stm/stm.mli b/stm/stm.mli index 0c0e19ce5c..b6071fa56b 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -16,7 +16,9 @@ open Names module AsyncOpts : sig type cache = Force - type async_proofs = APoff | APonLazy | APon + type async_proofs = APoff + | APonLazy (* Delays proof checking, but does it in master *) + | APon type tac_error_filter = [ `None | `Only of string list | `All ] type stm_opt = { @@ -27,7 +29,6 @@ module AsyncOpts : sig async_proofs_mode : async_proofs; async_proofs_private_flags : string option; - async_proofs_full : bool; async_proofs_never_reopen_branch : bool; async_proofs_tac_error_resilience : tac_error_filter; |