[petanque] Initial commit, as an OCaml library

CHANGES.md

@@ -117,6 +117,8 @@
    #689)
  - Update server settings on the fly when tweaking them in VSCode.
    Implement `workspace/didChangeConfiguration` (@ejgallego, #702)
+ - 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 monorepos, 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
 

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
@@ -95,10 +97,6 @@ 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
-
 let format_to_file ~file ~f x =
   let open Ocaml_414 in
   Out_channel.with_open_bin file (fun oc ->

fleche/compat.mli

@@ -0,0 +1,18 @@
+(* 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 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

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.

petanque/agent.ml

@@ -0,0 +1,152 @@
+(************************************************************************)
+(* Flèche => RL agent: petanque                                         *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias & coq-lsp contributors           *)
+(************************************************************************)
+
+let pet_debug = false
+
+module State = struct
+  type t = Coq.State.t
+
+  let hash = Coq.State.hash
+  let equal = Coq.State.equal
+end
+
+module Env = struct
+  type t = Fleche.Doc.Env.t
+end
+
+(** Init errors *)
+module Init_error = struct
+  type t = string
+end
+
+module Run_error = struct
+  type t =
+    | Interrupted
+    | Parsing of string
+    | Coq of string
+    | Anomaly of string
+end
+
+module Start_error = struct
+  type t =
+    | Run of Run_error.t
+    | Theorem_not_found of string
+end
+
+let init_coq ~debug =
+  let load_module = Dynlink.loadfile in
+  let load_plugin = Coq.Loader.plugin_handler None in
+  Coq.Init.(coq_init { debug; load_module; load_plugin })
+
+let cmdline : Coq.Workspace.CmdLine.t =
+  { coqlib = Coq_config.coqlib
+  ; coqcorelib = Filename.concat Coq_config.coqlib "../coq-core"
+  ; ocamlpath = None
+  ; vo_load_path = []
+  ; ml_include_path = []
+  ; args = []
+  ; require_libraries = []
+  }
+
+let io =
+  let trace hdr ?extra:_ msg =
+    Format.eprintf "@[[trace] %s | %s @]@\n%!" hdr msg
+  in
+  let message ~lvl:_ ~message =
+    Format.eprintf "@[[message] %s @]@\n%!" message
+  in
+  let diagnostics ~uri:_ ~version:_ _diags = () in
+  let fileProgress ~uri:_ ~version:_ _pinfo = () in
+  let perfData ~uri:_ ~version:_ _perf = () in
+  { Fleche.Io.CallBack.trace; message; diagnostics; fileProgress; perfData }
+
+let read_raw ~uri =
+  let file = Lang.LUri.File.to_string_file uri in
+  Stdlib.In_channel.(with_open_text file input_all)
+
+let find_thm ~(doc : Fleche.Doc.t) ~thm =
+  let { Fleche.Doc.toc; _ } = doc in
+  match CString.Map.find_opt thm toc with
+  | None ->
+    let msg = Format.asprintf "@[[find_thm] Theorem not found!@]" in
+    Error (Start_error.Theorem_not_found msg)
+  | Some range ->
+    if pet_debug then Format.eprintf "@[[find_thm] Theorem found!@\n@]%!";
+    (* let point = (range.start.line, range.start.character) in *)
+    let point = (range.end_.line, range.end_.character) in
+    let approx = Fleche.Info.PrevIfEmpty in
+    let node = Fleche.Info.LC.node ~doc ~point approx in
+    let error =
+      Start_error.Theorem_not_found
+        (Format.asprintf "@[[find_thm] No node found for point (%d, %d) @]"
+           (fst point) (snd point))
+    in
+    Base.Result.of_option ~error node |> Result.map Fleche.Doc.Node.state
+
+let pp_diag fmt { Lang.Diagnostic.message; _ } =
+  Format.fprintf fmt "%a" Pp.pp_with message
+
+let print_diags (doc : Fleche.Doc.t) =
+  let d = Fleche.Doc.diags doc in
+  Format.(eprintf "@[<v>%a@]" (pp_print_list pp_diag) d)
+
+let init ~token ~debug ~root =
+  let init = init_coq ~debug in
+  Fleche.Io.CallBack.set io;
+  let dir = Lang.LUri.File.to_string_file root in
+  let ( let+ ) = Base.Result.( >>| ) in
+  let+ workspace = Coq.Workspace.guess ~token ~debug ~cmdline ~dir in
+  let files = Coq.Files.make () in
+  Fleche.Doc.Env.make ~init ~workspace ~files
+
+let start ~token ~env ~uri ~thm =
+  let raw = read_raw ~uri in
+  (* Format.eprintf "raw: @[%s@]%!" raw; *)
+  let doc = Fleche.Doc.create ~token ~env ~uri ~version:0 ~raw in
+  print_diags doc;
+  let target = Fleche.Doc.Target.End in
+  let doc = Fleche.Doc.check ~io ~token ~target ~doc () in
+  find_thm ~doc ~thm
+
+let parse ~loc tac st =
+  let str = Gramlib.Stream.of_string tac in
+  let str = Coq.Parsing.Parsable.make ?loc str in
+  Coq.Parsing.parse ~st str
+
+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
+
+let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
+  match r with
+  | { r = Interrupted; feedback = _ } -> Error Run_error.Interrupted
+  | { r = Completed (Error (User (_loc, msg))); feedback = _ } ->
+    Error (Run_error.Coq (Pp.string_of_ppcmds msg))
+  | { r = Completed (Error (Anomaly (_loc, msg))); feedback = _ } ->
+    Error (Run_error.Anomaly (Pp.string_of_ppcmds msg))
+  | { r = Completed (Ok r); feedback = _ } -> Ok r
+
+let run_tac ~token ~st ~tac : (Coq.State.t, Run_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
+  |> protect_to_result
+
+let goals ~token ~st =
+  let f goals =
+    let f = Coq.Goals.map_reified_goal ~f:Pp.string_of_ppcmds in
+    let g = Pp.string_of_ppcmds in
+    Option.map (Coq.Goals.map_goals ~f ~g) goals
+  in
+  Coq.Protect.E.map ~f (Fleche.Info.Goals.goals ~token ~st) |> protect_to_result
+
+let contents () = ()