google / google/zerocopy

Manage all toolchain dependencies hermetically

Open
#3,331 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

*Co-authored with @mdittmer*

Design goals:
- Once you run `cargo anneal setup` successfully, it should be possible to work with Anneal entirely offline
- If a `~/.anneal/toolchain/` directory exists, it is fully and successfully installed; checking that directory's existence is sufficient to ensure that everything is setup correctly

Currently, the `setup` command and various "runtime" commands (`expand`, `generate`, `verify`) do a messy combination of using tools we've installed and managed in `~/.anneal` and falling back to the user's `PATH`. This results in surprising behavior which can differ across machines, differ as users make seemingly unrelated configuration changes, etc.

Instead, we should move to a world in which Anneal unambiguously manages everything in a hermetic manner. If we want to relax this policy later to allow users to opt into using non-managed toolchains, we can do that, but hermeticity should be the default. Concretely:
- [ ] Create a shared Rust uility for installing and running subcommands. This utility should not propagate the current process's `PATH` at all, instead constructing a new one from scratch. The new `PATH` should *only* include paths inside of `~/.anneal`
- [ ] Pin a *specific* version of `elan` in `Cargo.toml` and hash its version in order to determine the toolchain directory's unique slug
- [ ] During `setup`, download this version of `elan` and then use it to download the pinned Lean toolchain
- Note: This has the effect of having each `elan` install only manage a single Lean install. It's somewhat redundant, but ensures that we always use the blessed path for managing Lean toolchains.

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.