LSP in Lean4 repo (module keyword error)

Stream: lean4

[Lua Viana Reis]

Hi all,

I'm having trouble enabling the LSP server for files in the Lean 4 repository. I changed the lean-toolchain file to use leanprover/lean4-nightly, but lake serve reports

warning: package configuration has errors, falling back to plain `lean --server`

and then every file has the error

error   Lean 4: `module` keyword is experimental and not enabled here

[Lua Viana Reis]

should I manually create a lakefile? or somehow pass experimental.module=true to lean --server directly? how is development in the repo supposed to work?

[Lua Viana Reis]

lean -D experimental.module=true --server

works! Is it the right way?

[Henrik Böving]

I assume you are working with Emacs? This just works in both neovim and vscode so I would suggest to figure out how they implement this part.

[Lua Viana Reis]

I see, I'm using "plain" eglot in emacs with a major-mode I am writing. Perhaps I should look how vscode special-case this

[Lua Viana Reis]

because the original content of lean-toolchain is lean4, which makes lean --serve report

error: no such release: 'lean4'

[Henrik Böving]

Have you set up your elan in accordance with the development guide?

[Lua Viana Reis]

thanks, I had not seen it before :) perhaps it deserves a mention in CONTRIBUTING.md

[Lua Viana Reis]

oops, it is mentioned in contributing.md :face_with_peeking_eye:

[Lua Viana Reis]

Sorry about that, the elan setup makes lake serve work perfectly!! Thanks @Henrik Böving!