Stream: Ltac2

Topic: incremental porting of Ltac1 code?

view this post on Zulip Jason Gross (Aug 27 2022 at 06:32):

Is there a story for incremental porting of performance-critical Ltac1 code? The overhead of switching between Ltac1 and Ltac2 is so high (see that it's essentially impossible to debug performance regressions introduced by porting to Ltac2.

Last updated: Jan 31 2023 at 09:01 UTC