google / google/zerocopy

Stop treating user-global directory as writeable; cache build artifacts

Open
#3,303 0 comments 0 reactions 0 assignees View on GitHub
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.