lean-mode
lean-mode copied to clipboard
wrong lean version used? -- "Syntax checker lean-checker reported too many errors"
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?