Jason Gross (Aug 29 2022 at 03:42): Jason Gross (Aug 29 2022 at 03:42):Any ideas for how to performance-debug the additional 30 seconds added by translating ~110 loc from Ltac to Ltac2 at https://github.com/mit-plv/fiat-crypto/pull/1361/commits/2fa728620a50dd2b4448d23fb16e13c9451e006e ? (Build target make TIMED=1 SKIP_BEDROCK2=1 pre-standalone in fiat-crypto)
My current guess is that it's the overhead introduced by the four extra evars involved in replacing
lazymatch ty with
| base_interp ?T => T
| @base.interp base base_interp (@base.type.type_base base ?T) => T
| @type.interp (base.type base) (@base.interp base base_interp) (@Compilers.type.base (base.type base) (@base.type.type_base base ?T)) => T
with
(* work around COQBUG(https://github.com/coq/coq/issues/13962) *)
lazy_match! '($base_interp, $base, $ty) with
| (?base_interp, ?base, ?base_interp ?t) => Some t
| (?base_interp, ?base, @base.interp ?base ?base_interp (@base.type.type_base ?base ?t)) => Some t
| (?base_interp, ?base, @type.interp (base.type ?base) (@base.interp ?base ?base_interp) (@Compilers.type.base (base.type ?base) (@base.type.type_base ?base ?t))) => Some t
but I'm not sure how to go about debugging these issues systematically
Last updated: Oct 08 2024 at 14:01 UTC