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
61
62
63
64
65
66
67
68
69
70
open Fleche
let msg_info ~io = Io.(Report.msg ~io ~lvl:Info)
let pp_goals ~token ~st =
match Coq.State.lemmas ~st with
| None -> Coq.Pp_t.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; _ }))
; _
} -> Coq.Pp_t.(str "error when printing goals: " ++ msg)
| { Coq.Protect.E.r = Interrupted; _ } ->
Coq.Pp_t.str "goal printing was interrupted")
module Error_info = struct
type t =
{ error : Coq.Pp_t.t
; command : string
; goals : Coq.Pp_t.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@]" Coq.Pp_t.pp_with error command Coq.Pp_t.pp_with goals
end
let ~token ~root ~contents (node : Doc.Node.t) =
let errors = List.filter Lang.Diagnostic.is_error node.diags in
let st = Stdlib.Option.fold ~some:Doc.Node.state ~none: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 ()