search

leanprover / lean3-mode

Emacs mode for Lean
Apache License 2.0
69 stars 17 forks source link

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

Open holtzermann17 opened 6 years ago

holtzermann17 commented 6 years ago

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?