package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file main.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
(* Example plugin to print errors with goals *)
(* c.f. https://github.com/coq/coq/issues/19601 *)
open Fleche

let msg_info ~io = Io.(Report.msg ~io ~lvl:Info)

let pp_goals ~token ~st =
  match Coq.State.lemmas ~st with
  | None -> Pp.str "no goals"
  | Some proof -> (
    match Coq.Print.pr_goals ~token ~proof with
    | { Coq.Protect.E.r = Completed (Ok goals); _ } -> goals
    | { Coq.Protect.E.r =
          Completed (Error (User { msg; _ } | Anomaly { msg; _ }))
      ; _
      } -> Pp.(str "error when printing goals: " ++ msg)
    | { Coq.Protect.E.r = Interrupted; _ } ->
      Pp.str "goal printing was interrupted")

module Error_info = struct
  type t =
    { error : Pp.t
    ; command : string
    ; goals : Pp.t
    }

  let print ~io { error; command; goals } =
    msg_info ~io
      "[explain errors plugin]@\n\
       Error:@\n\
      \ @[%a@]@\n\
       @\n\
       when trying to apply@\n\
       @\n\
      \ @[%s@]@\n\
       for goals:@\n\
      \ @[%a@]" Pp.pp_with error command Pp.pp_with goals
end

let extract_errors ~token ~root ~contents (node : Doc.Node.t) =
  let errors = List.filter Lang.Diagnostic.is_error node.diags in
  let st = Option.cata Doc.Node.state root node.prev in
  let command = Contents.extract_raw ~contents ~range:node.range in
  let goals = pp_goals ~token ~st in
  List.map
    (fun { Lang.Diagnostic.message; _ } ->
      { Error_info.error = message; command; goals })
    errors

let explain_error ~io ~token ~(doc : Doc.t) =
  let root = doc.root in
  let contents = doc.contents in
  let errors =
    List.(map (extract_errors ~token ~root ~contents) doc.nodes |> concat)
  in
  msg_info ~io "[explain errors plugin] we got %d errors" (List.length errors);
  List.iter (Error_info.print ~io) errors

let main () = Theory.Register.Completed.add explain_error
let () = main ()
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct