Add a Petanque TCP server

.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:

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
 -----------------------------

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 ]

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.
+```

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))

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

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 ()

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))