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?
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
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