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 to redact
- 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
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:
Progress