[petanque] Split shell parts of petanque_json to petanque_shell

petanque/json/dune

@@ -0,0 +1,6 @@
+(library
+ (name petanque_json)
+ (public_name coq-lsp.petanque.json)
+ (preprocess
+  (staged_pps ppx_import ppx_deriving_yojson))
+ (libraries lsp petanque))

petanque/json_shell/client.ml

@@ -1,3 +1,5 @@
+open Petanque_json
+
 (* Client wrap *)
 module type Chans = sig
   val ic : in_channel

petanque/json_shell/client.mli

@@ -1,3 +1,5 @@
+open Petanque_json
+
 module type Chans = sig
   val ic : in_channel
   val oc : Format.formatter

petanque/json_shell/dune

@@ -1,20 +1,20 @@
 (library
- (name petanque_json)
- (public_name coq-lsp.petanque.json)
+ (name petanque_shell)
+ (public_name coq-lsp.petanque.json_shell)
  (modules :standard \ pet server)
  (preprocess
   (staged_pps ppx_import ppx_deriving_yojson))
- (libraries lsp petanque))
+ (libraries lsp petanque petanque_json))
 
 (executable
  (name pet)
  (public_name pet)
  (modules pet)
- (libraries petanque_json))
+ (libraries petanque_shell))
 
 (executable
  (name server)
  (public_name pet-server)
  (modules server)
  (optional)
- (libraries logs.lwt lwt.unix petanque_json))
+ (libraries logs.lwt lwt.unix petanque_shell))

petanque/json_shell/interp_shell.ml

@@ -4,7 +4,7 @@
 (* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
 (************************************************************************)
 
-open Interp
+open Petanque_json.Interp
 open Protocol_shell
 
 let do_handle ~fn ~token action =

petanque/json_shell/pet.ml

@@ -1,5 +1,5 @@
 (* json rpc server *)
-open Petanque_json
+open Petanque_shell
 
 let use_http_headers = ref true
 
@@ -28,7 +28,7 @@ let send_message msg =
 (* Format.fprintf Format.std_formatter "@[%a@]@\n%!" Yojson.Safe.pretty_print
    msg *)
 
-let fn = Petanque.Shell.build_doc
+let fn = Shell.build_doc
 
 let interp ~token request =
   match Interp_shell.interp ~fn ~token request with
@@ -64,10 +64,10 @@ let log_error err =
 let pet_main debug roots http_headers =
   Coq.Limits.start ();
   if trace_enabled then (
-    Petanque.Shell.trace_ref := trace_notification;
-    Petanque.Shell.message_ref := message_notification);
+    Shell.trace_ref := trace_notification;
+    Shell.message_ref := message_notification);
   let token = Coq.Limits.Token.create () in
-  Result.iter_error log_error (Petanque.Shell.init_agent ~token ~debug ~roots);
+  Result.iter_error log_error (Shell.init_agent ~token ~debug ~roots);
   use_http_headers := http_headers;
   loop ~token
 

petanque/json_shell/protocol_shell.ml

@@ -1,3 +1,5 @@
+open Petanque_json
+
 (* set_workspace RPC *)
 module SetWorkspace = struct
   let method_ = "petanque/setWorkspace"
@@ -24,6 +26,6 @@ module SetWorkspace = struct
     let handler =
       Protocol.HType.Immediate
         (fun ~token { Params.debug; root } ->
-          Petanque.Shell.set_workspace ~token ~debug ~root)
+          Shell.set_workspace ~token ~debug ~root)
   end
 end

petanque/json_shell/server.ml

@@ -1,6 +1,6 @@
 open Lwt
 open Lwt.Syntax
-open Petanque_json
+open Petanque_shell
 
 let rq_info (r : Lsp.Base.Message.t) =
   match r with
@@ -9,7 +9,7 @@ let rq_info (r : Lsp.Base.Message.t) =
   | Response (Ok { id; _ } | Error { id; _ }) ->
     Format.asprintf "response for: %d" id
 
-let fn = Petanque.Shell.build_doc
+let fn = Shell.build_doc
 
 let rec handle_connection ~token ic oc () =
   try
@@ -76,7 +76,7 @@ let pet_main debug roots address port backlog =
   (* EJGA: pet-server should handle this at some point *)
   (* Petanque.Shell.trace_ref := trace_notification; *)
   (* Petanque.Shell.message_ref := message_notification); *)
