wrong lean version used? -- "Syntax checker lean-checker reported too many errors"

[holtzermann17]

Hi, I created a simple project to test out mathlib. It was working initially but revisiting the test file later, I got an error message:

Warning (flycheck): Syntax checker lean-checker reported too many errors (659) and is disabled.

I found that if I switch to a different version of lean with M-x lean-server-switch-version, the error messages stop appearing, and interactions continue as usual.

I have two Lean versions available: stable and 3.4.1. Is there a better way to get lean-mode to use the correct version of Lean on a per-project basis?