Armaël Guéneau (Feb 01 2021 at 21:20): 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?
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
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: Oct 04 2023 at 20:01 UTC