quickstart instructions; where to file issues?

Stream: lean4

[Scott Morrison]

The Lean4 quickstart instructions don't seem to be working on a freshly installed VSCode on a fresh Windows 10 machine. After installing the lean4 extension, upon creating a new .lean file, and being prompted to click a button to install elan, I receive the following error message on the command line:

PS C:\Users\kim> Start-BitsTransfer -Source "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1" -Destination "elan-init.ps1"
PS C:\Users\kim> Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope Process
PS C:\Users\kim> $rc = .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain leanprover/lean4:nightly
info: downloading installer to C:\Users\kim\AppData\Local\Temp\
Elan failed with error code -1073741515
PS C:\Users\kim> Write-Host "elan-init returned [$rc]"
elan-init returned [1]
PS C:\Users\kim> del .\elan-init.ps1
PS C:\Users\kim> if ($rc -ne 0) {
>>     Read-Host -Prompt "Press ENTER to continue"
>> }
Press ENTER to continue:

I am not at all a Windows user, so I'm not sure if the right diagnosis here is:

1. There is a problem in the VSCode extension, and it doing something wrong trying to run elan-init.
2. There is a problem in elan-init on a bare Windows 10 machine.
3. There are other prerequisites, and the quickstart instructions need updating.
4. EBKAC.

[Scott Morrison]

Following the elan installation instructions for Windows results in

C:\Users\kim>powershell -f elan-init.ps1
File C:\Users\kim\elan-init.ps1 cannot be loaded because running scripts is disabled on this system. For more
information, see about_Execution_Policies at https:/go.microsoft.com/fwlink/?LinkID=135170.
    + CategoryInfo          : SecurityError: (:) [], ParentContainsErrorRecordException
    + FullyQualifiedErrorId : UnauthorizedAccess

I've reported this as https://github.com/leanprover/elan/issues/96.

[Scott Morrison]

Does anyone have preferences for which way to take installation instructions next, given these failures?

[Scott Morrison]

/poll What instructions to give Windows users?

[Scott Morrison]

(git bash was what we've previously told people to do for Lean3, but I don't know enough about windows to know if this is still the simplest path)

[Sebastian Ullrich]

