Additional LSP server capabilities

Stream: Editors & UIs

[Willem vanhulle]

Hey, I have experimented with some added capabilities to the LSP server:

Links to reference manual
image.png

Progress messages:
image.png

more tweaks at https://github.com/wvhulle/lean4

Can someone help in opening a PR since I don't know where to start....?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Willem vanhulle do you mean a PR against the Lean server (which is in the lean4 repo)? The contribution process is described here. The recommended sequence of events is to first discuss the exact feature being proposed on Zulip, then if people seem in favor of it to make an RFC issue on the repository, and finally if the RFC is accepted to make a PR.

[Willem vanhulle]

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 said:

Willem vanhulle do you mean a PR against the Lean server (which is in the lean4 repo)? The contribution process is described here. The recommended sequence of events is to first discuss the exact feature being proposed on Zulip, then if people seem in favor of it to make an RFC issue on the repository, and finally if the RFC is accepted to make a PR.

Okay thanks! :)
I made a draft pr already (marked work in progress) but I can close it.

It’s here: https://github.com/leanprover/lean4/pull/12731
I attached issues it might close including some rfcs

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Willem vanhulle I don't mean to discourage you from contributing--it is great and much appreciated when people are interested in making Lean better--but the trouble explained in the contributions doc is that all new code comes with a maintenance burden, potential bugs, etc. The PR includes quite a lot of orthogonal changes which could be split into smaller PRs, so is unlikely to be accepted as-is for just that reason. I would recommend splitting things up and going the RFC route.

[Willem vanhulle]

Okay I closed it. Sorry about the noise. Will split up in coming weeks. It’s a bit late at this part of the world and I’ll get some sleep ;)

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 said:

Willem vanhulle I don't mean to discourage you from contributing--it is great and much appreciated when people are interested in making Lean better--but the trouble explained in the contributions doc is that all new code comes with a maintenance burden, potential bugs, etc. The PR includes quite a lot of orthogonal changes which could be split into smaller PRs, so is unlikely to be accepted as-is for just that reason. I would recommend splitting things up and going the RFC route.