elan
elan copied to clipboard
leanprover
The Lean version manager
``` $ elan self update ~ info: checking for self-updates info: downloading self-update error: failed to set permissions for '/Users/ncihnegn/.elan/bin/elan-init' info: caused by: No such file or directory (os error...
Currently, lake/leanpkg doesn't reuse toolchain versions. ## How to reproduce 1. `elan default leanprover/lean4:nightly` 2. `lake init foo` which produce `lean-toolchain` with `4.0.0-nightly-2022-07-19` (which is the same version already installed)...
I figured out that I needed a windows friendly version of perl from https://strawberryperl.com/ because the one in "c:\Program Files\Git\usr\bin\perl.exe" doesn't work for some reason. So the openssl configure steps...
1. Lock the lean.exe by running it in VS Code 2. run `elan toolchain uninstall leanprover/lean4:nightly` to try and remove that version **Actual**: it fails to remove the locked file...
Hi! On Linux, elan stores files in `~/.elan`. It may be better to follow the [XDG desktop specification](https://specifications.freedesktop.org/basedir-spec/basedir-spec-latest.html). In particular, Configuration files should go under `$XDG_CONFIG_HOME` (if empty, `$HOME/.config/`) Data...
`$ elan default stable` returns ```bash info: syncing channel updates for 'stable' thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value: Error { description: "Failure when receiving data from...
It would be very useful if `elan toolchain list` also reported the path that a "linked" toolchain is pointing to. For example, today I get this output: ``` stable (default)...
The `elan-init.sh` script doesn't work as I would have expected when run inside `msys2`. It installs everything (and sets up the PATH) in the Windows home directory `C:\Users\scott\.elan`, rather than...
Suggested plan: * Inject a `leanpkg lean-upgrade ` command into `leanpkg` (i.e. it will only be available when calling `~/.elan/bin/leanpkg`). This is not just a convenience command for editing the...
We should copy stack's [script command](https://docs.haskellstack.org/en/stable/GUIDE/#script-interpreter) to extend isolation to standalone files and gists.