feat: @[builtin_doc] attribute (part 2)

[digama0]

This solves the issue where certain subexpressions are lacking syntax hovers because the hover text is not "builtin" - it only shows up if the Parser constant is imported in the environment. For top level syntaxes this is not a problem because builtin_term_parser will automatically add this doc information, but nested syntaxes don't get the same treatment.

We could walk the expression and add builtin docs recursively, but this is somewhat expensive and unnecessary given that it's a fixed list of declarations in lean core. Moreover, there are reasons to want to control which syntax nodes actually get hovers, and while a better system for that is forthcoming, for now it can be achieved by strategically not applying the @[builtin_doc] attribute.

Fixes #3842

[Kha]

Part 2 can be moved into a separate PR, no?

[Kha]

Part 1 is fine to merge as is

[nomeata]

This will fix #3842, right?

[digama0]

Part 2 can be moved into a separate PR, no?

As I indicated in the PR, I'm not sure how the protocol for this works. Do I open two PRs, one with the first and one with all 3 commits? And then rebase the second one after the first is merged and the stage0 bot runs? How do I signal the bot to run?

[nomeata]

If the first step works on it's own (i.e. passes the test suite), you can put it on a PR of it's own and merge. If this changes the stdflags.h file, as such PRs often do, the bot will automatically update stage0 on master. If not you can trigger the workflow manually using the button at https://github.com/leanprover/lean4/actions/workflows/update-stage0.yml.

If the first step on its own is not suitable for master, then doing it as you do here, and asking an admin to rebase merge, is the way to go.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 291bb84c972dae470e8f5602729e9d5a5e9433a2 --onto d6474135baac39a271c301a17d6621691a48b80b. (2024-04-19 16:48:44)
• ✅ Mathlib branch lean-pr-testing-3918 has successfully built against this PR. (2024-04-20 18:30:10) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a47c590a914e5ed564d07e8ec303c77b81f51c5c --onto adfd6c090ef7d6bdcc8f69c5dd6f919b1b71cab3. (2024-09-12 20:31:47)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b34379554d3e75ac021c5cddd7101b482c600a98 --onto adfd6c090ef7d6bdcc8f69c5dd6f919b1b71cab3. (2024-09-13 08:07:47)

[nomeata]

Remember to update the PR description so that it also works as the commit message

[digama0]

It does, did you want me to put (part 2)?

[nomeata]

Ah, maybe by browser still showed the old message asking about the procedure, but a reload helped. All good.

[nomeata]

Hmm, looks like this doesn't bootstrap as is.

[nomeata]

@digama0, what is the status of this PR? Would be good to fix the issue, but I also see some FIXME in the code, and also builtin_docs on parser combinators where I don’t fully understand if the attribute should be there.

[digama0]

this PR was meant to be merged immediately after part 1, but I guess it wasn't and now presumably it has rotted

[digama0]

The FIXMEs are fine to merge as is. The issue is that while it would be nice to have docs for these bits of syntax, they appear far too often and suppress more useful hovers, so they probably need another attribute to undo the effect of @[builtin_doc] here for the purpose of hovers.

[nomeata]

Thanks for the explanation!

so they probably need another attribute to undo the effect of @[builtin_doc] here for the purpose of hovers.

Is this specific to builtin_doc? Or would you need a mechanism to suppress the hovers also if the syntax wasn’t builtin? I.e. a “This syntax has documentation, but never show it in hovers”

Indeed, for example the doc string for /-- … -/ (“A docComment parses a "d…”) shows up once I import Lean. That explains why I get these unhelpful hovers when working on lean itself, but not regular users! Ugh.

Do we have a fundamental issue here that a docstring on a parser is used for two very different audiences, authors of parsers and users of the resulting syntax?

I guess this is what you are saying in the PR description. You say “while a better system for that is forthcoming” - is there an PR or RFC for that? It might be useful to link to that from the FIXME, so that when I or someone else stumble over the FIXME comment in a year we it’s clearer why it’s there and when it can be fixed.

[nomeata]

Uff, now that understand the issue better I find many hovers of dubious quality when doing import Lean. For example

optDeclSig matches the signature of a declaration with optional type: a list of binders and then possibly : type

when hovering over the : in a declaration. That’s kinda bad, the optDeclSig is not useful to a user, and this is arguably worse than no hovers! And others are worse.

But this already affects everyone doing import Lean, so including everyone working on mathlib, so I guess it’s only consistent to show the same to users without that import.

The proper fix would require going through all docstrings of parsers and either rephrase them to make sense to users, or (somehow?) prevent them from leaking into hovers. That sounds like a fair bit of work, though.

[digama0]

Yes, you see the issue now. There is a difference between documentation useful for people reading the parser or hovering references in a syntax declaration, and documentation useful for people hovering bits of syntax to understand how lean works. I think the best way to address this in the near term is to selectively avoid @[builtin_doc], and in the slightly longer term to add an attribute to suppress hovers for specific syntax nodes (both builtin and user-defined) which we want to document but not for end users. We might also want to have two sets of documentation in some cases, for separating dev-focused and user-focused docs.

As for whether I'm working on such an attribute: I may have been thinking about it at the time, but this PR took way too long to merge and now I've forgotten any plans I had (and also in the meantime the governmental structure of lean has changed to the point that I don't really like making PRs like this anymore). It doesn't seem like a particularly hard task though, the spec and implementation seem clear enough.

[nomeata]

I think the best way to address this in the near term is to selectively avoid @[builtin_doc]

Hmm, but that only helps users on a bare lean file, but for example not mathlib users, does it?

in the slightly longer term to add an attribute to suppress hovers for specific syntax nodes (both builtin and user-defined) which we want to document but not for end users. We might also want to have two sets of documentation in some cases, for separating dev-focused and user-focused docs.

Agreed!

Sorry for the slow handling of this PR, I think it fell between the cracks when I sent it to the merge queue, but it came back due to a failed CI check (bootstrapping issues?). Actually, I wonder if we still have that problem, let me add the release-ci label to check.

[digama0]

I think the best way to address this in the near term is to selectively avoid @[builtin_doc]

Hmm, but that only helps users on a bare lean file, but for example not mathlib users, does it?

Mathlib doesn't have many syntax definitions which are internal in the same way as core lean definitions. For those that do exist, they currently are causing problems and that issue is not addressed by this PR (which is about adding docstrings for syntax that can clearly benefit from it and which currently only shows the docstring with import Lean).

The bootstrapping issue was probably caused by an import Lean.DocString which was a cyclic import after the bump and had to be changed to import Lean.DocString.Extension.

[nomeata]

Hmm, but import Mathlib implies import Lean, doesn’t it? At least in my testing,

inductive Foo

has no hover over inductive (fixed by this PR), but

import Mathlib
inductive Foo

has (already before this PR). In that sense this change doesn’t affect the typical mathlib user, but only the user working on files without a (transitive) import of Lean. And it’s good if they all get the same experience, even if we ought to improve that at some point.

[digama0]

Yes, that is correct. The fact that import Lean is needed for several not obviously related features to work, like go to definition and hovers for core syntax, is a frequent source of confusion/questions on the zulip.