Stop treating user-global directory as writeable; cache build artifacts
- Dominant language
- Rust
- Stars
- 2.6k
- Forks
- 179
- Avg merge
- 1d 19h
- Merged PRs (30d)
- 29
Description
- [x] https://github.com/google/zerocopy/pull/3304
- **NOTE**: This deletes the `setup_repair` test in preparation for future changes, leaving `setup`'s repair logic untested
- [x] Update `setup` to initialize git repo in Aeneas Lean library
- [x] Update `setup` to `lake build` with `LAKE_CACHE_DIR` and `LAKE_ARTIFACT_CACHE=1`
- [x] Update `generate`/`verify` to generate a local-filesystem git dep on the Aeneas Lean library
- [x] Update `generate`/`verify` to set `LAKE_CACHE_DIR` when running `lake build`
- [x] Investigate whether the prior work allows us to remove the worker pool/cache pool infra from integration tests
- https://github.com/google/zerocopy/pull/3305
- [x] Update `setup` to clone Mathlib into the toolchain directory and rewrite Aeneas's dep to be a local-filesystem git dep. Do this recursively for Mathlib's deps
- https://github.com/google/zerocopy/pull/3306
- [ ] Do as much of this as possible while building the .zst artifact
- [ ] Add extensive comments to explain all design decisions; refactor code so relevant tricky bits of logic all live together if necessary
Contributor guide
Assessment
This issue has not been assessed yet.