[petanque] Initial commit, as an OCaml library

CHANGES.md

@@ -119,6 +119,8 @@
    Implement `workspace/didChangeConfiguration` (@ejgallego, #702)
  - [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)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

CONTRIBUTING.md

@@ -3,17 +3,23 @@ Contributing to Coq LSP
 
 Thank you very much for willing to contribute to coq-lsp!
 
-`coq-lsp` has two components:
+The `coq-lsp` repository contains several tightly coupled components
+in a single repository, also known as a monorepo, in particular:
 
-- a LSP server for Coq project written in OCaml.
-- a `coq-lsp` VS Code extension written in TypeScript and React, in
-  the `editor/code` directory.
+- Flèche: an incremental document engine for Coq supporting literate
+  programming and programability, written in OCaml
+- `fcc`: an extensible command line compiler built on top of Flèche
+- `petanque`: direct access to Coq's proof engine
+- `coq-lsp`a LSP server for the Coq project, written in OCaml on top of Flèche
+- a `coq-lsp/VSCode` extension written in TypeScript and React, in
+  the `editor/code` directory
 
-Read coq-lsp [FAQ](etc/FAQ.md) for an explanation on what the above mean.
+Read coq-lsp [FAQ](etc/FAQ.md) to learn more about LSP and
+server/client roles.
 
-It is possible to hack only in the server, on the client, or on both at the same
-time. We have thus structured this guide in 3 sections: general guidelines,
-server, and VS Code client.
+It is possible to hack only in the server, on the client, or on both
+at the same time. We have thus structured this guide in 3 sections:
+general guidelines, server, and VS Code client.
 
 ## General guidelines
 
@@ -184,14 +190,17 @@ coq-lsp.packages.${system}.default
 
 The `coq-lsp` server consists of several components, we present them bottom-up
 
+- `vendor/coq`: [vendored] Coq version to build coq-lsp against
 - `vendor/coq-serapi`: [vendored] improved utility functions to handle Coq AST
 - `coq`: Utility library / abstracted Coq API. This is the main entry point for
   communication with Coq, and it reifies Coq calls as to present a purely
   functional interface to Coq.
+- `lang`: base language definitions for Flèche
 - `fleche`: incremental document processing backend. Exposes a generic API, but
   closely modelled to match LSP
 - `lsp`: small generic LSP utilities, at some point to be replaced by a generic
   library
+- `petanque`: low-level access to Coq's API
 - `controller`: LSP controller, a thin layer translating LSP transport layer to
   `flèche` surface API, plus some custom event queues for Coq.
 - `controller-js`: LSP controller for Javascript, used for `vscode.dev` and

README.md

@@ -182,6 +182,12 @@ fully-fledged LSP client.
 add your pre/post processing passes, for example to analyze or serialize parts
 of Coq files.
 
+### 🪄 Advanced APIs for Coq Interaction
+
+Thanks to Flèche, we provide some APIs on top of it that allow advanced use
+cases with Coq. In particular, we provide direct, low-overhead access to Coq's
+proof engine using [petanque](./petanque).
+
 ### ♻️ Reusability, Standards, Modularity
 
 The incremental document checking library of `coq-lsp` has been designed to be

compiler/compile.ml

@@ -22,7 +22,7 @@ let save_diags_file ~(doc : Fleche.Doc.t) =
   let file = Lang.LUri.File.to_string_file doc.uri in
   let file = Filename.remove_extension file ^ ".diags" in
   let diags = Fleche.Doc.diags doc in
-  Util.format_to_file ~file ~f:Output.pp_diags diags
+  Fleche.Compat.format_to_file ~file ~f:Output.pp_diags diags
 
 (** Return: exit status for file:
 
@@ -47,7 +47,9 @@ let compile_file ~cc file : int =
     let workspace = workspace_of_uri ~io ~workspaces ~uri ~default in
     let files = Coq.Files.make () in
     let env = Doc.Env.make ~init:root_state ~workspace ~files in
-    let raw = Util.input_all file in
+    let raw =
+      Fleche.Compat.Ocaml_414.In_channel.(with_open_bin file input_all)
+    in
     let () = Theory.create ~io ~token ~env ~uri ~raw ~version:1 in
     match Theory.Check.maybe_check ~io ~token with
     | None -> 102

coq/goals.ml

@@ -50,9 +50,10 @@ type ('a, 'pp) goals =
   ; given_up : 'a list
   }
 
-let map_goals ~f { goals; stack; bullet; shelf; given_up } =
+let map_goals ~f ~g { goals; stack; bullet; shelf; given_up } =
   let goals = List.map f goals in
   let stack = List.map (fun (s, r) -> (List.map f s, List.map f r)) stack in
+  let bullet = Option.map g bullet in
   let shelf = List.map f shelf in
   let given_up = List.map f given_up in
   { goals; stack; bullet; shelf; given_up }

coq/goals.mli

@@ -42,7 +42,8 @@ type ('a, 'pp) goals =
   ; given_up : 'a list
   }
 
