Zulip Chat Archive

Stream: new members

Topic: lean broke

King Arthur (Oct 14 2022 at 08:51):

I wanted to use something from a newer version of mathlib, so I used leanproject up on the command line. this ended up backfiring and now I can't seem to use lean anymore. whenever I open vscode, this message appears in the output:

info: downloading component 'lean'
error: binary package was not provided for 'windows'

Yaël Dillies (Oct 14 2022 at 09:30):

@King Arthur, do elan self update

King Arthur (Oct 14 2022 at 10:01):

I did that and now the output is showing a long list of lines that look like {"caption":"","file_name":"(project folder)\\_target\\deps\\mathlib\\src\\tactic\\congr.lean","pos_col":0,"pos_line":7,"severity":"warning","text":"imported file '(project folder)\\_target\\deps\\mathlib\\src\\tactic\\rcases.lean' uses sorry"}

Kevin Buzzard (Oct 14 2022 at 10:56):

Did elan self update work? What does elan -V now show?

If it's showing 1.4.2 (which is what we want it to show), what happens if you do leanproject up ?

King Arthur (Oct 14 2022 at 11:09):

elan -V gives me elan 1.4.2 (4a1b1b918 2022-09-13) and leanproject up gives me 'dependencies' (vscode output is still the same after doing this)

King Arthur (Oct 15 2022 at 06:49):

I'm still having trouble with this but I don't want to do a full reinstall just yet because there's probably a solution to this somewhere (and I'm going to run into this again eventually when I do try to update another time)

Kevin Buzzard (Oct 15 2022 at 07:02):

If you type leanproject get-mathlib-cache followed by leanproject build do both of these now work?

Kevin Buzzard (Oct 15 2022 at 07:02):

The last one should start building your project

Last updated: Dec 20 2023 at 11:08 UTC