-  Result.iter_error log_error (Petanque.Shell.init_agent ~token ~debug ~roots);
+  Result.iter_error log_error (Shell.init_agent ~token ~debug ~roots);
   Lwt_main.run @@ serve ()
 
 open Cmdliner

petanque/shell.ml → petanque/json_shell/shell.ml

@@ -19,7 +19,7 @@ let setup_workspace ~token ~init ~debug ~root =
    let+ workspace = Coq.Workspace.guess ~token ~debug ~cmdline ~dir in
    let files = Coq.Files.make () in
    Fleche.Doc.Env.make ~init ~workspace ~files)
-  |> Result.map_error Agent.Error.coq
+  |> Result.map_error Petanque.Agent.Error.coq
 
 let trace_stderr hdr ?extra:_ msg =
   Format.eprintf "@[[trace] %s | %s @]@\n%!" hdr msg
@@ -68,7 +68,7 @@ let print_diags (doc : Fleche.Doc.t) =
 let read_raw ~uri =
   let file = Lang.LUri.File.to_string_file uri in
   try Ok Coq.Compat.Ocaml_414.In_channel.(with_open_text file input_all)
-  with Sys_error err -> Error (Agent.Error.system err)
+  with Sys_error err -> Error (Petanque.Agent.Error.system err)
 
 let setup_doc ~token env uri contents =
   let contents =
@@ -90,7 +90,7 @@ let build_doc ~token ~uri ~contents =
 (* Flèche LSP backend handles the conversion at the protocol level *)
 let to_uri uri =
   Lang.LUri.of_string uri |> Lang.LUri.File.of_uri
-  |> Result.map_error Agent.Error.system
+  |> Result.map_error Petanque.Agent.Error.system
 
 let uri_of_path path = Format.asprintf "file:///%s" path |> to_uri
 

petanque/shell.mli → petanque/json_shell/shell.mli

@@ -1,3 +1,5 @@
+open Petanque
+
 (** I/O handling, by default, print to stderr *)
 
 (** [trace header extra message] *)

petanque/test/basic_api.ml

@@ -1,4 +1,5 @@
 open Petanque
+open Petanque_shell
 
 let prepare_paths () =
   let to_uri file =
@@ -18,18 +19,18 @@ let dump_msgs () = List.iter (Format.eprintf "%s@\n") (List.rev !msgs)
 
 let start ~token =
   let debug = false in
-  Petanque.Shell.trace_ref := trace;
-  Petanque.Shell.message_ref := message;
+  Shell.trace_ref := trace;
+  Shell.message_ref := message;
   (* Will this work on Windows? *)
   let open Coq.Compat.Result.O in
-  let _ : _ Result.t = Petanque.Shell.init_agent ~token ~debug ~roots:[] in
+  let _ : _ Result.t = Shell.init_agent ~token ~debug ~roots:[] in
   (* Twice to test for #766 *)
   let root, uri = prepare_paths () in
-  let* () = Petanque.Shell.set_workspace ~token ~debug ~root in
-  let* () = Petanque.Shell.set_workspace ~token ~debug ~root in
+  let* () = Shell.set_workspace ~token ~debug ~root in
+  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 = Petanque.Shell.build_doc ~token ~uri ~contents:None in
+  let* doc = Shell.build_doc ~token ~uri ~contents:None in
   Agent.start ~token ~doc ~thm:"rev_snoc_cons" ()
 
 let extract_st { Agent.Run_result.st; _ } = st

petanque/test/dune

@@ -2,20 +2,20 @@
  (name basic_api)
  (modules basic_api)
  (deps test.v)
- (libraries petanque))
+ (libraries petanque_shell))
 
 (test
  (name json_api)
  (modules json_api)
  (deps test.v %{bin:pet})
  (enabled_if
   (<> %{os_type} "Win32"))
- (libraries petanque petanque_json lsp))
+ (libraries petanque petanque_shell 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))
+ (libraries petanque petanque_shell lsp))

petanque/test/json_api.ml

@@ -1,4 +1,5 @@
 open Petanque_json
+open Petanque_shell
 
 let prepare_paths () =
   let to_uri file =

petanque/test/json_api_failure.ml

@@ -1,4 +1,5 @@
 open Petanque_json
+open Petanque_shell
 
 let prepare_paths () =
   let to_uri file =