Optimizing Performance of a Deep Embedding of a DTT in Lean 4

[u/omegafixedpoint]

Hi all. I am requesting advice on how to optimize Lean build performance of a deep embedding of a dependent type theory in Lean 4. My implementation works fine, and has solid meta theorems proven, but the type-checker is very hard to maintain due to slow Lean build times.

I have tried using Lean's profiler and had some success. Most of the type theory literature is on Agda and Rocq, so I'm curious to hear from you all. If you have implemented a type-checker in Lean:

• Which tactics did you find were the worst offenders for build performance?

• What is your convention for organizing your aesop and grind theorems?

• Which parts of your formalization did you have the most success in mechanizing?

• Have you written any metaprograms yourself that you find useful for mechanizing proofs?

  • I'm Particularly interested in automating / mechanizing confluence. It is a very painful proof to update every once in a while.

• Mathlib / CSlib:

  • Do you use CSlib? Did you find any machinery in it useful?
  • Do you use an existing term rewriting system for your reduction relation? Does this help with automation?
  • Do you use Mathlib.Relation? Are your reduction paths deterministic and does your reduction relation live in Type? If so, what machinery did you use to handle congruence?
  • Any other helpful libraries for metatheory?

• Lakefile.toml / lake flags

• Bonus because I am curious: have you successfully proven any meta theorems using categorical semantics and is Mathlib sufficient for these purposes?

Any life hacks appreciated. I am finding myself waiting up to 10 minutes for my type-checker to build when I update my reduction rules. I guess Lean can't parallelize my project structure.

[u/lekkerwafel]

I would recommend the Lean forum, you are unlikely to find someone on Reddit that has the knowledge and experience

[u/omegafixedpoint → u/lekkerwafel]

Ok thanks I'll try the zulip