-val map_goals : f:('a -> 'b) -> ('a, 'pp) goals -> ('b, 'pp) goals
+val map_goals :
+  f:('a -> 'b) -> g:('pp -> 'pp') -> ('a, 'pp) goals -> ('b, 'pp') goals
 
 type 'pp reified_pp = ('pp reified_goal, 'pp) goals
 

coq/library_file.ml

@@ -109,3 +109,5 @@ let toc dps : _ list =
   in
   let () = Declaremods.iter_all_interp_segments obj_action in
   List.rev !res
+
+let toc ~token ~st dps = State.in_state ~token ~st ~f:toc dps

coq/library_file.mli

@@ -20,7 +20,11 @@ val name : t -> Names.DirPath.t
 
     There have been several upstream Coq PRs trying to improve this situation,
     but so far they didn't make enough progress. *)
-val toc : t list -> (string * Constr.t) list
+val toc :
+     token:Limits.Token.t
+  -> st:State.t
+  -> t list
+  -> ((string * Constr.t) list, Loc.t) Protect.E.t
 
 (** Recovers the list of loaded libraries for state [st] *)
 val loaded : token:Limits.Token.t -> st:State.t -> (t list, Loc.t) Protect.E.t

compiler/util.ml → fleche/compat.ml

@@ -1,3 +1,5 @@
+(* Compatibility file *)
+
 module Ocaml_414 = struct
   module In_channel = struct
     (* 4.14 can do this: In_channel.with_open_bin file In_channel.input_all, so
@@ -8,6 +10,7 @@ module Ocaml_414 = struct
       Fun.protect ~finally:(fun () -> Stdlib.close_in_noerr ic) (fun () -> f ic)
 
     let with_open_bin s f = with_open Stdlib.open_in_bin s f
+    let with_open_text s f = with_open Stdlib.open_in s f
 
     (* Read up to [len] bytes into [buf], starting at [ofs]. Return total bytes
        read. *)
@@ -95,9 +98,14 @@ module Ocaml_414 = struct
   end
 end
 
-let input_all file =
-  let open Ocaml_414 in
-  In_channel.with_open_bin file In_channel.input_all
+module Result = struct
+  include Result
+
+  module O = struct
+    let ( let+ ) r f = map f r
+    let ( let* ) r f = bind r f
+  end
+end
 
 let format_to_file ~file ~f x =
   let open Ocaml_414 in

fleche/compat.mli

@@ -0,0 +1,28 @@
+(* Compatiblity and general utils *)
+
+(* We should at some point remove all of this file in favor of a standard
+   library that suits our needs *)
+module Ocaml_414 : sig
+  module In_channel : sig
+    val with_open_bin : string -> (in_channel -> 'a) -> 'a
+    val with_open_text : string -> (in_channel -> 'a) -> 'a
+    val input_all : in_channel -> string
+  end
+
+  module Out_channel : sig
+    val with_open : ('a -> out_channel) -> 'a -> (out_channel -> 'b) -> 'b
+    val with_open_bin : string -> (out_channel -> 'a) -> 'a
+  end
+end
+
+val format_to_file :
+  file:string -> f:(Format.formatter -> 'a -> unit) -> 'a -> unit
+
+module Result : sig
+  include module type of Result
+
+  module O : sig
+    val ( let+ ) : ('a, 'l) t -> ('a -> 'b) -> ('b, 'l) t
+    val ( let* ) : ('a, 'l) t -> ('a -> ('b, 'l) t) -> ('b, 'l) t
+  end
+end

petanque/README.md

@@ -0,0 +1,39 @@
+_Petanque_ (pronounced "petanque") is a
+[gymnasium](https://gymnasium.farama.org/)-like environment for the
+Coq Proof Assistant.
+
+_Petanque_ is geared towards use cases where interacting at the
+document-level (like Flèche provides) in not enough, usually because
+we want to work on purely proof-search level vs the document level
+one.
+
+Petanque follows the methodology developed in SerAPI, thus we specify
+an OCaml API (`agent.mli`) which is then exposed via some form of RPC.
+
+## Authors
+
+- Guilaume Baudart (Inria)
+- Emilio J. Gallego Arias (Inria)
+- Laetitia Teodorescu (Inria)
+
+## Acknowledgments
+
+- Andrei Kozyrev
+- Alex Sánchez-Stern
+
+## Install instructions
+
+Please see the regular `coq-lsp` install instructions. In general you
+have three options:
+
+- use a released version from Opam
+- use a development version directly from the tree
+- install a development version using Opam
+
+See the contributing guide for instructions on how to perform the last
+two.
+
+## Using `petanque`
+
+To use `petanque`, you need to some form of shell, or you can just
+call the API directly from your OCaml program.