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 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: Jan 31 2023 at 09:01 UTC