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/<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:
Co-authored with @mdittmer
Design goals:
cargo anneal setupsuccessfully, it should be possible to work with Anneal entirely offline~/.anneal/toolchain/<toolchain>directory exists, it is fully and successfully installed; checking that directory's existence is sufficient to ensure that everything is setup correctlyCurrently, the
setupcommand and various "runtime" commands (expand,generate,verify) do a messy combination of using tools we've installed and managed in~/.annealand falling back to the user'sPATH. 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:
PATHat all, instead constructing a new one from scratch. The newPATHshould only include paths inside of~/.annealelaninCargo.tomland hash its version in order to determine the toolchain directory's unique slugsetup, download this version ofelanand then use it to download the pinned Lean toolchainelaninstall only manage a single Lean install. It's somewhat redundant, but ensures that we always use the blessed path for managing Lean toolchains.