The release of 4.27.0 has brought with it the stabilisation of the Lean module system, bringing benefits to build times and binary size. Given that projects using Lampe can get quite large with some extremely complex proofs and definitions, it might be worth exploring the use of the module system here.