lean4-mode json-readtable-error 47

I have installed Lean4 via elan and have set lean-rootdir to home/cla/.elan and then home/cla/.elan/ and both times when I try to use lean-toggle-show-goal with the default Main.lean file generated by lake init foo, it gives me the error: lean get info: (json-readtable-error 47)

Apr 27 '23 19:04 Pi-Cla

Do you have Lean 3 mode installed?

Jul 13 '23 19:07 urkud

I also saw this error when I had lean-mode installed; replacing it with lean4-mode fixed this for me.

Aug 15 '23 20:08 kisonecat

You can have both packages, but the command to see goals in lean4-mode is lean4-toggle-info (bound to C-c TAB). The command you cited is from the lean-mode package (i.e., Lean 3).

Sep 27 '23 18:09 collares

Notice: you also need to not have lean-company installed to avoid this error.

Mar 12 '24 01:03 quinn-dougherty

You can have both packages, but the command to see goals in lean4-mode is lean4-toggle-info (bound to C-c TAB). The command you cited is from the lean-mode package (i.e., Lean 3).

I agree. lean4-mode does not define a command named lean-toggle-show-goal. The issue-report is just invalid and can be closed, in my opinion.

Jul 21 '24 18:07 mekeor

Notice: you also need to not have lean-company installed to avoid this error.

That'd be because lean-company depends on lean-mode. Only then, the command lean-toggle-show-goal becomes available.

Jul 21 '24 18:07 mekeor

I fixed this by thoroughly purging (with doom purge), since I had previously installed lean-mode and naively removing it didn't purge it thoroughly enough. So I'd expect people to keep running into it if they mistakenly install lean-mode before they realize they need lean4-mode.

Jul 22 '24 02:07 quinn-dougherty