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 https://github.com/coq/coq/issues/4636 and https://github.com/coq/coq/issues/13788#issuecomment-767217443 (there's a fast_set in the next comment in https://github.com/coq/coq/issues/13788#issuecomment-767217670). 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: Feb 06 2023 at 12:04 UTC