linterOptions vs Options errors

Stream: mathlib4

[Damiano Testa]

I just pulled master and downloaded the cache. lake build reports Build completed successfully.

[Damiano Testa]

However, when I open files in VSCode, I get errors that seem to come from the new linterSets and Lean complains about linterOptions vs Options.

[Damiano Testa]

I tried removing the .lake dir and redownloading, but it did not help.

[Damiano Testa]

Is anyone else seeing this?

[Yaël Dillies]

Sounds like the kind of errors I get when I forget to restart the server after a Lean update. It sounds quite likely to be what's happening in your case since we're the start of the month

[Damiano Testa]

:man_facepalming: Thanks, Yaël, restarting the server seems to have fixed it!