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

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

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
 

petanque/README.md

@@ -0,0 +1,85 @@
+_Petanque_ (pronounced "petanque") is a gym-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
+
+## Authors
+
+- Guilaume Baudart (Inria)
+- Emilio J. Gallego Arias (Inria)
+- Laetitia Teodorescu (Inria)
+
+## Acknowlements
+
+- Alex-Sánchez Stern
+
+## Install instructions
+
+Once in a `coq-lsp` dev environment, you need
+
+Then do the `ocaml-in-python` setup:
+
+```
+You should register the "ocaml" package in your Python environment.
+   There are two options:
+
+     (1) either you register the package with "pip" using the following
+         command:
+           pip install --editable "/home/egallego/.opam/dev-coq-lsp/lib/ocaml-in-python"
+
+     (2) or you add the following definition to your environment:
+           export PYTHONPATH="/home/egallego/.opam/dev-coq-lsp/share/python/:$PYTHONPATH"
+```
+
+## Running `pet shell`
+
+Only once, setup the coq-lsp build environment (if you haven't already):
+```
+opam install --deps-only .
+make submodules-init
+```
+
+to build and execute `petanque` do:
+```
+make
+dune exec -- rlwrap %{bin:pet}
+```
+
+`rlwrap` is just a convenience, if your dune version is too old and
+don't recognize the `%{bin:pet}` form, you can just do `dune exec -- pet`.
+
+### A first example:
+
+Please use one line per json input. json input examples are:
+```json
+["Start",{"uri":"file:///home/egallego/research/coq-lsp/examples/ex0.v","thm":"addnC"}]
+["Start",131266756246311]
+
+["Run_tac", {"st": 131266756246311, "tac": "induction n."}]
+["Run_tac",131266894677423]
+
+["Run_tac", {"st": 131266894677423, "tac": "simpl."}]
+["Run_tac",131266896660087]
+
+["Run_tac", {"st": 131266896660087, "tac": "auto."}]
+["Run_tac",131266896448871]
+```
+
+Seems to work! (TM) (Famous last words)
+
+## Running (not yet working ocaml-in-python)
+
+```
+make && PYTHONPATH="/home/egallego/.opam/dev-coq-lsp/share/python/:$PYTHONPATH" dune exec -- python3
+```
+
+then in the Python shell:
+```
+import ocaml
+ocaml.require("coq-lsp.petanque")
+
+from ocaml import Petanque
+
+Petanque.Agent.start()
+```

petanque/agent.ml

@@ -0,0 +1,147 @@
+(* Petanque *)
+
+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 () = ()

petanque/agent.mli

@@ -0,0 +1,65 @@
+(** Petanque.Agent *)
+module State : sig
+  type t
+
+  val hash : t -> int
+  val equal : t -> t -> bool
+end
+
+module Env : sig
+  (** Coq Workspaces / project enviroments *)
+  type t
+end
+
+(** Init errors *)
+module Init_error : sig
+  type t = string
+end
+
+(** Runtime errors *)
+module Run_error : sig
+  type t =
+    | Interrupted
+    | Parsing of string
+    | Coq of string
+    | Anomaly of string
+end
+
+module Start_error : sig
+  type t =
+    | Run of Run_error.t  (** Runtime errors may happen on start *)
+    | Theorem_not_found of string
+end
+
+(** [init ~debug ~root] Initializes Coq, with project and workspace settings
+    from [root]. [root] needs to be in URI format. This function needs to be
+    called _once_ before all others. *)
+val init :
+     token:Coq.Limits.Token.t
+  -> debug:bool
+  -> root:Lang.LUri.File.t
+  -> (Env.t, Init_error.t) Result.t
+
+(** [start uri thm] start a new proof for theorem [thm] in file [uri]. *)
+val start :
+     token:Coq.Limits.Token.t
+  -> env:Env.t
+  -> uri:Lang.LUri.File.t
+  -> thm:string
+  -> (State.t, Start_error.t) Result.t
+
+(** [run_tac ~token ~st ~tac] tries to run [tac] over state [st] *)
+val run_tac :
+     token:Coq.Limits.Token.t
+  -> st:State.t
+  -> tac:string
+  -> (State.t, Run_error.t) Result.t
+
+(** [goals ~token ~st] return the list of goals for a given [st] *)
+val goals :
+     token:Coq.Limits.Token.t
+  -> st:State.t
+  -> (string Coq.Goals.reified_pp option, Run_error.t) Result.t
+
+(** Return the table of contents for a file *)
+val contents : unit -> unit

petanque/dune

@@ -0,0 +1,4 @@
+(library
+ (public_name coq-lsp.petanque)
+ (name petanque)
+ (libraries fleche))