Jason Gross (Aug 27 2022 at 06:32): 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 https://github.com/coq/coq/issues/16412) that it's essentially impossible to debug performance regressions introduced by porting to Ltac2.
Last updated: Oct 08 2024 at 14:01 UTC