[plugin] Goal dump plugin.

This is a simple plugin that will output the Ast and goals of a
document. This is just a start, there are many tweaks that could be
performed indeed.

cc: @gbdrt

Co-authored-by: Guillaume Baudart <guillaume.baudart@inria.fr>

CHANGES.md

@@ -58,6 +58,8 @@
    (@ejgallego, #661)
  - interpret require thru our own custom execution env-aware path
    (@bhaktishh, @ejgallego, #642, #643, #644)
+ - new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump
+   goals from a document (@ejgallego @gbdrt, #619)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

compiler/compile.ml

@@ -27,8 +27,8 @@ let save_diags_file ~(doc : Fleche.Doc.t) =
 let compile_file ~cc file =
   let { Cc.io; root_state; workspaces; default; token } = cc in
   let lvl = Io.Level.info in
-  let message = Format.asprintf "compiling file %s@\n%!" file in
-  io.message ~lvl ~message;
+  let message = Format.asprintf "compiling file %s" file in
+  Io.Report.message ~io ~lvl ~message;
   match Lang.LUri.(File.of_uri (of_string file)) with
   | Error _ -> ()
   | Ok uri -> (

examples/Demo.v

@@ -0,0 +1,5 @@
+Theorem add_0_r : forall n:nat, n + 0 = n.
+Proof.
+   intros n.  induction n as [| n' IHn'].
+  -  (* n = 0 *)    reflexivity.
+  -  (* n = S n' *) simpl.  rewrite -> IHn'. reflexivity.  Qed.

plugins/README.md

@@ -0,0 +1,13 @@
+# coq-lsp / Flèche plugins
+
+Easiest way to use plugins is
+
+```
+$ fcc --root=dir --plugin=coq-lsp.plugin.$name file.v
+```
+
+- `example`: prints a "this file was checked" message
+- `astdump`: dumps the Ast of the document, in both sexp and JSON
+  formats
+- `goaldump`: dumps the Ast of the document in JSON format, along with
+  the goals at that state.

plugins/goaldump/dune

@@ -0,0 +1,6 @@
+(library
+ (name Goaldumpl_plugin)
+ (public_name coq-lsp.plugin.goaldump)
+ (preprocess
+  (pps ppx_deriving_yojson))
+ (libraries coq-lsp.fleche coq-lsp.lsp))

plugins/goaldump/main.ml

@@ -0,0 +1,100 @@
+open Fleche
+
+(* Put these in an utility function for plugins *)
+let of_execution ~io ~what (v : (_, _) Coq.Protect.E.t) =
+  match v with
+  | { r; feedback = _ } -> (
+    match r with
+    | Coq.Protect.R.Completed (Ok goals) -> goals
+    | Coq.Protect.R.Completed (Error (Anomaly err))
+    | Coq.Protect.R.Completed (Error (User err)) ->
+      let message =
+        Format.asprintf "error when retrieving %s: %a" what Pp.pp_with (snd err)
+      in
+      Io.Report.message ~io ~lvl:Io.Level.error ~message;
+      None
+    | Coq.Protect.R.Interrupted -> None)
+
+let extract_raw ~(contents : Contents.t) ~(range : Lang.Range.t) =
+  let start = range.start.offset in
+  let length = range.end_.offset - start in
+  (* We need to be careful here as Doc.t always adds a last empty node on EOF,
+     but somehow the offset of this node seems suspicious, it seems like the Coq
+     parser increases the offset by one, we need to investigate. *)
+  let length =
+    if String.length contents.raw < start + length then
+      String.length contents.raw - start
+    else length
+  in
+  String.sub contents.raw start length
+
+(* We output a record for each sentence in the document, linear order. Note that
+   for unparseable nodes, we don't have an AST. *)
+module AstGoals = struct
+  (* Just to bring the serializers in scope *)
+  module Lang = Lsp.JLang
+  module Coq = Lsp.JCoq
+
+  type 'a t =
+    { raw : string
+    ; range : Lang.Range.t
+    ; ast : Coq.Ast.t option
+    ; goals : 'a Coq.Goals.reified_pp option
+    }
+  [@@deriving to_yojson]
+
+  let of_node ~io ~token ~(contents : Contents.t) (node : Doc.Node.t) =
+    let range = node.range in
+    let raw = extract_raw ~contents ~range in
+    let ast = Option.map (fun n -> n.Doc.Node.Ast.v) node.ast in
+    let st = node.state in
+    let goals = of_execution ~io ~what:"goals" (Info.Goals.goals ~token ~st) in
+    { raw; range; ast; goals }
+end
+
+let pp_json pp fmt (astgoal : _ AstGoals.t) =
+  let g_json = AstGoals.to_yojson pp astgoal in
+  Yojson.Safe.pretty_print fmt g_json
+
+(* For now we have not added sexp serialization, but we can easily do so *)
+(* let pp_sexp fmt (astgoal : AstGoals.t) = *)
+(*   let g_sexp = AstGoals.sexp_of astgoal in *)
+(*   Sexplib.Sexp.pp_hum fmt sast *)
+
+let pw pp fmt v = Format.fprintf fmt "@[%a@]@\n" pp v
+
+let pp_ast_goals ~io ~token ~contents pp fmt node =
+  let res = AstGoals.of_node ~io ~token ~contents node in
+  pw pp fmt res
+
+let dump_goals ~io ~token ~out_file ~(doc : Doc.t) pp =
+  let out = Stdlib.open_out out_file in
+  let fmt = Format.formatter_of_out_channel out in
+  let contents = doc.contents in
+  List.iter (pp_ast_goals ~io ~token ~contents pp fmt) doc.nodes;
+  Format.pp_print_flush fmt ();
+  Stdlib.close_out out
+
+let dump_ast ~io ~token ~(doc : Doc.t) =
+  let uri = doc.uri in
+  let uri_str = Lang.LUri.File.to_string_uri uri in
+  let message =
+    Format.asprintf "[goaldump plugin] dumping goals for %s ..." uri_str
+  in
+  let lvl = Io.Level.info in
+  Io.Report.message ~io ~lvl ~message;
+  let out_file_j = Lang.LUri.File.to_string_file uri ^ ".json.goaldump" in
+  let pp d = `String (Pp.string_of_ppcmds d) in
+  (* Uncomment to output Pp-formatted goals *)
+  (* let pp d = Lsp.JCoq.Pp.to_yojson d in *)
+  let () = dump_goals ~io ~token ~out_file:out_file_j ~doc (pp_json pp) in
+  (* let out_file_s = Lang.LUri.File.to_string_file uri ^ ".sexp.goaldump" in *)
+  (* let () = dump_goals ~out_file:out_file_s ~doc pp_sexp in *)
+  let message =
+    Format.asprintf "[ast plugin] dumping ast for %s was completed!" uri_str
+  in
+  Io.Report.message ~io ~lvl ~message;
+  ()
+
+let main () = Theory.Register.add dump_ast
+let () = main ()

test/compiler/run.t

@@ -23,7 +23,6 @@ Compile a single file, don't generate a `.vo` file:
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
-  
   $ ls proj1
   a.diags
   a.v
@@ -40,7 +39,6 @@ Compile a single file, generate a .vo file
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
-
   $ ls proj1
   a.diags
   a.v
@@ -61,7 +59,6 @@ Compile a dependent file
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/b.v
-  
   $ ls proj1
   a.diags
   a.v
@@ -82,9 +79,7 @@ Compile both files
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
-
   [message] compiling file proj1/b.v
-
   $ ls proj1
   a.diags
   a.v
@@ -105,7 +100,6 @@ Compile a dependent file without the dep being built
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/b.v
-  
   $ ls proj1
   a.diags
   a.v
@@ -167,9 +161,7 @@ Use two workspaces
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
-  
   [message] compiling file proj2/b.v
-  
   fcc: internal error, uncaught exception:
        Sys_error("proj2/b.v: No such file or directory")
        
@@ -186,7 +178,6 @@ Load the example plugin
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
-
   [message] [example plugin] file checking for proj1/a.v was completed
 
 Load the astdump plugin
@@ -200,7 +191,6 @@ Load the astdump plugin
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
-  
   [message] [ast plugin] dumping ast for proj1/a.v ...
   [message] [ast plugin] dumping ast for proj1/a.v was completed!
 
@@ -214,3 +204,19 @@ de-serialize the document back and check.
   $ ls proj1/a.v.json.astdump proj1/a.v.sexp.astdump
   proj1/a.v.json.astdump
   proj1/a.v.sexp.astdump
+
+We do the same for the goaldump plugin:
+  $ fcc --plugin=coq-lsp.plugin.goaldump --root proj1 proj1/a.v
+  [message] Configuration loaded from Command-line arguments
+   - coqlib is at: [TEST_PATH]
+     + coqcorelib is at: [TEST_PATH]
+   - Modules [Coq.Init.Prelude] will be loaded by default
+   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - ocamlpath wasn't overriden
+     + findlib config: [TEST_PATH]
+     + findlib default location: [TEST_PATH]
+  [message] compiling file proj1/a.v
+  [message] [goaldump plugin] dumping goals for proj1/a.v ...
+  [message] [ast plugin] dumping ast for proj1/a.v was completed!
+  $ ls proj1/a.v.json.goaldump
+  proj1/a.v.json.goaldump