I've been looking at `perf`

profiles of proofs and I saw one suspicious item today that I'd like to understand better. It's the call to `Evd.nf_univ_variables sigma`

in `prepare_hint`

called via `make_local_hint_db`

. IIUC it is called once for every lemma passed to `eauto`

via `using`

(probably `typeclasses eauto`

, too, but I am not sure). In a big proof I've been looking at today this call to universe normalization accounts for a total of 5% of the entire runtime. My first impulse was to try to perform the normalization only once for every call to `eauto`

but it turns out that the `sigma`

in question is the result of "instantiating" the provided lemmas, i.e. `sigma`

from the goal itself goes in and out comes a, presumably, slight larger `sigma`

which is at least in principle different for every provided lemma. Is there any way the universe normalizaton work could still be shared? Does it make sense to normalize the input `sigma`

once in order to save cost on normalizing the derived `sigma`

?

The code also has this comment which I don't fully understand. Is it possible that the normalization could be skipped entirely?

```
(* We re-abstract over uninstantiated evars and universes.
It is actually a bit stupid to generalize over evars since the first
thing make_resolves will do is to re-instantiate the products *)
let sigma = Evd.nf_univ_variables sigma in
```

I don't think it's actually needed at all ;)

it was introduced in coq/coq@1e389def84cc3eafc8aa5d1a1505f078a58234bd which did

```
- let c = drop_extra_implicit_args (Evarutil.nf_evar sigma c) in
+ let sigma, subst = Evd.nf_univ_variables sigma in
+ let c = Vars.subst_univs_constr subst (Evarutil.nf_evar sigma c) in
+ let c = drop_extra_implicit_args c in
```

maybe nf_evar didn't normalize universe variables back then? IDK

Well, that would be a nice speedup.. at least in our proofs

https://github.com/coq/coq/pull/18211

@Janno does that PR give a speedup in your code? our bench doesn't show any perf change AFAICT

I haven't gotten around to patching everything and rebuilding from scratch. I don't really see how it could not give a speedup, though, since the result of the normalization is discarded. There shouldn't be any slowdown in other places from not doing it.

Last updated: Oct 13 2024 at 01:02 UTC