leanprover-community / leanprover-community/lean
Elan download of Windows Nightly fails
Nobody has claimed this yet.
- Dominant language
- C++
- Stars
- 433
- Forks
- 79
- PR merge metrics
- No merged PRs in 30d
Description
Prerequisites
- [x ] Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
- Specifically, check out the wishlist, open RFCs,
or feature requests.
- Specifically, check out the wishlist, open RFCs,
- Reduced the issue to a self-contained, reproducible test case.
- Checked that your issue isn't already filed.
Description
Dowloading Lean Nightly on a Windows machine fails.
Steps to Reproduce
curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf \| sh info: downloading installer Archive: elan-init.zip inflating: elan-init.exe Welcome to Lean! This will download and install Elan, a tool for managing different Lean versions used in packages you create or download. It will also install a default version of Lean and its package manager, leanpkg, for editing files not belonging to any package. It will add the leanpkg, lean, and elan commands to Elan's bin directory, located at: C:\Users\sulli\.elan\bin This path will then be added to your PATH environment variable by modifying the HKEY_CURRENT_USER/Environment/PATH registry key. You can uninstall at any time with elan self uninstall and these changes will be reverted. Current installation options: default toolchain: stable modify PATH variable: yes 1) Proceed with installation (default) 2) Customize installation 3) Cancel installation 2 I'm going to ask you the value of each these installation options. You may simply press the Enter key to leave unchanged. Default toolchain? (stable/nightly/none) nightly Modify PATH variable? (y/n) y Current installation options: default toolchain: nightly modify PATH variable: yes 1) Proceed with installation (default) 2) Customize installation 3) Cancel installation 1 info: syncing channel updates for 'nightly' info: latest update on nightly, lean version nightly-2019-11-01 info: downloading component 'lean' error: binary package was not provided for 'windows' Press the Enter key to continue.
--
Expected behavior: Proper install
**Actual behavior:**fails
Reproduces how often: Student notified me, I tried it, saw same failure behavior.
Versions
You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.
3.4.2 nightly. Windows OS.
Additional Information
Any additional information, configuration or data that might be necessary to reproduce the issue.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Reproduce the failure with the curl ... elan-init.sh command on Windows, using the nightly toolchain option shown in the report. Start by tracing the installer and nightly download path; done means the Windows nightly binary package is provided and the installation completes successfully.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- shell
- Domain
- cli
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 25/100