Stream: Coq users

Topic: Performance of set (x := ..) in *

view this post on Zulip Armaël Guéneau (Feb 01 2021 at 21:20):

I'm trying to profile a tactic in which invocations to set (x := ..) in * are responsible for a good portion of the running time. Is there a faster version of this tactic somewhere that I should use instead, or is what I'm trying to do intrinsically expensive?

view this post on Zulip Jason Gross (Feb 03 2021 at 13:11):

set is modulo conversion, see also and (there's a fast_set in the next comment in You can speed things up by replacing set with pose and change

view this post on Zulip Armaël Guéneau (Feb 04 2021 at 11:13):

Thanks a lot! I'm testing your fast_set right now, it looks like it should be a lot better already.
You mention in the issue that an Ltac2 implementation might be even more efficient; if you have such an implementation then I'd also be interested :-).

Last updated: Jun 20 2024 at 13:02 UTC