feat: dot auto-completion for most occurrences of global identifiers

[Rob23oba]

This PR adds dot auto-completion to many syntactic constructions, including e.g. #print or unfold. A follow-up PR will be necessary for bootstrapping.

Closes #8353

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-8424 build failed against this PR. (2025-05-21 12:03:08) View Log
• 💥 Mathlib branch lean-pr-testing-8424 build failed against this PR. (2025-05-21 13:04:21) View Log
• 💥 Mathlib branch lean-pr-testing-8424 build failed against this PR. (2025-05-21 15:01:59) View Log
• 💥 Mathlib branch lean-pr-testing-8424 build failed against this PR. (2025-05-21 15:07:09) View Log
• 🟡 Mathlib branch lean-pr-testing-8424 build against this PR was cancelled. (2025-05-21 15:37:38) View Log
• 🟡 Mathlib branch lean-pr-testing-8424 build against this PR was cancelled. (2025-05-21 15:41:51) View Log
• ✅ Mathlib branch lean-pr-testing-8424 has successfully built against this PR. (2025-05-21 16:23:38) View Log
• ✅ Mathlib branch lean-pr-testing-8424 has successfully built against this PR. (2025-05-24 12:35:06) View Log

[eric-wieser]

This is surely worth its own PR!

[Rob23oba]

Well I'd rather do bootstrapping once with an unrelated fix than do it twice because of such a small change...

[eric-wieser]

I thought CI did bootstrapping automatically these days

[Rob23oba]

Oh no I mean I need to do things after a stage0 update to complete the change.

[eric-wieser]

#8517

[Kha]

Thanks for the in-depth PR. I believe this is not quite going in the right direction though: we should finally fix ident so that it can properly represent trailing dots as missing input.

[Rob23oba]

Hmm how do we make sure then that it doesn't parse trailing dots of e.g. field notation or provide an error for them? (e.g. a.1)

[Rob23oba]

Or should we treat erroring on trailing dots as default behavior and use identWithoutTrailingDot or whatever?

[Kha]

Field index notation is an interesting edge case, true! It may be best to special-case it in ident.

[Rob23oba]

Another problem is Lean.Parser.Term.completion which has it's own error message: "invalid field notation, identifier or numeral expected". I don't think we can get around adding some mechanism to make sure that identifiers in terms have special treatment. Maybe we could keep ident (the token) without trailing dot treatment but add special treatment for trailing dots to the default ident parser. Then we could have a variant that only parses ident (the token). However both of these have an ident antiquotation and correspond to Lean.Ident.

[Rob23oba]

Actually no I was just dumb lol I thought that ident would need to produce an error on its own but instead we can just make the ident parser take the position after the "." as the end position in the source info and the end of rawVal but keep the generated name and the position afterwards. Then the parsers that come after that make sure to produce an error message about the dot (or not). So basically we only make sure that the . becomes part of the syntax range and can be reliably detected in the rawVal.

[Rob23oba]

Actually no again that would probably not work because then we don't actually consume the dot and thus it doesn't become part of the syntax range when nested into other nodes.

[Rob23oba]

Okay so the best I can come up with is that ident (the token) stays and ident (the parser) additionally consumes trailing dots and if it did, produce an error message. Then we provide identBeforeDot which can be used for term and e.g. declId. Both variants would then have the ident antiquot though and produce Lean.Ident nodes while the default ident additionally puts the trailing dot into its rawVal and source info.

[Rob23oba]

I'll open a separate PR for a better fix