lean broke

Stream: new members

[King Arthur]

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]

@King Arthur, do elan self update

[King Arthur]

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]

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]

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]

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]

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

[Kevin Buzzard]

The last one should start building your project