search

avigad / lamr

Logic and Mechanized Reasoning
82 stars 20 forks source link

Book assumes VSCode but doesn't say so #6

Closed dabrahams closed 4 weeks ago

dabrahams commented 4 weeks ago

Sorry if this is filed in the wrong place. https://avigad.github.io/lamr/using_lean_as_a_programming_language.html talks about hovering over things and an “ information window” that are confusing for an Emacs user, which is where I started my setup. It would be good for the book to say up front that it assuming you're using VSCode. (Also would be very useful if it had an up-front link to the codespaces option for people who want to dive right in)

Vtec234 commented 4 weeks ago

I agree it would be good for the book to clarify which editor setups are supported. However, both hovering and the infoview (information window) should work in Emacs with leanprover-community/lean4-mode.

dabrahams commented 4 weeks ago

I had it installed, but I didn't realize I needed to be inside a Lean project for LSP to do its thing. I do get hovering within the book project. However, I don't see any buffer corresponding to an “information window.” What am I missing?

dabrahams commented 4 weeks ago

Ah, never mind, I found toggle info display in the menu. Thanks!