diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 100 | ||||
| -rw-r--r-- | stm/stm.mli | 5 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 13 |
3 files changed, 66 insertions, 52 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 9359ab15e2..94405924b7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -27,6 +27,9 @@ open Feedback open Vernacexpr open Vernacextend +let is_vtkeep = function VtKeep _ -> true | _ -> false +let get_vtkeep = function VtKeep x -> x | _ -> assert false + module AsyncOpts = struct type cache = Force @@ -41,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; @@ -58,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" ]; @@ -1439,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 @@ -1479,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 } -> @@ -1532,12 +1535,13 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in if not drop then begin let checked_proof = Future.chain future_proof (fun p -> + let opaque = Proof_global.Opaque in (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) Vernacstate.unfreeze_interp_state st; let pobject, _ = - Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in + Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in @@ -1545,7 +1549,7 @@ end = struct (* {{{ *) stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }) in + expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1680,9 +1684,10 @@ end = struct (* {{{ *) (* The original terminator, a hook, has not been saved in the .vio*) Proof_global.set_terminator (Lemmas.standard_proof_terminator [] - (Lemmas.mk_hook (fun _ _ -> ()))); + (Lemmas.mk_hook (fun _ _ -> ()))); + let opaque = Proof_global.Opaque in let proof = - Proof_global.close_proof ~keep_body_ucst_separate:true (fun x -> x) in + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No start; @@ -1695,7 +1700,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }); + expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }); `OK proof end with e -> @@ -2121,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 (* }}} *) @@ -2145,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); @@ -2252,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 (keep == VtKeep || keep == VtKeepAsAxiom) && - (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 @@ -2440,9 +2442,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ), `Yes, true | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> let rec aux = function - | `ASync (block_start, nodes, name, delegate) -> (fun () -> - assert(keep == VtKeep || keep == VtKeepAsAxiom); - let drop_pt = keep == VtKeepAsAxiom in + | `ASync (block_start, nodes, name, delegate) -> (fun () -> + let keep' = get_vtkeep keep in + let drop_pt = keep' == VtKeepAxiom in let block_stop, exn_info, loc = eop, (id, eop), x.loc in log_processing_async id name; VCS.create_proof_task_box nodes ~qed:id ~block_start; @@ -2450,11 +2452,11 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | { VCS.kind = `Edit _ }, None -> assert false | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> assert(redefine_qed = true); - if okeep != keep then + if okeep <> keep then msg_warning(strbrk("The command closing the proof changed. " ^"The kernel cannot take this into account and will " - ^(if keep == VtKeep then "not check " else "reject ") - ^"the "^(if keep == VtKeep then "new" else "incomplete") + ^(if not drop_pt then "not check " else "reject ") + ^"the "^(if not drop_pt then "new" else "incomplete") ^" proof. Reprocess the command declaring " ^"the proof's statement to avoid that.")); let fp, cancel = @@ -2477,8 +2479,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ~drop_pt exn_info block_stop, ref false in qed.fproof <- Some (fp, cancel); + let opaque = match keep' with + | VtKeepAxiom | VtKeepOpaque -> + Proof_global.Opaque (* Admitted -> Opaque should be OK. *) + | VtKeepDefined -> Proof_global.Transparent + in let proof = - Proof_global.close_future_proof ~feedback_id:id fp in + Proof_global.close_future_proof ~opaque ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; let st = Vernacstate.freeze_interp_state `No in @@ -2502,15 +2509,19 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let proof = match keep with | VtDrop -> None - | VtKeepAsAxiom -> + | VtKeep VtKeepAxiom -> let ctx = UState.empty in let fp = Future.from_val ([],ctx) in qed.fproof <- Some (fp, ref false); None - | VtKeep -> - Some(Proof_global.close_proof + | VtKeep opaque -> + let opaque = let open Proof_global in match opaque with + | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent + | VtKeepAxiom -> assert false + in + Some(Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (State.exn_on id ~valid:eop)) in - if keep != VtKeepAsAxiom then + if keep <> VtKeep VtKeepAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in let st = Vernacstate.freeze_interp_state `No in @@ -2632,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 -> @@ -2649,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 @@ -2714,7 +2725,7 @@ let rec join_admitted_proofs id = if Stateid.equal id Stateid.initial then () else let view = VCS.visit id in match view.step with - | `Qed ({ keep = VtKeepAsAxiom; fproof = Some (fp,_) },_) -> + | `Qed ({ keep = VtKeep VtKeepAxiom; fproof = Some (fp,_) },_) -> ignore(Future.force fp); join_admitted_proofs view.next | _ -> join_admitted_proofs view.next @@ -2827,13 +2838,12 @@ let process_back_meta_command ~newtip ~head oid aast w = VCS.commit id (Alias (oid,aast)); 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 get_allow_nested_proofs = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"Nested Proofs Allowed" + ~key:Vernac_classifier.stm_allow_nested_proofs_option_name + ~value:false let process_transaction ~doc ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = @@ -2855,11 +2865,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 @@ -2867,7 +2876,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) (* Proof *) | VtStartProof (mode, guarantee, names), w -> - if not !allow_nested_proofs && VCS.proof_nesting () > 0 then + if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on." |> Pp.str |> (fun s -> (UserError (None, s), Exninfo.null)) @@ -3192,8 +3201,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; diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 526858bd73..44d07279fc 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -26,8 +26,8 @@ let string_of_vernac_type = function | VtUnknown -> "Unknown" | VtStartProof _ -> "StartProof" | VtSideff _ -> "Sideff" - | VtQed VtKeep -> "Qed(keep)" - | VtQed VtKeepAsAxiom -> "Qed(admitted)" + | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)" + | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)" | VtQed VtDrop -> "Qed(drop)" | VtProofStep { parallel; proof_block_detection } -> "ProofStep " ^ string_of_parallel parallel ^ @@ -43,6 +43,10 @@ let string_of_vernac_when = function let string_of_vernac_classification (t,w) = string_of_vernac_type t ^ " " ^ string_of_vernac_when w +let vtkeep_of_opaque = let open Proof_global in function + | Opaque -> VtKeepOpaque + | Transparent -> VtKeepDefined + let idents_of_name : Names.Name.t -> Names.Id.t list = function | Names.Anonymous -> [] @@ -65,8 +69,9 @@ let classify_vernac e = VtSideff [], VtNow (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater - | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater - | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater + | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom), VtLater + | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque)), VtLater + | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque), VtLater (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ | VernacCheckMayEval _ -> VtQuery, VtLater |