diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index eca26478..9a0d4732 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -104,6 +104,7 @@ jobs: - name: Install Coq and SerAPI into OPAM switch run: | + opam install lwt logs # Also build pet-server opam install memprof-limits # We need to do this to avoid coq-lsp rebuilding Coq below due to deptops opam install vendor/coq/{coq-core,coq-stdlib,coqide-server,coq}.opam opam install vendor/coq-serapi/coq-serapi.opam @@ -114,6 +115,9 @@ jobs: - name: Test `coq-lsp` in installed switch run: opam exec -- fcc examples/Demo.v + - name: Test `pet-server` is built + run: opam exec -- which pet-server + build-nix: name: Nix strategy: diff --git a/CHANGES.md b/CHANGES.md index f00ef9c4..427075ba 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -124,9 +124,12 @@ - [Coq API] Add functions to retrieve list of declarations done in .vo files (@ejallego, @eytans, #704) - New `petanque` API to interact directly with Coq's proof - engine. (@ejgallego, @gbdrt, #703, thanks to Alex Sanchez-Stern) + engine. (@ejgallego, @gbdrt, Laetitia Teodorescu #703, thanks to + Alex Sanchez-Stern for many insightful feedback and testing) - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI to perform proof search and more (@ejgallego, @gbdrt, #705) + - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt, + #697) - Always dispose UI elements. This should improve some strange behaviors on extension restart (@ejgallego, #708) - Support Coq meta-commands (Reset, Reset Initial, Back) They are @@ -162,6 +165,9 @@ (@ejgallego, #727) - Don't expand bullet goals at previous levels by default (@ejgallego, @Alizter, # cc #525) + - [petanque] Return basic goal information after `run_tac`, so we + avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego, + #733) # coq-lsp 0.1.8.1: Spring fix ----------------------------- diff --git a/coq-lsp.opam b/coq-lsp.opam index 7286614d..78149826 100644 --- a/coq-lsp.opam +++ b/coq-lsp.opam @@ -54,6 +54,8 @@ depends: [ "ppx_hash" { >= "v0.13.0" & < "v0.17" } ] +depopts: ["lwt" "logs"] + build: [ [ "rm" "-rf" "vendor" ] [ "dune" "build" "-p" name "-j" jobs ] diff --git a/petanque/README.md b/petanque/README.md index 3ea91397..a7a85a6c 100644 --- a/petanque/README.md +++ b/petanque/README.md @@ -33,7 +33,7 @@ have three options: See the contributing guide for instructions on how to perform the last two. -## Using `petanque` +## Running `petanque` JSON shell You can use `petanque` in 2 different ways: @@ -84,3 +84,47 @@ Please use one line per json input. json input examples are: Seems to work! (TM) (Famous last words) +## Running `pet-server` + +After building Petanque, you can launch a TCP server with: +``` +dune exec -- pet-server +``` + +Default address is 127.0.0.1 and default port is 8765. + +``` +❯ dune exec -- pet-server --help +PET(1) Pet Manual PET(1) + +NAME + pet - Petanque Server + +SYNOPSIS + pet [--address=ADDRESS] [--backlog=BACKLOG] [--port=PORT] [OPTION]… + +DESCRIPTION + Launch a petanque server to interact with Coq + +USAGE + See the documentation on the project's webpage for more information + +OPTIONS + -a ADDRESS, --address=ADDRESS (absent=127.0.0.1) + address to listen to + + -b BACKLOG, --backlog=BACKLOG (absent=10) + socket backlog + + -p PORT, --port=PORT (absent=8765) + port to listen to + +COMMON OPTIONS + --help[=FMT] (default=auto) + Show this help in format FMT. The value FMT must be one of auto, + pager, groff or plain. With auto, the format is pager or plain + whenever the TERM env var is dumb or undefined. + + --version + Show version information. +``` diff --git a/petanque/json_shell/dune b/petanque/json_shell/dune index 97f28324..bd19ff96 100644 --- a/petanque/json_shell/dune +++ b/petanque/json_shell/dune @@ -1,7 +1,7 @@ (library (name petanque_json) (public_name coq-lsp.petanque.json) - (modules :standard \ pet) + (modules :standard \ pet server) (preprocess (staged_pps ppx_import ppx_deriving_yojson)) (libraries cmdliner lsp petanque)) @@ -11,3 +11,10 @@ (public_name pet) (modules pet) (libraries petanque_json)) + +(executable + (name server) + (public_name pet-server) + (modules server) + (optional) + (libraries logs.lwt lwt.unix petanque_json)) diff --git a/petanque/json_shell/pet.ml b/petanque/json_shell/pet.ml index 58d944b6..2b390fe4 100644 --- a/petanque/json_shell/pet.ml +++ b/petanque/json_shell/pet.ml @@ -40,11 +40,6 @@ let message_notification ~lvl ~message = in Lsp.Io.send_json Format.std_formatter notification -(* XXX: Flèche LSP backend already handles the conversion at the protocol - level *) -let uri_of_string_exn uri = - Lang.LUri.of_string uri |> Lang.LUri.File.of_uri |> Result.get_ok - let trace_enabled = true let pet_main debug roots = @@ -54,19 +49,7 @@ let pet_main debug roots = Petanque.Agent.trace_ref := trace_notification; Petanque.Agent.message_ref := message_notification); let token = Coq.Limits.Token.create () in - let () = - match roots with - | [] -> () - | [ root ] | root :: _ -> ( - let root = uri_of_string_exn root in - match Petanque.Agent.init ~token ~debug ~root with - | Ok env -> - (* hack until we fix the stuff *) - let _ : Yojson.Safe.t = JAgent.Env.to_yojson env in - () - | Error err -> - Format.eprintf "Error: %s@\n%!" (Petanque.Agent.Error.to_string err)) - in + let () = Utils.set_roots ~token ~debug ~roots in loop ~token open Cmdliner diff --git a/petanque/json_shell/server.ml b/petanque/json_shell/server.ml new file mode 100644 index 00000000..1e536945 --- /dev/null +++ b/petanque/json_shell/server.ml @@ -0,0 +1,109 @@ +open Lwt +open Lwt.Syntax +open Petanque_json + +let rq_info (r : Lsp.Base.Message.t) = + match r with + | Notification { method_; _ } -> Format.asprintf "notification: %s" method_ + | Request { method_; _ } -> Format.asprintf "request: %s" method_ + | Response (Ok { id; _ } | Error { id; _ }) -> + Format.asprintf "response for: %d" id + +let rec handle_connection ~token ic oc () = + try + let* request = Lwt_io.read_line ic in + let request = Yojson.Safe.from_string request in + match Lsp.Base.Message.of_yojson request with + | Error err -> + (* error in Json message *) + let* () = Logs_lwt.info (fun m -> m "Error: %s" err) in + handle_connection ~token ic oc () + | Ok request -> ( + (* everything is fine up to JSON-RPC level *) + let* () = Logs_lwt.info (fun m -> m "Received: %s" (rq_info request)) in + (* request could be a notification, so maybe we don't have to do a + reply! *) + match Interp.interp ~token request with + | None -> handle_connection ~token ic oc () + | Some reply -> + let* () = Logs_lwt.info (fun m -> m "Sent reply") in + let* () = Lwt_io.fprintl oc (Yojson.Safe.to_string reply) in + handle_connection ~token ic oc ()) + with End_of_file -> return () + +let accept_connection ~token conn = + let fd, _ = conn in + let ic = Lwt_io.of_fd ~mode:Lwt_io.Input fd in + let oc = Lwt_io.of_fd ~mode:Lwt_io.Output fd in + let* () = Logs_lwt.info (fun m -> m "New connection") in + Lwt.on_failure (handle_connection ~token ic oc ()) (fun e -> + Logs.err (fun m -> m "%s" (Printexc.to_string e))); + return () + +let create_socket ~address ~port ~backlog = + let open Lwt_unix in + let sock = socket PF_INET SOCK_STREAM 0 in + ( bind sock @@ ADDR_INET (Unix.inet_addr_of_string address, port) |> fun x -> + ignore x ); + listen sock backlog; + sock + +let create_server ~token sock = + let rec serve () = + let* conn = Lwt_unix.accept sock in + let* () = accept_connection ~token conn in + serve () + in + serve + +let pet_main debug roots address port backlog = + Coq.Limits.start (); + let token = Coq.Limits.Token.create () in + let () = Logs.set_reporter (Logs.format_reporter ()) in + let () = Logs.set_level (Some Logs.Info) in + let sock = create_socket ~address ~port ~backlog in + let serve = create_server ~token sock in + let () = Utils.set_roots ~token ~debug ~roots in + Lwt_main.run @@ serve () + +open Cmdliner + +let address = + let doc = "address to listen to" in + Arg.( + value & opt string "127.0.0.1" + & info [ "a"; "address" ] ~docv:"ADDRESS" ~doc) + +let port = + let doc = "port to listen to" in + Arg.(value & opt int 8765 & info [ "p"; "port" ] ~docv:"PORT" ~doc) + +let backlog = + let doc = "socket backlog" in + Arg.(value & opt int 10 & info [ "b"; "backlog" ] ~docv:"BACKLOG" ~doc) + +let pet_cmd : unit Cmd.t = + let doc = "Petanque Server" in + let man = + [ `S "DESCRIPTION" + ; `P "Launch a petanque server to interact with Coq" + ; `S "USAGE" + ; `P + "See\n\ + \ the\n\ + \ documentation on the project's webpage for more information" + ] + in + let version = Fleche.Version.server in + let pet_term = + Term.( + const pet_main $ Coq.Args.debug $ Coq.Args.roots $ address $ port + $ backlog) + in + Cmd.(v (Cmd.info "pet" ~version ~doc ~man) pet_term) + +let main () = + let ecode = Cmd.eval pet_cmd in + exit ecode + +let () = main () diff --git a/petanque/json_shell/utils.ml b/petanque/json_shell/utils.ml new file mode 100644 index 00000000..84ebf089 --- /dev/null +++ b/petanque/json_shell/utils.ml @@ -0,0 +1,17 @@ +(* XXX: Flèche LSP backend already handles the conversion at the protocol + level *) +let uri_of_string_exn uri = + Lang.LUri.of_string uri |> Lang.LUri.File.of_uri |> Result.get_ok + +let set_roots ~token ~debug ~roots = + match roots with + | [] -> () + | [ root ] | root :: _ -> ( + let root = uri_of_string_exn root in + match Petanque.Agent.init ~token ~debug ~root with + | Ok env -> + (* hack until we fix the stuff *) + let _ : Yojson.Safe.t = JAgent.Env.to_yojson env in + () + | Error err -> + Format.eprintf "Error: %s@\n%!" (Petanque.Agent.Error.to_string err))