Stream: Coq users

Topic: Slow `autorewrite` Hint Databases


view this post on Zulip Irene Yoon (Sep 24 2020 at 17:12):

I have around ~20 rewrite lemmas in a hint database, and trying to use autorewrite with this database seems unreasonably slow (~6 seconds). (All of the lemmas are used pretty evenly, as far as I can tell.) Does anyone have any tips on how improve this slowness? I tried splitting the lemmas to more hint databases, but it feels cumbersome to do autorewrite with a database with only 5 lemmas, and I'm not familiar with other things I could do with hint rewrite databases.

view this post on Zulip Pierre-Marie Pédrot (Sep 24 2020 at 17:13):

What takes time? Hint application per se, or exponential blowup in rewriting?

view this post on Zulip Irene Yoon (Sep 24 2020 at 17:19):

Hmm, how can I check that? I've just used time to measure the time it takes to do autorewrite

view this post on Zulip Enrico Tassi (Sep 24 2020 at 17:25):

Can you give pointers to the rewrite rules and to a line that is slow?

view this post on Zulip Irene Yoon (Sep 24 2020 at 17:36):

The rewrite rules are on here (for now, I separated the lemmas to separate databases) : (https://github.com/vzaliva/helix/blob/9fe6a72a4589b57c08f86ff366c7fc3a45a5276d/coq/LLVMGen/Correctness_Prelude.v#L729), and here's an example of a slow instance (https://github.com/vzaliva/helix/blob/9fe6a72a4589b57c08f86ff366c7fc3a45a5276d/coq/LLVMGen/Correctness_AExpr.v#L316)

It's a bit of a hunky codebase, is there a way to get some debug trace for autorewrite? I attempted looking at the Coq buffer but couldn't find much useful information from it

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:40):

in principle, you could try passing the hints to rewrite_strat

view this post on Zulip Pierre-Marie Pédrot (Sep 24 2020 at 17:41):

... but rewrite_strat uses a totally different algorithm from autorewrite

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:42):

I only knew that there are issues because you must explicitly do some reductions...

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:42):

_actually_, I now seem to see that this uses setoid rewriting

view this post on Zulip Enrico Tassi (Sep 24 2020 at 17:43):

These are calls to setoid_rewrite, right?

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:44):

there’s Set Typeclasses Debug, but sadly setoid rewriting easily gets unreasonably slow in _manual_ uses

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:44):

even after you use all the semi-documented tricks to speed it up, like declaring Params instances etc.

view this post on Zulip Irene Yoon (Sep 24 2020 at 17:45):

Yes, I've been using setoid_rewrite especially because I'm using a custom equality here for the rewrite, and vanilla rewrite doesn't seem to work for some of the cases

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:45):

the vanilla rewrite tactic (and also ssreflect’s one) use the setoid rewriting machinery anyway

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:46):

(the Coq bug tracker has multiple issues from Iris devs on setoid rewriting performance)

view this post on Zulip Enrico Tassi (Sep 24 2020 at 17:46):

ssr's rewrite is reasonably fast/predictable but does not go under binders.

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:46):

separately, there are multiple other issues on the performance and functionality of autorewrite, rewrite_strat etc.

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:47):

ssr’s rewrite isn’t necessarily reasonably fast anymore, when used with setoid rewriting

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:47):

these tactics are weirdly named, BTW

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:47):

all rewrite tactics hook into setoids.

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:48):

but only setoid_rewrite (and rewrite_strat) go under binders

view this post on Zulip Enrico Tassi (Sep 24 2020 at 17:48):

It does not support Hint Dbs, but you can still use multi rules https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#multi-rule-rewriting

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:49):

and BTW — “ssreflect rewrite uses setoid rewriting” is true but confusing, since setoid rewriting uses typeclasses which don’t use evarconv, so it wouldn’t really mix with mathcomp-style developments

view this post on Zulip Enrico Tassi (Sep 24 2020 at 17:50):

ssr's rewrite uses keyd matching to identify where the replacement has to occur, then it calls setoid_rewriting using a laser-pointer. This phase is, to my knowledge, faster than the standard one that is not driven by a key symbol, but that is free to unfold here and there.

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:50):

(OTOH Iris uses almost exclusively ssreflect rewrite with setoids)

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:50):

ah, didn’t know.

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:51):

but if you use non-trivial setoids (as in ssreflect), you’ll still rely on typeclass search for Proper lemmas

view this post on Zulip Enrico Tassi (Sep 24 2020 at 17:51):

indeed

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:51):

(which, again, AFAIK won’t work with CS)

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:51):

and that typeclass search is what is very happy to diverge

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:52):

(I’ve witnessed it myself and heard Robbert complain; I’ve stolen some of his tricks to improve things)

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:53):

@Irene Yoon one helpful thing is declaring Params instances: https://gitlab.mpi-sws.org/iris/stdpp/blob/005887ee4cd20b48f85c4e6811e41731d2656f83/theories/base.v#L235-238

view this post on Zulip Enrico Tassi (Sep 24 2020 at 17:53):

yes. if it is the TC search that is slow, ssr rewrite can't help. if it is the search for the LHS of the rule which is expensive (eg you goal contains large terms that unfold), than ssr can help a little.

view this post on Zulip Enrico Tassi (Sep 24 2020 at 17:54):

The script above does cbn; rauto so I've no clue if it is a monster thing, or not.

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:54):

in fact, that comment is slightly inaccurate — you want a Params instance for each function that you declare Proper. Not sure what to do if you have Proper instances with conflicting arities.

view this post on Zulip Irene Yoon (Sep 24 2020 at 17:55):

Ah neat, thanks! I'll check Params. Yeah the script as of right now is a bit of a monster in various respects... I'll try looking at the Typeclasses search and see if ssr will be useful

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:56):

@Enrico Tassi does that rewrite respect Opaque or not?

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:58):

@Irene Yoon looking at your main theorem, I’d fear very long Qed times... I’d consider searching for a way to split it

view this post on Zulip Enrico Tassi (Sep 24 2020 at 18:03):

@Paolo Giarrusso I think it does not. It is reasonably common to rewrite [symbol]lock some_rule -lock in order to "opacify" a symbol temporarily. Also keyd matching and user provided patterns are usually enough to be precise (skip the thing you don't want).

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 18:09):

right, locking gives a more robust sealing — which IIRC you can also use in definitions

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 18:14):

I mention this because @Irene Yoon’s script has some Opaque calls, and when discussing performance Opaque is dangerous (unless you already know that after Opaque f, f is still convertible to its body, which affects both some tactics and the typechecking in the kernel)

view this post on Zulip Irene Yoon (Sep 25 2020 at 15:07):

@Paolo Giarrusso The Params trick worked beautifully! It's still slow, but not excruciatingly slow anymore. Thanks

view this post on Zulip Irene Yoon (Sep 26 2020 at 05:48):

Sort of tangential, but is there something like info_autothat I can use for autorewrite? (Set Info Auto also doesn't seem to give me anything when doing autorewrite)


Last updated: Feb 06 2023 at 13:03 UTC