The first log looks like an issue in elan itself (that unfortunately it doesn't tell us much about), not with Powershell

[Scott Morrison]

I guess I can give slightly more information: before it fails, a blue banner briefly appears over the top half of the shell (who designed this stuff?!?) first saying BITS Transfer with a progress bar, and then saying Expand-Archive (but disappears too quickly to read the rest).

[Scott Morrison]

Very happy to try stuff out on this fresh machine, but I really do not know Windows/Powershell.

[Scott Morrison]

Okay, trying something different now. I installed git for windows, and in a new git bash window ran

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

This results in:

info: downloading installer
Archive:  elan-init.zip
  inflating: elan-init.exe

but no further action before being returned to the git bash prompt, with no sign of a elan-init.zip or elan-init.exe in any directory I know to look in...

[Sebastian Ullrich]

Can you run that script again with sh -x?

[Sebastian Ullrich]

I would not be surprised if it's failing in elan again

[Scott Morrison]

Here's the output with sh -x.

[Scott Morrison]

I guess that is just elan-init.exe failing with error code 127.

[Sebastian Ullrich]

Yes, presumably same issue, again without error message

[Scott Morrison]

Ahha! Exiting git bash and running elan-init.exe on the regular windows command line produces:
Screen-Shot-2023-06-09-at-10.06.08-pm.png

[Scott Morrison]

I guess this is something that doesn't come with a fresh windows, but is so fundamental that no normal person would be without? :-)

[Scott Morrison]

It wasn't installed by either VSCode or git for windows, however.

[Scott Morrison]

Or if it was installed, isn't being found.

[Scott Morrison]

(You have to love whatever logic resulted in "Apparently I can't display a GUI system dialog from wherever I'm running, so instead I will fail silently without printing any text.")

[Sebastian Ullrich]

Phew.

[Scott Morrison]

So is this something that ought to be installed, or that elan-init ought to not need?

[Sebastian Ullrich]

You can install it manually from https://learn.microsoft.com/en-us/cpp/windows/latest-supported-vc-redist?view=msvc-170, but ideally elan should be compiled such that this is not needed

[Scott Morrison]

But presumably for now I should just include this as a step in the mathlib4 installation instructions?

[Scott Morrison]

Or can I assume that "no reasonable windows machine would be without this"!?

[Sebastian Ullrich]

I'll check if I can easily fix it in elan

[Scott Morrison]

Installing the vc_redist doesn't actually solve the problem, unfortunately. Same error message.

[Scott Morrison]

Ha, hilarious. The page you linked to has ARM, x86, and x64 downloads. I picked the x86 one, which installed happily, but didn't solve the problem. Uninstalling that one and installing the x64 one works, and allows elan to run...

[Scott Morrison]

Windows is FUN!

[Scott Morrison]

Next up, although the VSCode extension successfully installed elan, which successfully installed lean, I don't have elan or lake available in the PowerShell terminal. Should I have expected that?

[Scott Morrison]

Oh. If I start up a new powershell from the button thingy at the bottom left of Windows, then lake works. However a new terminal from within VSCode gives me a powershell that doesn't know about lake...

[Scott Morrison]

Restarting VSCode solves that problem. Lame, but manageable I guess.

[Scott Morrison]

(I had tried closing and reopening the terminal from within VSCode, to no avail; it required actually restarting VSCode)

[Scott Morrison]

Ugh, a bit further along,

lake +leanprover/lean4:nightly-2023-02-04 new lean-test math

terminates with:

error: dependency mathlib of «lean-test» not in manifest, use `lake update` to update

[Sebastian Ullrich]

I believe there was some issue with hyphens in package names

[Scott Morrison]

oops, did I copy-and-paste out of a bug report thread instead of instructions ... :woman_shrugging:

[Scott Morrison]

My mistake, it was not lake new that gave that error, but actually lake build a moment later.

[Scott Morrison]

And it happens with or without hyphens.

[Scott Morrison]

Running lake update works, but it seems pointlessly confusing to error on lake build right after you've run lake new. @Mac, what do you think?

[Scott Morrison]

If the only correct thing to do after lake new is lake update, then lake new should be doing that itself.

[Scott Morrison]

(FUN! that Powershell can't cope with Unicode...)

[Scott Morrison]

In any case, I'm done for the day, and will file issues / write up instructions / record a screen grab of all this next week.

[Kevin Buzzard]

Nice progress though! I would absolutely vote against demanding WSL, I would lose a lot of new (young mathematician) users that way.

[Mac Malone]

Scott Morrison said:

If the only correct thing to do after lake new is lake update, then lake new should be doing that itself.

That is only because lake new foo math adds a dependency (mathlib). All other setups would require you adding a require to lakefile before lake update would be useful. But yeah, performing a lake update in the lake new foo math would be convenient.

Also, based on my understanding of mathlib, is not the sequence lake new -> lake update -> lake exe cache get -> lake build?

[Scott Morrison]

Yes, that's correct, we currently require

• lake new blah math
• lake update
• lake exe cache get
• lake build
  Certainly we should incorporate lake update into lake new when called with math.
  I'm not sure about incorporating lake exe cache get, as it feels like that's something we want to teach new users about, to there's no harm in requiring it as a setup step.

[Mario Carneiro]

If lake build just transparently does lake cache get the way it does lake upload, I don't see why not to just hide it away

[Mac Malone]

Also, alternatively, if lake exe cache get was incorporating into lake build, one could just do lake build -U to do all three steps (update, cache get, and build) at once.

[Sebastian Ullrich]

If the cache was integrated into Lake, it could even be refined to only download the parts actually needed by the user, right from the editor (if global tasks like build testing and linting are offloaded to the CI)