search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.04k stars 348 forks source link

Completion of keywords into identifiers #3623

Open Kha opened 4 months ago

Kha commented 4 months ago 
#check with

When typing this line, we get ident completion up to typing the h. Ideally we should get it even then.

Kha commented 4 months ago

Note: we should make sure to also provide the keyword itself as a completion option here, which is not the case yet

nomeata commented 4 months ago

That would probably fix https://github.com/leanprover/lean4/issues/3462 as well.

kmill commented 3 months ago

Something that trips me up a lot is a popup on do, both in Lean and in Mathlib.

image image

This Mathlib one might not be related, but I thought I'd mention it.

These are especially painful since the natural thing to do after typing do is to hit "enter", which activates the completions.

semorrison commented 2 months ago

I get bitten by the do completion regularly!

mhuisi commented 2 months ago

I get bitten by the do completion regularly!

Do you still see this issue after #3778?

Note that this issue is not about the popup issue that Kyle mentioned (which should have been resolved by #3778), but specifically about offering identifier completions when typing in keywords.

semorrison commented 2 months ago

Unfortunately yes:

do-completion
mhuisi commented 2 months ago

Unfortunately yes: do-completion

That's a code snippet manually added by Mathlib, the language server is not involved here.

leodemoura commented 1 month ago

As far as I can tell this issue has been fixed. I cannot reproduce any of them using v4.8.0-rc2. Closing soon.

mhuisi commented 1 month ago

As far as I can tell this issue has been fixed. I cannot reproduce any of them using v4.8.0-rc2. Closing soon.

The issue reported by Sebastian is still there (we don't report identifier completions for keywords), the other unrelated issues in the thread should have been fixed by #3778.