json-readtable-error 47

[Pi-Cla]

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)

[urkud]

Do you have Lean 3 mode installed?

[kisonecat]

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

[collares]

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).

[quinn-dougherty]

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

[mekeor]

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.

[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.

[quinn-dougherty]

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.