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