leanprover-community / leanprover-community/lean

Elan download of Windows Nightly fails

Open
#98 1 comment 0 reactions 0 assignees View on GitHub

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.
    • Reduced the issue to a self-contained, reproducible test case.
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

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.