[petanque] Run_tac: check if proof are finished

petanque/agent.ml

@@ -47,6 +47,12 @@ module R = struct
   type 'a t = ('a, Error.t) Result.t
 end
 
+module Run_result = struct
+  type 'a t =
+    | Proof_finished of 'a
+    | Current_state of 'a
+end
+
 let init_coq ~debug =
   let load_module = Dynlink.loadfile in
   let load_plugin = Coq.Loader.plugin_handler None in
@@ -131,14 +137,22 @@ let parse ~loc tac st =
   let str = Coq.Parsing.Parsable.make ?loc str in
   Coq.Parsing.parse ~st str
 
+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 parse_and_execute_in ~token ~loc tac st =
   let open Coq.Protect.E.O in
   let* ast = parse ~token ~loc tac st in
   match ast with
-  | Some ast -> Fleche.Memo.Interp.eval ~token (st, ast)
-  (* On EOF we return the previous state, the command was the empty string or a
-     comment *)
-  | None -> Coq.Protect.E.ok st
+  | Some ast -> (
+    let open Coq.Protect.E.O in
+    let* st = Fleche.Memo.Interp.eval ~token (st, ast) in
+    let+ goals = Fleche.Info.Goals.goals ~token ~st in
+    match goals with
+    | None -> Run_result.Proof_finished st
+    | Some goals when proof_finished goals -> Run_result.Proof_finished st
+    | _ -> Run_result.Current_state st)
+  | None -> Coq.Protect.E.ok (Run_result.Current_state st)
 
 let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
   match r with
@@ -149,7 +163,7 @@ let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
     Error (Error.Anomaly (Pp.string_of_ppcmds msg))
   | { r = Completed (Ok r); feedback = _ } -> Ok r
 
-let run_tac ~token ~st ~tac : (Coq.State.t, Error.t) Result.t =
+let run_tac ~token ~st ~tac : (_ Run_result.t, Error.t) Result.t =
   (* Improve with thm? *)
   let loc = None in
   Coq.State.in_stateM ~token ~st ~f:(parse_and_execute_in ~token ~loc tac) st

petanque/agent.mli

@@ -37,6 +37,12 @@ module R : sig
   type 'a t = ('a, Error.t) Result.t
 end
 
+module Run_result : sig
+  type 'a t =
+    | Proof_finished of 'a
+    | Current_state of 'a
+end
+
 (** I/O handling, by default, print to stderr *)
 
 (** [trace header extra message] *)
@@ -61,7 +67,10 @@ val start :
 
 (** [run_tac ~token ~st ~tac] tries to run [tac] over state [st] *)
 val run_tac :
-  token:Coq.Limits.Token.t -> st:State.t -> tac:string -> State.t R.t
+     token:Coq.Limits.Token.t
+  -> st:State.t
+  -> tac:string
+  -> State.t Run_result.t R.t
 
 (** [goals ~token ~st] return the list of goals for a given [st] *)
 val goals :

petanque/json_shell/jAgent.ml

@@ -16,6 +16,10 @@ module Error = struct
   type t = [%import: Petanque.Agent.Error.t] [@@deriving yojson]
 end
 
+module Run_result = struct
+  type 'a t = [%import: 'a Petanque.Agent.Run_result.t] [@@deriving yojson]
+end
+
 module R = struct
   type 'a t = [%import: 'a Petanque.Agent.R.t] [@@deriving yojson]
 end

petanque/json_shell/protocol.ml

@@ -115,11 +115,11 @@ module RunTac = struct
   end
 
   module Response = struct
-    type t = State.t [@@deriving yojson]
+    type t = State.t Run_result.t [@@deriving yojson]
   end
 
   module Response_ = struct
-    type t = int [@@deriving yojson]
+    type t = int Run_result.t [@@deriving yojson]
   end
 
   let handler ~token { Params.st; tac } = Agent.run_tac ~token ~st ~tac

petanque/test/basic_api.ml

@@ -26,18 +26,26 @@ let start ~token =
   let* env = Agent.init ~token ~debug ~root in
   Agent.start ~token ~env ~uri ~thm:"rev_snoc_cons"
 
+let extract_st (st : _ Agent.Run_result.t) =
+  match st with
+  | Proof_finished st | Current_state st -> st
+
 let main () =
   let open Fleche.Compat.Result.O in
   let token = Coq.Limits.create_atomic () in
+  let r ~st ~tac =
+    let st = extract_st st in
+    Agent.run_tac ~token ~st ~tac
+  in
   let* st = start ~token in
   let* _premises = Agent.premises ~token ~st in
   let* st = Agent.run_tac ~token ~st ~tac:"induction l." in
-  let* st = Agent.run_tac ~token ~st ~tac:"-" in
-  let* st = Agent.run_tac ~token ~st ~tac:"reflexivity." in
-  let* st = Agent.run_tac ~token ~st ~tac:"-" in
-  let* st = Agent.run_tac ~token ~st ~tac:"now simpl; rewrite IHl." in
-  let* st = Agent.run_tac ~token ~st ~tac:"Qed." in
-  Agent.goals ~token ~st
+  let* st = r ~st ~tac:"-" in
+  let* st = r ~st ~tac:"reflexivity." in
+  let* st = r ~st ~tac:"-" in
+  let* st = r ~st ~tac:"now simpl; rewrite IHl." in
+  let* st = r ~st ~tac:"Qed." in
+  Agent.goals ~token ~st:(extract_st st)
 
 let check_no_goals = function
   | Error err ->

