Irene Yoon (Sep 24 2020 at 17:12): 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.
Pierre-Marie Pédrot (Sep 24 2020 at 17:13):What takes time? Hint application per se, or exponential blowup in rewriting?
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
Enrico Tassi (Sep 24 2020 at 17:25):Can you give pointers to the rewrite rules and to a line that is slow?
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
Paolo Giarrusso (Sep 24 2020 at 17:40):in principle, you could try passing the hints to rewrite_strat
Pierre-Marie Pédrot (Sep 24 2020 at 17:41):... but rewrite_strat uses a totally different algorithm from autorewrite
Paolo Giarrusso (Sep 24 2020 at 17:42):I only knew that there are issues because you must explicitly do some reductions...
Paolo Giarrusso (Sep 24 2020 at 17:42):_actually_, I now seem to see that this uses setoid rewriting
Enrico Tassi (Sep 24 2020 at 17:43):These are calls to setoid_rewrite, right?
Paolo Giarrusso (Sep 24 2020 at 17:44):there’s Set Typeclasses Debug, but sadly setoid rewriting easily gets unreasonably slow in _manual_ uses
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.
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
Paolo Giarrusso (Sep 24 2020 at 17:45):the vanilla rewrite tactic (and also ssreflect’s one) use the setoid rewriting machinery anyway
Paolo Giarrusso (Sep 24 2020 at 17:46):(the Coq bug tracker has multiple issues from Iris devs on setoid rewriting performance)
Enrico Tassi (Sep 24 2020 at 17:46):ssr's rewrite is reasonably fast/predictable but does not go under binders.
Paolo Giarrusso (Sep 24 2020 at 17:46):separately, there are multiple other issues on the performance and functionality of autorewrite, rewrite_strat etc.
Paolo Giarrusso (Sep 24 2020 at 17:47):ssr’s rewrite isn’t necessarily reasonably fast anymore, when used with setoid rewriting
Paolo Giarrusso (Sep 24 2020 at 17:47):these tactics are weirdly named, BTW
Paolo Giarrusso (Sep 24 2020 at 17:47):all rewrite tactics hook into setoids.
Paolo Giarrusso (Sep 24 2020 at 17:48):but only setoid_rewrite (and rewrite_strat) go under binders
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
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
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.
Paolo Giarrusso (Sep 24 2020 at 17:50):(OTOH Iris uses almost exclusively ssreflect rewrite with setoids)
Paolo Giarrusso (Sep 24 2020 at 17:50):ah, didn’t know.
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
Enrico Tassi (Sep 24 2020 at 17:51):indeed
Paolo Giarrusso (Sep 24 2020 at 17:51):(which, again, AFAIK won’t work with CS)
Paolo Giarrusso (Sep 24 2020 at 17:51):and that typeclass search is what is very happy to diverge
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)
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
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.
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.
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.
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
Paolo Giarrusso (Sep 24 2020 at 17:56):@Enrico Tassi does that rewrite respect Opaque or not?
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
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).
Paolo Giarrusso (Sep 24 2020 at 18:09):right, locking gives a more robust sealing — which IIRC you can also use in definitions
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)
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
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: Oct 12 2024 at 13:01 UTC