From de2d78235556d79b4de1b79c90fe6df68d31630a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 11 Jul 2022 14:08:11 +0200 Subject: [PATCH] [toplevel] move check_pending_proofs to common_compile and remove use of legacy API --- ide/coqide/idetop.ml | 10 +++++----- stm/stm.ml | 13 ++++++++++--- stm/stm.mli | 4 ++-- toplevel/ccompile.ml | 21 ++++----------------- toplevel/common_compile.ml | 14 ++++++++++++++ toplevel/common_compile.mli | 6 +++++- vernac/vernacstate.mli | 1 + 7 files changed, 41 insertions(+), 28 deletions(-) diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index c27e56df59ff..c131f80719ac 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -226,7 +226,7 @@ let export_pre_goals flags Proof.{ sigma; goals; stack } process = let subgoals flags = let doc = get_doc () in - set_doc @@ Stm.finish ~doc; + set_doc @@ fst @@ Stm.finish ~doc; let short = match flags.Interface.gf_mode with | "short" -> true | _ -> false @@ -257,7 +257,7 @@ let goals () = let evars () = try let doc = get_doc () in - set_doc @@ Stm.finish ~doc; + set_doc @@ fst @@ Stm.finish ~doc; let pfts = Vernacstate.Declare.give_me_the_proof () in let Proof.{ sigma } = Proof.data pfts in let exl = Evar.Map.bindings (Evd.undefined_map sigma) in @@ -291,9 +291,9 @@ let status force = (* We remove the initial part of the current [DirPath.t] (usually Top in an interactive session, cf "coqtop -top"), and display the other parts (opened sections and modules) *) - set_doc (Stm.finish ~doc:(get_doc ())); + set_doc (fst @@ Stm.finish ~doc:(get_doc ())); if force then - set_doc (Stm.join ~doc:(get_doc ())); + set_doc (fst @@ Stm.join ~doc:(get_doc ())); let path = let l = Names.DirPath.repr (Lib.cwd ()) in List.rev_map Names.Id.to_string l @@ -467,7 +467,7 @@ let init = get_doc (), init_sid, `NewTip in if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; - set_doc (Stm.finish ~doc); + set_doc (fst @@ Stm.finish ~doc); initial_id end diff --git a/stm/stm.ml b/stm/stm.ml index 0298c894f9eb..e295c307e54f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2429,7 +2429,11 @@ let observe ~doc id = let finish ~doc = let head = VCS.current_branch () in let doc = observe ~doc (VCS.get_branch_pos head) in - VCS.print (); doc + let tip = VCS.cur_tip () in + if not (State.is_cached ~cache:true tip) then + CErrors.anomaly Pp.(str "Stm.join: tip not cached"); + VCS.print (); + doc, State.get_cached tip let wait ~doc = let doc = observe ~doc (VCS.get_branch_pos VCS.Branch.master) in @@ -2469,8 +2473,11 @@ let join ~doc = stm_prerr_endline (fun () -> "Checking no error states"); ignore(check_no_err_states ~doc (Stateid.Set.singleton Stateid.initial) (VCS.get_branch_pos VCS.Branch.master)); + let tip = VCS.cur_tip () in + if not (State.is_cached ~cache:true tip) then + CErrors.anomaly Pp.(str "Stm.join: tip not cached"); VCS.print (); - doc + doc, State.get_cached tip type tasks = Opaqueproof.opaque_handle option Slaves.tasks let check_task name tasks i = @@ -2534,7 +2541,7 @@ let handle_failure (e, info) vcs = Exninfo.iraise (e, info) let snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_vo = - let doc = finish ~doc in + let doc, _ = finish ~doc in if List.length (VCS.branches ()) > 1 then CErrors.user_err (str"Cannot dump a vio with open proofs."); (* LATER: when create_vos is true, it could be more efficient to not allocate the futures; but for now it seems useful for synchronization of the workers, diff --git a/stm/stm.mli b/stm/stm.mli index 89b6cad3d504..208e280dadb2 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -130,7 +130,7 @@ val edit_at : doc:doc -> Stateid.t -> doc * edit_focus val observe : doc:doc -> Stateid.t -> doc (* [finish doc] Fully checks a document up to the "current" tip. *) -val finish : doc:doc -> doc +val finish : doc:doc -> doc * Vernacstate.t (* Internal use (fake_ide) only, do not use *) val wait : doc:doc -> doc @@ -138,7 +138,7 @@ val wait : doc:doc -> doc val stop_worker : string -> unit (* Joins the entire document. Implies finish, but also checks proofs *) -val join : doc:doc -> doc +val join : doc:doc -> doc * Vernacstate.t (* Saves on the disk a .vio corresponding to the current status: - if the worker pool is empty, all tasks are saved diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 86ea33d36812..787a23cf5396 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Pp open Coqargs open Coqcargs open Common_compile @@ -21,18 +20,6 @@ let create_empty_file filename = let f = open_out filename in close_out f -let check_pending_proofs filename = - let pfs = Vernacstate.Declare.get_all_proof_names () [@ocaml.warning "-3"] in - if not (CList.is_empty pfs) then - fatal_error (str "There are pending proofs in file " ++ str filename ++ str": " - ++ (pfs - |> List.rev - |> prlist_with_sep pr_comma Names.Id.print) - ++ str "."); - let pm = Vernacstate.Declare.get_program () [@ocaml.warning "-3"] in - let what_for = Pp.str ("file " ^ filename) in - NeList.iter (fun pm -> Declare.Obls.check_solved_obligations ~what_for ~pm) pm - (* Compile a vernac file *) let compile opts stm_options injections copts ~echo ~f_in ~f_out = let open Vernac.State in @@ -75,9 +62,9 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out = let wall_clock1 = Unix.gettimeofday () in let check = Stm.AsyncOpts.(stm_options.async_proofs_mode = APoff) in let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state ~ldir long_f_dot_in in - let _doc = Stm.join ~doc:state.doc in + let doc, state = Stm.join ~doc:state.doc in let wall_clock2 = Unix.gettimeofday () in - check_pending_proofs long_f_dot_in; + ensure_no_pending_proofs ~filename:long_f_dot_in state; (* In .vo production, dump a complete .vo file. *) if mode = BuildVo then Library.save_library_to ~output_native_objects Library.ProofsTodoNone ldir long_f_dot_out; @@ -116,8 +103,8 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out = let state = Load.load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_in in - let doc = Stm.finish ~doc:state.doc in - check_pending_proofs long_f_dot_in; + let doc, state = Stm.finish ~doc:state.doc in + ensure_no_pending_proofs state ~filename:long_f_dot_in; let create_vos = (mode = BuildVos) in (* In .vos production, the output .vos file contains compiled statements. In .vio production, the output .vio file contains compiled statements and suspended proofs. *) diff --git a/toplevel/common_compile.ml b/toplevel/common_compile.ml index a6ef6dc62f05..e1a98528237d 100644 --- a/toplevel/common_compile.ml +++ b/toplevel/common_compile.ml @@ -53,3 +53,17 @@ let ensure_exists_with_prefix ~src ~tgt:f_out ~src_ext ~tgt_ext = | None -> safe_chop_extension long_f_dot_src ^ tgt_ext | Some f -> ensure ~ext:tgt_ext ~src:long_f_dot_src ~tgt:f in long_f_dot_src, long_f_dot_tgt + +let ensure_no_pending_proofs ~filename s = + match s.Vernacstate.lemmas with + | Some lemmas -> + let pfs = Vernacstate.LemmaStack.get_all_proof_names lemmas in + fatal_error (str "There are pending proofs in file " ++ str filename ++ str": " + ++ (pfs + |> List.rev + |> prlist_with_sep pr_comma Names.Id.print) + ++ str "."); + | None -> + let pm = s.Vernacstate.program in + let what_for = Pp.str ("file " ^ filename) in + NeList.iter (fun pm -> Declare.Obls.check_solved_obligations ~what_for ~pm) pm diff --git a/toplevel/common_compile.mli b/toplevel/common_compile.mli index 1fcae8e4af31..66fe3320329d 100644 --- a/toplevel/common_compile.mli +++ b/toplevel/common_compile.mli @@ -26,5 +26,9 @@ val ensure_exists : string -> unit [src_ext] and [tgt_ext] are expected to begin with dot, eg [".v"]. *) val ensure_exists_with_prefix : src:string -> tgt:string option -> src_ext:string -> tgt_ext:string -> string * string -(* [safe_chop_extension f] is like Filename.chop_extension but fail safe *) +(* [chop_extension f] is like Filename.chop_extension but fail safe *) val safe_chop_extension : string -> string + +(* [ensure_no_pending_proofs ~filename] checks that no proof or obligation + is open *) +val ensure_no_pending_proofs : filename:string -> Vernacstate.t -> unit diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index f9f265b62e55..f2df931261ed 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -40,6 +40,7 @@ module LemmaStack : sig val map_top : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t val with_top : t -> f:(Declare.Proof.t -> 'a ) -> 'a val get_top : t -> Declare.Proof.t + val get_all_proof_names : t -> Names.Id.t list end