petanque/test/dune

@@ -11,3 +11,11 @@
  (enabled_if
   (<> %{os_type} "Win32"))
  (libraries petanque petanque_json lsp))
+
+(test
+ (name json_api_failure)
+ (modules json_api_failure)
+ (deps test.v %{bin:pet})
+ (enabled_if
+  (<> %{os_type} "Win32"))
+ (libraries petanque petanque_json lsp))

petanque/test/json_api.ml

@@ -13,6 +13,10 @@ let trace ?verbose:_ msg = msgs := Format.asprintf "[trace] %s" msg :: !msgs
 let message ~lvl:_ ~message = msgs := message :: !msgs
 let dump_msgs () = List.iter (Format.eprintf "%s@\n") (List.rev !msgs)
 
+let extract_st (st : Protocol.RunTac.Response_.t) =
+  match st with
+  | Proof_finished st | Current_state st -> st
+
 let run (ic, oc) =
   let open Fleche.Compat.Result.O in
   let debug = false in
@@ -22,18 +26,22 @@ let run (ic, oc) =
     let trace = trace
     let message = message
   end) in
+  let r ~st ~tac =
+    let st = extract_st st in
+    S.run_tac { st; tac }
+  in
   (* Will this work on Windows? *)
   let root, uri = prepare_paths () in
   let* env = S.init { debug; root } in
   let* st = S.start { env; uri; thm = "rev_snoc_cons" } in
   let* _premises = S.premises { st } in
   let* st = S.run_tac { st; tac = "induction l." } in
-  let* st = S.run_tac { st; tac = "-" } in
-  let* st = S.run_tac { st; tac = "reflexivity." } in
-  let* st = S.run_tac { st; tac = "-" } in
-  let* st = S.run_tac { st; tac = "now simpl; rewrite IHl." } in
-  let* st = S.run_tac { st; tac = "Qed." } in
-  S.goals { st }
+  let* st = r ~st ~tac:"-" in
+  let* st = r ~st ~tac:"reflexivity." in
+  let* st = r ~st ~tac:"-" in
+  let* st = r ~st ~tac:"now simpl; rewrite IHl." in
+  let* st = r ~st ~tac:"Qed." in
+  S.goals { st = extract_st st }
 
 let main () =
   let server_out, server_in = Unix.open_process "pet" in

petanque/test/json_api_failure.ml

@@ -0,0 +1,68 @@
+open Petanque_json
+
+let prepare_paths () =
+  let to_uri file =
+    Lang.LUri.of_string file |> Lang.LUri.File.of_uri |> Result.get_ok
+  in
+  let cwd = Sys.getcwd () in
+  let file = Filename.concat cwd "test.v" in
+  (to_uri cwd, to_uri file)
+
+let msgs = ref []
+let trace ?verbose:_ msg = msgs := Format.asprintf "[trace] %s" msg :: !msgs
+let message ~lvl:_ ~message = msgs := message :: !msgs
+let dump_msgs () = List.iter (Format.eprintf "%s@\n") (List.rev !msgs)
+
+let extract_st (st : Protocol.RunTac.Response_.t) =
+  match st with
+  | Proof_finished st | Current_state st -> st
+
+let run (ic, oc) =
+  let open Fleche.Compat.Result.O in
+  let debug = false in
+  let module S = Client.S (struct
+    let ic = ic
+    let oc = oc
+    let trace = trace
+    let message = message
+  end) in
+  let r ~st ~tac =
+    let st = extract_st st in
+    S.run_tac { st; tac }
+  in
+  (* Will this work on Windows? *)
+  let root, uri = prepare_paths () in
+  let* env = S.init { debug; root } in
+  let* st = S.start { env; uri; thm = "rev_snoc_cons" } in
+  let* _premises = S.premises { st } in
+  let* st = S.run_tac { st; tac = "induction l." } in
+  let* st = r ~st ~tac:"-" in
+  (* Introduce an error *)
+  (* let* st = r ~st ~tac:"reflexivity." in *)
+  let* st = r ~st ~tac:"-" in
+  let* st = r ~st ~tac:"now simpl; rewrite IHl." in
+  let* st = r ~st ~tac:"Qed." in
+  S.goals { st = extract_st st }
+
+let main () =
+  let server_out, server_in = Unix.open_process "pet" in
+  run (server_out, Format.formatter_of_out_channel server_in)
+
+let check_no_goals = function
+  | Error _err ->
+    (* errored as expected! *)
+    0
+  | Ok None ->
+    dump_msgs ();
+    Format.eprintf "error: we did succeded when we should not@\n%!";
+    1
+  | Ok (Some _goals) ->
+    dump_msgs ();
+    Format.eprintf "error: goals remaining@\n%!";
+    1
+
+let () =
+  let result = main () in
+  (* Need to kill the sever... *)
+  (* let () = Unix.kill server 9 in *)
+  check_no_goals result |> exit