Stream: Ltac2

Topic: performance diffing Ltac2 vs Ltac

view this post on Zulip 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 ? (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


(* work around COQBUG( *)
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: Jun 10 2023 at 06:31 UTC