Merge pull request #847 from ejgallego/fix_stack_petanque

[petanque] Fix bug for detection of proof finished in deep stacks

CHANGES.md

@@ -38,6 +38,8 @@
    extra data from list to named record (@ejgallego, #843)
  - [lsp] Implement support for `textDocument/codeAction`. For now, we
    support Coq's 8.21 `quickFix` data (@ejgallego, #840, #843, #845)
+ - [petanque] Fix bug for detection of proof finished in deep stacks
+   (@ejgallego, @gbdrt, #847)
 
 # coq-lsp 0.2.0: From Green to Blue
 -----------------------------------

petanque/agent.ml

@@ -144,7 +144,10 @@ let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
   | { r = Completed (Ok r); feedback = _ } -> Ok r
 
 let proof_finished { Coq.Goals.goals; stack; shelf; given_up; _ } =
-  List.for_all CList.is_empty [ goals; shelf; given_up ] && CList.is_empty stack
+  let check_stack stack =
+    CList.(for_all (fun (l, r) -> is_empty l && is_empty r)) stack
+  in
+  List.for_all CList.is_empty [ goals; shelf; given_up ] && check_stack stack
 
 (* At some point we want to return both hashes *)
 module Hash_kind = struct

petanque/test/basic_api.ml

@@ -17,7 +17,7 @@ let trace hdr ?extra:_ msg =
 let message ~lvl:_ ~message = msgs := message :: !msgs
 let dump_msgs () = List.iter (Format.eprintf "%s@\n") (List.rev !msgs)
 
-let start ~token =
+let init ~token =
   let debug = false in
   Shell.trace_ref := trace;
   Shell.message_ref := message;
@@ -30,19 +30,17 @@ let start ~token =
   let* () = Shell.set_workspace ~token ~debug ~root in
   (* Careful to call [build_doc] before we have set an environment! [pet] and
      [pet-server] are careful to always set a default one *)
-  let* doc = Shell.build_doc ~token ~uri in
-  Agent.start ~token ~doc ~thm:"rev_snoc_cons" ()
+  Shell.build_doc ~token ~uri
 
 let extract_st { Agent.Run_result.st; _ } = st
 
-let main () =
+let snoc_test ~token ~doc =
   let open Coq.Compat.Result.O in
-  let token = Coq.Limits.create_atomic () in
   let r ~st ~tac =
     let st = extract_st st in
     Agent.run ~token ~st ~tac ()
   in
-  let* { st; _ } = start ~token in
+  let* { st; _ } = Agent.start ~token ~doc ~thm:"rev_snoc_cons" () in
   let* _premises = Agent.premises ~token ~st in
   let* st = Agent.run ~token ~st ~tac:"induction l." () in
   let h1 = Agent.State.hash st.st in
@@ -58,6 +56,34 @@ let main () =
   let* st = r ~st ~tac:"Qed." in
   Agent.goals ~token ~st:(extract_st st)
 
+let finished_stack ~token ~doc =
+  let open Coq.Compat.Result.O in
+  let r ~st ~tac =
+    let st = extract_st st in
+    Agent.run ~token ~st ~tac ()
+  in
+  let* { st; _ } = Agent.start ~token ~doc ~thm:"deepBullet" () in
+  let* st = Agent.run ~token ~st ~tac:"split." () in
+  let* st = r ~st ~tac:"-" in
+  let* st = r ~st ~tac:"now reflexivity." in
+  let* st = r ~st ~tac:"-" in
+  let* st = r ~st ~tac:"split." in
+  let* st = r ~st ~tac:"+" in
+  let* st = r ~st ~tac:"now reflexivity." in
+  let* st = r ~st ~tac:"+" in
+  let* { st; proof_finished; _ } = r ~st ~tac:"now reflexivity." in
+  (* Check that we properly detect no goals with deep stacks. *)
+  assert proof_finished;
+  let* st = Agent.run ~token ~st ~tac:"Qed." () in
+  Agent.goals ~token ~st:(extract_st st)
+
+let main () =
+  let open Coq.Compat.Result.O in
+  let token = Coq.Limits.create_atomic () in
+  let* doc = init ~token in
+  let* _goals = snoc_test ~token ~doc in
+  finished_stack ~token ~doc
+
 let check_no_goals = function
   | Error err ->
     Format.eprintf "error: in execution: %s@\n%!" (Agent.Error.to_string err);

petanque/test/test.v

@@ -8,3 +8,13 @@ Proof.
   - reflexivity.
   - simpl. rewrite IHl. simpl. reflexivity.
 Qed.
+
+(* This is for testing proof finished *)
+Lemma deepBullet : (1 = 1) /\ (21 = 21 /\ 22 = 22).
+Proof.
+split.
+- now reflexivity.
+- split.
+  + now reflexivity.
+  + now reflexivity.
+Qed.