Zulip Chat Archive

Stream: general

Topic: what is the tag for lean3?

Joseph O (Apr 21 2022 at 22:14):

PS C:\Users\vatis\Desktop\programming\natural_number_game\lean3> elan default leanprover/lean3:stable
info: syncing channel updates for 'stable'
error: failed to resolve latest version of 'stable'
info: caused by: failed to parse latest release tag

Eric Wieser (Apr 21 2022 at 22:17):

I would guess it's v3.42.0 or similar; but I think this is an #xy problem

Eric Wieser (Apr 21 2022 at 22:17):

You shouldn't have to invoke elan yourself, leanpkg does that for you by reading the leanpkg.toml

Joseph O (Apr 21 2022 at 22:18):

image.png

Joseph O (Apr 21 2022 at 22:19):

I have a leanpkg.toml, also, the lsp is not working at all

Joseph O (Apr 21 2022 at 22:24):

image.png

Joseph O (Apr 21 2022 at 22:35):

ANy ideas why the server might fail?

Joseph O (Apr 21 2022 at 22:42):

Im using the lean vscode extension, and the lean 4 one is disabled

Arthur Paulino (Apr 21 2022 at 22:52):

How did you install Lean 3?

Joseph O (Apr 21 2022 at 22:53):

Joseph O said:

PS C:\Users\vatis\Desktop\programming\natural_number_game\lean3> elan default leanprover/lean3:stable
info: syncing channel updates for 'stable'
error: failed to resolve latest version of 'stable'
info: caused by: failed to parse latest release tag

i tried doing this but it was failing

Arthur Paulino (Apr 21 2022 at 22:56):

I never tried creating my own Lean 3 project. I just open mathlib and it works

Joseph O (Apr 21 2022 at 22:59):

hmm

Last updated: Dec 20 2023 at 11:08 UTC