Conversation
coqbot-app
Bot
added
the
needs: full CI
| (match gref with | ||
| | ConstRef c -> | ||
| let def_height_c = Environ.constant_definitional_height (Global.env ()) c in | ||
| Global.set_constant_def_height c def_height_c; |
There was a problem hiding this comment.
This should be computed by the kernel and we should trust the height, in my opinion. (As usual limitations with functors apply.)
26d026b to
5bcf719
Compare
|
According to the CI logs, there are 7 tests failing: The first one is the test that I added. a I had a look at the other tests' outputs and there are indeed differences in outputs. rocq/test-suite/output/Arguments.v Lines 12 to 18 in 295beaf When If I deactivate the flag, the messages coincide with what's recorded in the .out files. So I suppose I shouldn't change these files, seeing as the flag won't be active by default. |
f05407e to
52ac248
Compare
|
@coqbot bench |
|
I am curious to see if this will run into the same problem that lead to the mathcomp regressions in #21514 (comment). I don't see a reason why it wouldn't, given that unfolding a term will decrease the depth and in case of a tie we'll ping-pong back and forth between the LHS and RHS. (I suspect this back and forth is also responsible for a lot of the slowdown in other projects in that PR but I have not confirmed that.) I wonder if we can work around the problem by committing to a side in a way that is stable over delta reductions at the head of the term. If the heuristic chooses |
|
🏁 Bench results: INFO: failed to install rocq-bignums (dependency rocq-stdlib failed) 🐢 Top 25 slow downs┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 0.00205 4.56 4.5530 222204.20% 2007 rocq-mathcomp-order/order/total_order_instances.v.html │ │ 0.000872 0.947 0.9464 108531.42% 2747 rocq-mathcomp-boot/boot/finset.v.html │ │ 0.000804 0.939 0.9377 116633.21% 2010 rocq-mathcomp-boot/boot/finset.v.html │ │ 0.000645 0.937 0.9367 145222.48% 2008 rocq-mathcomp-boot/boot/finset.v.html │ │ 0.000816 0.935 0.9341 114475.61% 2011 rocq-mathcomp-boot/boot/finset.v.html │ │ 0.000907 0.846 0.8450 93160.31% 2013 rocq-mathcomp-boot/boot/finset.v.html │ │ 0.000684 0.735 0.7340 107305.99% 270 rocq-mathcomp-boot/boot/finset.v.html │ │ 0.0134 0.543 0.5296 3949.19% 277 rocq-mathcomp-boot/boot/fingraph.v.html │ │ 0.000553 0.454 0.4532 81952.80% 2012 rocq-mathcomp-boot/boot/finset.v.html │ │ 0.00116 0.344 0.3428 29452.23% 1939 rocq-mathcomp-order/order/total_order_instances.v.html │ │ 0.00821 0.348 0.3401 4144.47% 934 rocq-mathcomp-boot/boot/fingraph.v.html │ │ 0.000554 0.238 0.2375 42867.15% 2514 rocq-mathcomp-boot/boot/finset.v.html │ │ 0.00341 0.178 0.1745 5117.63% 256 rocq-mathcomp-order/order/interval.v.html │ │ 0.000997 0.154 0.1527 15312.14% 1941 rocq-mathcomp-order/order/total_order_instances.v.html │ │ 0.000538 0.104 0.1036 19259.85% 2016 rocq-mathcomp-boot/boot/finset.v.html │ │ 0.000320 0.103 0.1025 32026.56% 2291 rocq-mathcomp-boot/boot/finset.v.html │ │ 0.000363 0.103 0.1023 28185.67% 271 rocq-mathcomp-boot/boot/finset.v.html │ │ 0.00241 0.0562 0.0537 2227.14% 910 rocq-mathcomp-boot/boot/fingraph.v.html │ │ 1.40 1.44 0.0483 3.46% 87 rocq-mathcomp-order/order/total_order.v.html │ │ 1.44 1.49 0.0457 3.17% 150 rocq-mathcomp-order/order/complemented_lattice.v.html │ │ 0.888 0.929 0.0414 4.67% 3 rocq-mathcomp-order/order/all_order.v.html │ │ 0.000102 0.0341 0.0340 33302.94% 94 rocq-mathcomp-order/order/total_order_instances.v.html │ │ 0.898 0.927 0.0294 3.27% 872 rocq-mathcomp-order/order/lattice.v.html │ │ 0.583 0.612 0.0287 4.92% 5 rocq-mathcomp-order/order/orderedzmod.v.html │ │ 0.000383 0.0281 0.0278 7247.26% 105 rocq-mathcomp-boot/boot/prime.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌──────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 0.0309 0.00139 -0.0295 -95.51% 208 rocq-mathcomp-boot/boot/ssrAC.v.html │ │ 0.0309 0.00179 -0.0291 -94.21% 40 rocq-mathcomp-boot/boot/binomial.v.html │ │ 0.0483 0.0196 -0.0288 -59.51% 1065 rocq-mathcomp-order/order/lattice.v.html │ │ 0.0285 0.000802 -0.0277 -97.19% 110 rocq-mathcomp-boot/boot/prime.v.html │ │ 0.0244 0.00166 -0.0227 -93.22% 84 rocq-mathcomp-boot/boot/fingraph.v.html │ │ 0.0687 0.0473 -0.0214 -31.18% 145 rocq-mathcomp-order/order/interval.v.html │ │ 0.0208 0.000322 -0.0205 -98.45% 154 rocq-mathcomp-boot/boot/choice.v.html │ │ 0.0205 0.000150 -0.0203 -99.27% 96 rocq-mathcomp-boot/boot/div.v.html │ │ 0.0196 0.000509 -0.0190 -97.40% 362 rocq-mathcomp-boot/boot/seq.v.html │ │ 0.0145 0.000220 -0.0143 -98.48% 1329 rocq-mathcomp-boot/boot/nmodule.v.html │ │ 0.0121 0.000398 -0.0117 -96.72% 924 rocq-mathcomp-boot/boot/eqtype.v.html │ │ 0.0253 0.0137 -0.0116 -45.83% 1447 rocq-mathcomp-boot/boot/fintype.v.html │ │ 0.0147 0.00310 -0.0116 -78.98% 866 rocq-mathcomp-order/order/total_order_instances.v.html │ │ 0.0119 0.000450 -0.0115 -96.22% 458 rocq-mathcomp-boot/boot/finset.v.html │ │ 0.0119 0.000498 -0.0114 -95.80% 554 rocq-mathcomp-boot/boot/tuple.v.html │ │ 0.0127 0.00143 -0.0113 -88.74% 1996 rocq-mathcomp-order/order/total_order_instances.v.html │ │ 0.0134 0.00236 -0.0111 -82.41% 2413 rocq-mathcomp-boot/boot/bigop.v.html │ │ 0.0118 0.00114 -0.0107 -90.32% 2245 rocq-mathcomp-boot/boot/bigop.v.html │ │ 0.0172 0.00679 -0.0104 -60.56% 2351 rocq-mathcomp-boot/boot/bigop.v.html │ │ 0.0105 0.000340 -0.0101 -96.75% 864 rocq-mathcomp-boot/boot/bigop.v.html │ │ 0.0103 0.000641 -0.0097 -93.78% 56 rocq-mathcomp-order/order/order_instances.v.html │ │ 0.0102 0.000596 -0.0096 -94.17% 1222 rocq-mathcomp-boot/boot/seq.v.html │ │ 0.0102 0.000611 -0.0096 -94.01% 322 rocq-mathcomp-order/order/orderedzmod.v.html │ │ 0.0143 0.00493 -0.0094 -65.51% 2185 rocq-mathcomp-boot/boot/bigop.v.html │ │ 0.0839 0.0746 -0.0093 -11.12% 677 rocq-mathcomp-order/order/interval.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────┘ |
2659885 to
aeeae80
Compare
- Behind flag `Kernel Conversion Height Heuristic` - When a constant is defined, its definitional height [h] is computed and stored. - If the flag is active, a strategy level equal to [-h] is set for the constant. - Over-approximates dependencies between constants. I.e. if [c1] depends on [c2] => h1 > h2.
…purposes. - Updated some .out files to consider transparency levels shown when `About.` is run on definitions.
aeeae80 to
ae60841
Compare
| in | ||
| (kn, eff), senv | ||
|
|
||
| let set_constant_def_height kn dh senv = |
There was a problem hiding this comment.
This shouldn't be done after the fact, but at the very moment the constant body is created, so either from Constant_typing.infer_definition, or if you want to slightly tweak the type pconstant_body so that it's clear the height is empty at this point, somewhere around Safe_typing.add_constant.
4 participants
Adds an optional heuristic for the conversion of two constants.
Kernel Conversion Height Heuristichis computed and a strategy level equal to-his set for it.c1depends onc2=>h1 > h2.Changes:
kernel/declarations.mli : Added typing flag to (de)activate heuristic. Added field to constant_body record to store computed heights.
kernel/environ.ml : Added function to compute definitional height and to store the height in a constant's body
kernel/safe_typing.ml : Lifted functions defined in kernel/environ.ml to safe environments.
library/global.ml : Globalized functions defined in kernel/safe_typing.ml
vernac/comDefinition.ml : When heuristic is active,
do_definitioncomputes height of constant, stores computed height, and sets strategy level.vernac/vernacinterp.ml : When heuristic is active, transparent proof-ending commands (
Defined) triggers the mechanics mentioned above. This allows constants defined interactively to profit from the heuristic.vernac/vernacentries.ml : Register flag.
Added / updated test-suite.
make doc_gram_rsts.