search

leanprover / elan

The Lean version manager
Apache License 2.0
292 stars 34 forks source link

fix: when toolchains are empty, message is confusing #82

Closed marianaalanis93 closed 1 year ago

marianaalanis93 commented 1 year ago

This fix adds a second message, in case we want to install the default version of lean.

Kha commented 1 year ago

How about simply "use elan install toolchain to install a toolchain"?

Kha commented 1 year ago

I meant as the whole message, I don't see a point in repeating the information from the first message in that way

lovettchris commented 1 year ago

I think the first part is good, it indicates to the user that something went wrong, then the second part shows how to fix it.

Kha commented 1 year ago

But the first line already does that...? The repetition is wrong in any case: the first line specifically talks about updateable toolchains, as you can get this error message even if you have other, pinned toolchains installed.

marianaalanis93 commented 1 year ago

But the first line already does that...? The repetition is wrong in any case: the first line specifically talks about updateable toolchains, as you can get this error message even if you have other, pinned toolchains installed.

I think the first line is not too clear in case you have your .elan folder empty. In my case when it´s the first time seeing this message my first thought was "ok, I have toolchain(s) there but for some reason there aren´t updatable (maybe corrupted) "

Kha commented 1 year ago

Okay, that is information I can work with. We can either be more precise than "updateable" ("unpinned"? "toolchains following a channel"?), and/or we need a separate branch and message in the case of 0 installed toolchains in total.

marianaalanis93 commented 1 year ago

Okay, that is information I can work with. We can either be more precise than "updateable" ("unpinned"? "toolchains following a channel"?), and/or we need a separate branch and message in the case of 0 installed toolchains in total.

But, in this case we are checking 'if toolchains.is_empty() ' so I think this is the case just for empty folders, we can add a try-catch for checking the case that we have toolchains but for some reason they are not updatable.

Kha commented 1 year ago

so I think this is the case just for empty folders

no: https://github.com/leanprover/elan/blob/690bf35e0d4cb30322154397edd4e8c93111a18c/src/elan/config.rs#L353-L355

marianaalanis93 commented 1 year ago

Ok, so your suggestion is just leaving the second message as: "use elan toolchain install to install a toolchain.")