From 8a965d8af53b3525aa24b74cfb26c3582bf8e0fb Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 8 Jun 2024 17:25:10 +0200 Subject: [PATCH] [hover] Display debug statistic for universes New config option `show_universes_on_hover`, that will display information about the universe graph for developer debug. Results seem a bit mixed, more research is needed. Fixes #330 --- CHANGES.md | 4 +++- controller/rq_hover.ml | 29 ++++++++++++++++++++++++++++- controller/rq_hover.mli | 5 +++++ coq/state.ml | 20 ++++++++++++++++++++ coq/state.mli | 4 ++++ editor/code/package.json | 5 +++++ editor/code/src/config.ts | 2 ++ fleche/config.ml | 3 +++ 8 files changed, 70 insertions(+), 2 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 9ed426ecc..fc9bf3d74 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -4,7 +4,7 @@ - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, #698) - - [fleche] Remove 8.16 compatibility layer (@ejgallgo, #747) + - [fleche] Remove 8.16 compatibility layer (@ejgallego, #747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, #748) @@ -47,6 +47,8 @@ - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, #772) + - [hover] New option `show_universes_on_hover` that will display + universe data on hover (@ejgallego, @SkySkimmer, #666) # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_... ---------------------------------------------------- diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index 00abe0727..38fec2ff7 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -263,6 +263,33 @@ module InputHelp : HoverProvider = struct let h = Handler.MaybeNode input_help end +module UniDiff = struct + let show_unidiff ~token ?diff ~st () = + let nuniv_prev, nconst_prev = + match diff with + | Some st -> ( + match Coq.State.info_universes ~token ~st with + | Coq.Protect.{ E.r = R.Completed (Ok (nuniv, nconst)); feedback = _ } + -> (nuniv, nconst) + | _ -> (0, 0)) + | None -> (0, 0) + in + match Coq.State.info_universes ~token ~st with + | Coq.Protect.{ E.r = R.Completed (Ok (nuniv, nconst)); feedback = _ } -> + Some + (Format.asprintf "@[univ data (%4d,%4d) {+%d, +%d}@\n@]" nuniv nconst + (nuniv - nuniv_prev) (nconst - nconst_prev)) + | _ -> None + + let h ~token ~contents:_ ~point:_ ~(node : Fleche.Doc.Node.t) = + if !Fleche.Config.v.show_universes_on_hover then + let diff = Option.map Fleche.Doc.Node.state node.prev in + show_unidiff ~token ?diff ~st:node.state () + else None + + let h = Handler.WithNode h +end + module Register = struct let handlers : Handler.t list ref = ref [] let add fn = handlers := fn :: !handlers @@ -282,7 +309,7 @@ end (* Register in-file hover plugins *) let () = List.iter Register.add - [ Loc_info.h; Stats.h; Type.h; Notation.h; InputHelp.h ] + [ Loc_info.h; Stats.h; Type.h; Notation.h; InputHelp.h; UniDiff.h ] let hover ~token ~(doc : Fleche.Doc.t) ~point = let node = Info.LC.node ~doc ~point Exact in diff --git a/controller/rq_hover.mli b/controller/rq_hover.mli index d97867311..263003c80 100644 --- a/controller/rq_hover.mli +++ b/controller/rq_hover.mli @@ -41,3 +41,8 @@ end module Register : sig val add : Handler.t -> unit end + +(** Auxiliary functions *) +module UniDiff : sig + (** [info_universes ~node] returns [nunivs, nconstraints] *) +end diff --git a/coq/state.ml b/coq/state.ml index 5d8e6e37f..2ba815954 100644 --- a/coq/state.ml +++ b/coq/state.ml @@ -135,3 +135,23 @@ let admit_goal ~st () = { st with interp = { st.interp with lemmas } } let admit_goal ~token ~st = Protect.eval ~token ~f:(admit_goal ~st) () + +let count_edges univ = + let univ = UGraph.repr univ in + Univ.Level.Map.fold + (fun _ node acc -> + acc + + + match node with + | UGraph.Alias _ -> 1 + | Node m -> Univ.Level.Map.cardinal m) + univ + (Univ.Level.Map.cardinal univ) + +let info_universes ~token ~st = + let open Protect.E.O in + let+ univ = in_state ~token ~st ~f:Global.universes () in + let univs = UGraph.domain univ in + let nuniv = Univ.Level.Set.cardinal univs in + let nconst = count_edges univ in + (nuniv, nconst) diff --git a/coq/state.mli b/coq/state.mli index 0a32c9412..2e5b7152f 100644 --- a/coq/state.mli +++ b/coq/state.mli @@ -38,6 +38,10 @@ val admit : token:Limits.Token.t -> st:t -> (t, Loc.t) Protect.E.t (** Admit the current sub-goal *) val admit_goal : token:Limits.Token.t -> st:t -> (t, Loc.t) Protect.E.t +(** Info about universes *) +val info_universes : + token:Limits.Token.t -> st:t -> (int * int, Loc.t) Protect.E.t + (** Extra / interanl *) val marshal_in : in_channel -> t diff --git a/editor/code/package.json b/editor/code/package.json index d1e2d4660..d4ccf71ee 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -217,6 +217,11 @@ "type": "boolean", "default": false, "description": "Show parsing information for a sentence on hover." + }, + "coq-lsp.show_universes_on_hover": { + "type": "boolean", + "default": false, + "description": "Show universe information and diff for a sentence on hover." } } }, diff --git a/editor/code/src/config.ts b/editor/code/src/config.ts index 21f4821f8..a55320fca 100644 --- a/editor/code/src/config.ts +++ b/editor/code/src/config.ts @@ -13,6 +13,7 @@ export interface CoqLspServerConfig { pp_type: 0 | 1 | 2; show_stats_on_hover: boolean; show_loc_info_on_hover: boolean; + show_universes_on_hover: boolean; check_only_on_request: boolean; send_perf_data: boolean; } @@ -35,6 +36,7 @@ export namespace CoqLspServerConfig { pp_type: wsConfig.pp_type, show_stats_on_hover: wsConfig.show_stats_on_hover, show_loc_info_on_hover: wsConfig.show_loc_info_on_hover, + show_universes_on_hover: wsConfig.show_universes_on_hover, check_only_on_request: wsConfig.check_only_on_request, send_perf_data: wsConfig.send_perf_data, }; diff --git a/fleche/config.ml b/fleche/config.ml index 2ad0b3025..27dc90902 100644 --- a/fleche/config.ml +++ b/fleche/config.ml @@ -39,6 +39,8 @@ type t = ; show_stats_on_hover : bool [@default false] (** Show stats on hover *) ; show_loc_info_on_hover : bool [@default false] (** Show loc info on hover *) + ; show_universes_on_hover : bool [@default false] + (** Show universe data on hover *) ; pp_json : bool [@default false] (** Whether to pretty print the protocol JSON on the wire *) ; send_perf_data : bool [@default true] @@ -71,6 +73,7 @@ let default = ; pp_type = 0 ; show_stats_on_hover = false ; show_loc_info_on_hover = false + ; show_universes_on_hover = false ; verbosity = 2 ; pp_json = false ; send_perf_data = true