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.
What takes time? Hint application per se, or exponential blowup in rewriting?
Hmm, how can I check that? I've just used
time to measure the time it takes to do autorewrite
Can you give pointers to the rewrite rules and to a line that is slow?
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
in principle, you could try passing the hints to
... but rewrite_strat uses a totally different algorithm from autorewrite
I only knew that there are issues because you must explicitly do some reductions...
_actually_, I now seem to see that this uses setoid rewriting
These are calls to setoid_rewrite, right?
Set Typeclasses Debug, but sadly setoid rewriting easily gets unreasonably slow in _manual_ uses
even after you use all the semi-documented tricks to speed it up, like declaring
Params instances etc.
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
the vanilla rewrite tactic (and also ssreflect’s one) use the setoid rewriting machinery anyway
(the Coq bug tracker has multiple issues from Iris devs on setoid rewriting performance)
ssr's rewrite is reasonably fast/predictable but does not go under binders.
separately, there are multiple other issues on the performance and functionality of autorewrite, rewrite_strat etc.
ssr’s rewrite isn’t necessarily reasonably fast anymore, when used with setoid rewriting
these tactics are weirdly named, BTW
all rewrite tactics hook into setoids.
rewrite_strat) go under binders
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
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
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.
(OTOH Iris uses almost exclusively ssreflect rewrite with setoids)
ah, didn’t know.
but if you use non-trivial setoids (as in ssreflect), you’ll still rely on typeclass search for Proper lemmas
(which, again, AFAIK won’t work with CS)
and that typeclass search is what is very happy to diverge
(I’ve witnessed it myself and heard Robbert complain; I’ve stolen some of his tricks to improve things)
@Irene Yoon one helpful thing is declaring
Params instances: https://gitlab.mpi-sws.org/iris/stdpp/blob/005887ee4cd20b48f85c4e6811e41731d2656f83/theories/base.v#L235-238
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.
The script above does
cbn; rauto so I've no clue if it is a monster thing, or not.
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.
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
@Enrico Tassi does that
Opaque or not?
@Irene Yoon looking at your main theorem, I’d fear very long
Qed times... I’d consider searching for a way to split it
@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).
right, locking gives a more robust sealing — which IIRC you can also use in definitions
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
f is still convertible to its body, which affects both some tactics and the typechecking in the kernel)
@Paolo Giarrusso The
Params trick worked beautifully! It's still slow, but not excruciatingly slow anymore. Thanks
Sort of tangential, but is there something like
info_autothat I can use for
Set Info Auto also doesn't seem to give me anything when doing
Last updated: Sep 26 2023 at 13:01 UTC