elan
elan copied to clipboard
leanprover
The Lean version manager
On Windows 11, running inside Parallels on Apple Silicon (perhaps an unusual combination): Running ``` curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1 powershell -ExecutionPolicy Bypass -f elan-init.ps1 del elan-init.ps1 ``` in a Windows...
``` % elan toolchain install leanprover/lean4:v4.0.0 % rm -rf ~/.elan/toolchains/leanprover--lean4---v4.0.0 % lake +leanprover/lean4:v4.0.0 env error: toolchain 'leanprover/lean4:v4.0.0' is not installed % elan toolchain install leanprover/lean4:v4.0.0 leanprover/lean4:v4.0.0 unchanged - (toolchain not...
When I run `elan self update`, the following error occurs: ``` $ elan self update ←[1minfo: ←[0mchecking for self-updates ←[31m←[1merror: ←[0mcould not create link from 'C:\Users\pwintz\.elan\bin\elan.exe' to 'C:\Users\pwintz\.elan\bin\lake.exe' ``` Any...
`src/elan-cli/download_tracker.rs` messed up the download progress. There are messages all over the screen. I see that it says: ```rust // delete_line() doesn't seem to clear the line properly. // Instead,...
On PS v4 or below `Expand-Archive` is unavailable, so the install script fails. This seems to work (I haven't tested this intensively): ```powershell Add-Type -assembly "system.io.compression.filesystem" [System.IO.Compression.ZipFile]::ExtractToDirectory("$_dir/elan-init.zip", "$_dir") ```
**Issue Description:** While attempting to run elan-init.exe, I encountered a crash scenario. Specifically, upon running the program, the command prompt window disappears immediately, and I'm unable to obtain any error...
See this shell session: ```shell $ elan toolchain list leanprover/lean4:v4.13.0-rc3 leanprover/lean4:v4.8.0-rc2 $ elan toolchain link oh--no--anyway ~/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/ $ elan toolchain list error: invalid toolchain name: 'oh/no/anyway' ``` Some motivation for...
related: #99 Currently, the remote toolchain reference feature on GitHub does not support repositories with underscores in their names. This limitation affects repositories like `leanprover-community/mathematics_in_lean`.
I'm trying to build 'elan' on macOS Sequoia and ran into an issue with float16 building OpenSSL. ``` % rustup update stable info: syncing channel updates for 'stable-x86_64-apple-darwin' stable-x86_64-apple-darwin unchanged...
