From cf67e9ec4ec6db8a6b3199310e166a7d20f0b4e9 Mon Sep 17 00:00:00 2001 From: Guillaume Baudart Date: Mon, 13 May 2024 14:52:46 +0200 Subject: [PATCH] [petanque] Run_tac: check if proof are finished --- petanque/agent.ml | 24 ++++++++--- petanque/agent.mli | 11 ++++- petanque/json_shell/jAgent.ml | 4 ++ petanque/json_shell/protocol.ml | 4 +- petanque/test/basic_api.ml | 20 ++++++--- petanque/test/dune | 8 ++++ petanque/test/json_api.ml | 20 ++++++--- petanque/test/json_api_failure.ml | 68 +++++++++++++++++++++++++++++++ 8 files changed, 139 insertions(+), 20 deletions(-) create mode 100644 petanque/test/json_api_failure.ml diff --git a/petanque/agent.ml b/petanque/agent.ml index 6648d412..2fba9fb6 100644 --- a/petanque/agent.ml +++ b/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 diff --git a/petanque/agent.mli b/petanque/agent.mli index 8f1a0cb1..7e4782e8 100644 --- a/petanque/agent.mli +++ b/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 : diff --git a/petanque/json_shell/jAgent.ml b/petanque/json_shell/jAgent.ml index 8f6f1a6a..d7d21c65 100644 --- a/petanque/json_shell/jAgent.ml +++ b/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 diff --git a/petanque/json_shell/protocol.ml b/petanque/json_shell/protocol.ml index 546a3eaa..9d138582 100644 --- a/petanque/json_shell/protocol.ml +++ b/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 diff --git a/petanque/test/basic_api.ml b/petanque/test/basic_api.ml index e8360520..9b5ed231 100644 --- a/petanque/test/basic_api.ml +++ b/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 -> diff --git a/petanque/test/dune b/petanque/test/dune index 4186be83..fe4c7a8e 100644 --- a/petanque/test/dune +++ b/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)) diff --git a/petanque/test/json_api.ml b/petanque/test/json_api.ml index bb6ef535..446f5c16 100644 --- a/petanque/test/json_api.ml +++ b/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 diff --git a/petanque/test/json_api_failure.ml b/petanque/test/json_api_failure.ml new file mode 100644 index 00000000..c709b342 --- /dev/null +++ b/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