[toplevel] move check_pending_proofs to common_compile

and remove use of legacy API

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
 

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,

stm/stm.mli

@@ -130,15 +130,15 @@ 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
 
 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

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. *)

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

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

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