Zulip Chat Archive

Stream: new members

Topic: leanpkg uncaught exception


Max (May 28 2021 at 09:01):

Hallo, lean looks very promising! I'm just (starting to) exploring what it can do in my spare time for now.
I installed lean4 via curl in WSL, but when I try to invoke leanpkg init I get

uncaught exception: Lean package manager, version nightly-2021-05-28

Usage: ...

is this a known bug or is that new to the nightly version and should I just wait until tomorrow :P ?


Last updated: Dec 20 2023 at 11:08 UTC