Stream: Coq devs & plugin devs

Topic: Very slow algorithmic in Ssreflect rewrite

Pierre-Marie Pédrot (Mar 10 2022 at 14:44):

I've discovered a critical source of slowness in metacoq that comes from the ssr rewrite implementation, but I am not sure I fully understand the code so I am publicly asking for help. (@Enrico Tassi maybe?)

Pierre-Marie Pédrot (Mar 10 2022 at 14:44):

The issue is visible in https://github.com/coq/coq/pull/15782.

Pierre-Marie Pédrot (Mar 10 2022 at 14:45):

In rwprocess_rule we compute multirewrite rules by extraction from a proof p : T where T is recursively built out of equalities, products and functions.

Enrico Tassi (Mar 10 2022 at 14:45):

indeed

Pierre-Marie Pédrot (Mar 10 2022 at 14:45):

When T ≡ A × B we compute the projections of p, but there is a "fast path" when p is already a pair

Pierre-Marie Pédrot (Mar 10 2022 at 14:46):

but for some reason, we simpl the hell out of it when trying to check whether it's a pair

Pierre-Marie Pédrot (Mar 10 2022 at 14:46):

(in master, we do it even twice)

Pierre-Marie Pédrot (Mar 10 2022 at 14:46):

in the PR we only simpl it once and share the result

Pierre-Marie Pédrot (Mar 10 2022 at 14:47):

but even there it's horribly slow because we're normalizing huge proofs

Enrico Tassi (Mar 10 2022 at 14:47):

Where are the huge proofs? in A or B ????

Pierre-Marie Pédrot (Mar 10 2022 at 14:47):

since it's recursive you pay the price of normalization at every recursive step

Pierre-Marie Pédrot (Mar 10 2022 at 14:47):

it's p

Pierre-Marie Pédrot (Mar 10 2022 at 14:47):

we normalize the proof not the type

Pierre-Marie Pédrot (Mar 10 2022 at 14:48):

I tried not normalizing and always rebuilding projections but it breaks mathcomp

Pierre-Marie Pédrot (Mar 10 2022 at 14:48):

(line 576 in the PR)

Pierre-Marie Pédrot (Mar 10 2022 at 14:49):

1. is it normal to normalize proofs and 2. why does mathcomp care about the shape of the proof?

Enrico Tassi (Mar 10 2022 at 14:49):

This line? let sr sigma = match EConstr.kind sigma (Tacred.hnf_constr env sigma r) with ?

Pierre-Marie Pédrot (Mar 10 2022 at 14:49):

yup

Pierre-Marie Pédrot (Mar 10 2022 at 14:49):

(see the PR for a slightly more readable variant)

Enrico Tassi (Mar 10 2022 at 14:50):

Maybe I know, but it is very subtle

Pierre-Marie Pédrot (Mar 10 2022 at 14:50):

I am all ears

Pierre-Marie Pédrot (Mar 10 2022 at 14:51):

(this is terrible algorithmically if you have many nested pairs regardless of the cost of simpl)

Enrico Tassi (Mar 10 2022 at 14:54):

Imagine r = (thm1, thm2) : T = (forall x, x = 1) * (forall x, x = 2), then the proof term would be, say, projT2 r a for some a in the goal. That is the easy case. Now, one may have defined r as Definition r x y := (thm1 x, thm2 y). So T = forall x y, (x = 1) * (y = 2). In this case the proof term is projT2 (r a _) for unresolved _. But if you reduce you prune the offending _.

Pierre-Marie Pédrot (Mar 10 2022 at 14:55):

I see...

Pierre-Marie Pédrot (Mar 10 2022 at 14:55):

but this is a heuristic, simpl might not be enough to get rid of the dependency

Enrico Tassi (Mar 10 2022 at 14:56):

I think the right fix is to "distribute" binders, but it all comes down to the poor man implementation of "rewrite databases"

Pierre-Marie Pédrot (Mar 10 2022 at 14:57):

so, one δ unfolding should be considered enough a long as there are leading products or something?

Enrico Tassi (Mar 10 2022 at 14:57):

in some sense you have to reduce all projT

Enrico Tassi (Mar 10 2022 at 14:58):

why isn't lazy the right chooice here??

Pierre-Marie Pédrot (Mar 10 2022 at 14:58):

that's one thing I am wondering

Pierre-Marie Pédrot (Mar 10 2022 at 14:58):

(at least in its whd variant)

Pierre-Marie Pédrot (Mar 10 2022 at 14:58):

if the only thing we care about is the head of the term...

Enrico Tassi (Mar 10 2022 at 14:59):

yes, weak head call by need

Pierre-Marie Pédrot (Mar 10 2022 at 14:59):

I'll try that to see if it works any better (and is more efficient)

Pierre-Marie Pédrot (Mar 10 2022 at 16:05):

mathcomp seems to be happy with whd-lazy

Maxime Dénès (Mar 10 2022 at 17:46):

and is it more efficient? :)

Maxime Dénès (Mar 10 2022 at 17:46):

(I hope so)

Pierre-Marie Pédrot (Mar 10 2022 at 17:57):

I can't test right now on the bench because metacoq doesn't compile

Pierre-Marie Pédrot (Mar 10 2022 at 17:57):

but locally it does seem so

Pierre-Marie Pédrot (Mar 10 2022 at 17:57):

(this hotspot was responsible for 90% of the time in some parts)

Enrico Tassi (Mar 10 2022 at 20:29):

opam package for metacoq fixed and merged

Last updated: Dec 07 2023 at 09:01 UTC