[hover] Display debug statistic for universes

[ejgallego]

Stats seem a bit mixed, more research is needed.

We will improve the analysis shortly, for now we do two kind of analysis:

• on hover, we print the number of universes and constraints at point

In #773 , there is also a plugin:

• using fcc --root $abs_path --plugin=coq-lsp.plugin.univdiff $abs_file.v , the plugin will output an $abs_file.v.univdiff file with the following information:
  • a line univs for "sentence": (nunivs, nconstr) { +diff_nunivs, +diff_constr } for "sentence"s that have changed the number of universes
  • a summary for qed items, where qed_total: n is the number of qed in the file, and qed_yes: n is the number of qed that actually changes the universe constraints.

Fixes #310

[ejgallego]

@SkySkimmer find some preliminary results on Qed universe alterations:

- ssrnat.v: qed_total: 479 / qed_yes: 10
- seq.v: qed_total: 790 / qed_yes: 179
- bigop.v: qed_total: 295 / qed_yes: 137
- compcert/lib/Coqlib: qed_total: 114 / qed_yes: 70
- compcert/lib/Integers: qed_total: 404 / qed_yes: 3

typical profile for ssrnat.v:

univs for "From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.":
 ( 751,3806) {+344, +1802}
univs for "Require Import BinNat.":
 (1017,4914) {+266, +1108}
univs for "Require BinPos Ndec.":
 (1373,7080) {+356, +2166}
univs for "Qed.":
 (1374,7084) {+1, +4}
univs for "Qed.":
 (1374,7085) {+0, +1}
univs for "Qed.":
 (1375,7088) {+1, +3}
univs for "Inductive ex_minn_spec : nat -> Type :=
  ExMinnSpec m of P m & (forall n, P n -> n >= m) : ex_minn_spec m.":
 (1376,7090) {+1, +2}
univs for "Variable T : Type.":
 (1377,7092) {+1, +2}
univs for "Qed.":
 (1377,7093) {+0, +1}
univs for "Qed.":
 (1377,7094) {+0, +1}
univs for "Qed.":
 (1377,7095) {+0, +1}
univs for "Qed.":
 (1377,7100) {+0, +5}
univs for "Qed.":
 (1378,7106) {+1, +6}
univs for "Qed.":
 (1379,7113) {+1, +7}
univs for "Variable T : Type.":
 (1380,7115) {+1, +2}
univs for "Qed.":
 (1380,7116) {+0, +1}

[SkySkimmer]

How do I read those results?

[ejgallego]

How do I read those results?

Added some more info to the PR description. Will add some more info and an improved hover mode.

I did some more experiments in Compcert for example and the results are not too bad, we should be able to skip a lot of proofs and re-check them, tho still the dynamic barriers can be complex to schedule in parallel, but the linear model doesn't look too bad.

Something interesting is that some Qed happen to remove constraints.

[SkySkimmer]

Something interesting is that some Qed happen to remove constraints.

Probably just collapsing some loops? eg if you have a <= b <= c and a <= c (3 constraints) then add c <= a the graph becomes a = b = c (2 constraints)

[ejgallego]

Something interesting is that some Qed happen to remove constraints.

Probably just collapsing some loops? eg if you have a <= b <= c and a <= c (3 constraints) then add c <= a the graph becomes a = b = c (2 constraints)

Interesting! I'm gonna add some code to "diff" universe graphs so we can see with more details what is going on.

Feel free to push to this branch if you want to add some kind of diff, or let me know if we already have some functions that could be useful.

Note that I do Global.universes () so we are not getting the new constraints added in tactics, maybe we would like to correct this too?

[SkySkimmer]

See also https://github.com/coq/coq/pull/18900

[ejgallego]

Cool!

The way I'd go ahead with this PR is to have the plugin emit a warning when the diff is not 0, and in some cases display the diff (for example not on require)

That should be a good way to debug rebuilds as soon as we start skipping Qed proofs here.

[SkySkimmer]

Does your debug info say +1 univ on something like

Lemma foo : forall A : Type, A -> A.
Proof. intros A x;exact x. Qed.

?

[ejgallego]

Lemma foo : forall A : Type, A -> A.
Proof. intros A x;exact x. Qed.

It says

univs for "Qed.":
 ( 408,2006) {+1, +2}
qed_total: 1 / qed_yes: 1

so yes.

Note that I don't restore the initial env at Qed time as is done in the Stm, so that's a difference that could matter.

[Alizter]

May I suggest using the heatmap for this?

[ejgallego]

I think this is ready for now @SkySkimmer , would an optional warning for Qed that leak be useful?

Maybe that's something that could be done in the Coq side, but here is easy to do too.