[hover] Display debug statistic for universes #666
Conversation
|
@SkySkimmer find some preliminary results on typical profile for 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}
|
ejgallego
force-pushed
the
hover_univdiff
branch
3 times, most recently
from
410e6f7
to
ae5cbe9
Compare
|
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 |
Probably just collapsing some loops? eg if you have |
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 |
|
See also coq/coq#18900 |
|
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 |
|
Does your debug info say +1 univ on something like Lemma foo : forall A : Type, A -> A.
Proof. intros A x;exact x. Qed.? |
It says so yes. Note that I don't restore the initial env at |
Stats seem a bit mixed, more research is needed. We will improve the analysis shortly, by output diffs and summaries.
Can be used with ``` $ dune exec -- fcc --root $absolute_path --plugin=coq-lsp.plugin.univdiff $absolute_path.v $ cat $absolute_path.v.univdiff ``` Attention to compiling files with error-recovery, that can lead to misleading results.
|
May I suggest using the heatmap for this? |
Stats seem a bit mixed, more research is needed.
We will improve the analysis shortly, for now we do two kind of analysis:
fcc --root $abs_path --plugin=coq-lsp.plugin.univdiff $abs_file.v, the plugin will output an$abs_file.v.univdifffile with the following information:univs for "sentence": (nunivs, nconstr) { +diff_nunivs, +diff_constr }for "sentence"s that have changed the number of universesqeditems, whereqed_total: nis the number ofqedin the file, andqed_yes: nis the number ofqedthat actually changes the universe constraints.