Merge PR #17620: Fix "tip not cached" anomaly when there are open pro…

…ofs at file end

Reviewed-by: Alizter
Co-authored-by: Alizter <Alizter@users.noreply.github.com>

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

@@ -1189,17 +1189,16 @@ end = struct (* {{{ *)
       match np with
       | None -> None
       | Some cp ->
-        let did = ref id in
-        let rv = ref np in
-        let done_ = ref false in
-        while not !done_ do
-          did := fold_until back_tactic 1 !did;
-          rv := get_proof ~doc !did;
-          done_ := match !rv with
-            | Some rv -> not (Evar.Set.equal (Proof.all_goals rv) (Proof.all_goals cp))
-            | None -> true
-        done;
-        !rv
+        let rec search did =
+          let did = fold_until back_tactic 1 did in
+          match get_proof ~doc did with
+          | None -> None
+          | Some rv ->
+            if Evar.Set.equal (Proof.all_goals rv) (Proof.all_goals cp)
+            then search did
+            else Some rv
+        in
+        search id
     with Not_found | PG_compat.NoCurrentProof -> None
 
 end (* }}} *)
@@ -2430,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
 
@@ -2474,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;