ITADN

Ship pre-built Aeneas Lean library

#3233Closedjoshlf 创建于 2026-04-10
J
joshlfcommented
Currently, generated Lean depends on Aeneas's Lean library by source (specifically, the dependency is on Aeneas's GitHub repo at a pinned commit hash). This causes a number of problems, all of which would be solved if we instead distributed a pre-built artifact: - Increases Lean build times during verification - Increases cache complexity (ie, increases the complexity required to reason about *what* artifacts are cached) - Causes output noise during the build, some of which we have [logic](https://github.com/google/zerocopy/blob/9b8b49e742d51c7cdb8194375b17fc5ab56cab79/hermes/src/aeneas.rs#L452) to [redact](https://github.com/google/zerocopy/blob/9b8b49e742d51c7cdb8194375b17fc5ab56cab79/hermes/src/aeneas.rs#L474) - Increases the complexity of our local development and CI infrastructure (by requiring fancy caching in order to avoid the performance impact of needing to constantly re-build) - Increases performance tax of local development and CI when caches haven't been populated or when the cache isn't used ## Progress - [ ] https://github.com/AeneasVerif/aeneas/pull/921 - [ ] Consume in Hermes
关闭于 2026-04-12 0 条评论