Manage all toolchain dependencies hermetically
- 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
Assessment
This issue has not been assessed yet.