Fix "tip not cached" anomaly when there are open proofs at file end

Fix #16335

ide/coqide/idetop.ml

@@ -305,8 +305,7 @@ let status force =
      (usually Top in an interactive session, cf "coqtop -top"),
      and display the other parts (opened sections and modules) *)
   ignore (Stm.finish ~doc:(get_doc ()) : Vernacstate.t);
-  if force then
-    ignore (Stm.join ~doc:(get_doc ()) : Vernacstate.t);
+  if force then Stm.join ~doc:(get_doc ());
   let path =
     let l = Names.DirPath.repr (Lib.cwd ()) in
     List.rev_map Names.Id.to_string l

stm/stm.ml

@@ -2429,7 +2429,7 @@ let finish ~doc =
   let () = observe ~doc (VCS.get_branch_pos head) in
   let tip = VCS.cur_tip () in
   if not (State.is_cached ~cache:true tip) then
-    CErrors.anomaly Pp.(str "Stm.join: tip not cached");
+    CErrors.anomaly Pp.(str "Stm.finish: tip not cached");
   VCS.print ();
   State.get_cached tip
 
@@ -2473,8 +2473,7 @@ let join ~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 ();
-  State.get_cached tip
+  VCS.print ()
 
 type tasks = Opaqueproof.opaque_handle option Slaves.tasks
 let check_task name tasks i =

stm/stm.mli

@@ -136,7 +136,7 @@ val wait : doc:doc -> unit
 val stop_worker : string -> unit
 
 (* Joins the entire document.  Implies finish, but also checks proofs *)
-val join : doc:doc -> Vernacstate.t
+val join : doc:doc -> unit
 
 (* Saves on the disk a .vio corresponding to the current status:
    - if the worker pool is empty, all tasks are saved

test-suite/output/bug_16335.out

@@ -0,0 +1,3 @@
+Error: There are pending proofs in file ./output/bug_16335.v: foo.
+
+coqc exited with code 1

test-suite/output/bug_16335.v

@@ -0,0 +1,2 @@
+Lemma foo: True.
+Proof.

toplevel/ccompile.ml

@@ -68,9 +68,10 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out =
       let check = Stm.AsyncOpts.(stm_options.async_proofs_mode = APoff) in
       let source = source copts ldir long_f_dot_in in
       let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state ~source long_f_dot_in in
-      let state = Stm.join ~doc:state.doc in
+      let fullstate = Stm.finish ~doc:state.doc in
+      ensure_no_pending_proofs ~filename:long_f_dot_in fullstate;
+      let () = Stm.join ~doc:state.doc in
       let wall_clock2 = Unix.gettimeofday () 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;