Ship pre-built Aeneas Lean library
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 条评论