feat: add #help note command

[edegeltje]

on zulip it was mentioned that there used to be an easy way to find and/or read library notes, but that this feature no longer works, presumably since lean4.

This PR aims to remedy the situation by introducing the #help note "some tag" command, which displays all library notes marked with the tag "some tag" that are declared before the command, including in imports.

[edegeltje]

awaiting-review

[leanprover-community-bot]

Mathlib CI status (docs):

• ❌ Mathlib branch batteries-pr-testing-948 built against this PR, but testing failed. (2024-09-27 20:56:40) View Log
• ❌ Mathlib branch batteries-pr-testing-948 built against this PR, but testing failed. (2024-09-28 15:07:44) View Log
• ❌ Mathlib branch batteries-pr-testing-948 built against this PR, but testing failed. (2024-10-19 08:13:56) View Log
• ✅ Mathlib branch batteries-pr-testing-948 has successfully built against this PR. (2024-10-26 15:09:02) View Log
• ✅ Mathlib branch batteries-pr-testing-948 has successfully built against this PR. (2024-10-26 18:16:48) View Log
• ✅ Mathlib branch batteries-pr-testing-948 has successfully built against this PR. (2024-10-27 17:26:05) View Log

[fgdorais]

The Mathlib test help_cmd.lean will need to be updated as a result of this. Was this expected?

PS: Thank you for being the first live test of this new Batteries feature that checks whether a Batteries PR will break Mathlib downstream!

[edegeltje]

Was this expected?

when writing this PR i certainly did not take this in consideration, so it was not something i was expecting...
still, looking at how the failing test is written, it is not a surprise it "broke", as its success does indeed depend on what commands start with "#chec" despite that not being the goal of the test.

[fgdorais]

Indeed, that is a poorly designed test. On the other hand, that test's output shows that #check_notes doesn't quite fit with the other #check commands. It fits better with #print commands but not perfectly. Perhaps it should be a #help command? What do you think?

[edegeltje]

i guess it could be a #help command, but i think #help is in mathlib? i think #show_note is an acceptable alternative name. What mathlib does with #help is their concern, they are free to reuse the code here to get the output, although i don't think this feature fits the expectations of #help...

[fgdorais]

Actually, it makes sense to move #help here or even to Lean since it's useful to everyone and nothing about it is Mathlib specific. 🤔

[fgdorais]

The #help command is now in Batteries. This PR can now be adapted as the #help notes subcommand.

[edegeltje]

wip

[edegeltje]

awaiting-review

[fgdorais]

This is looking excellent and it now passes Mathlib CI!

One final thing: the command should be in Batteries.Tactic.HelpCmd along with the other #help commands and the module doc there should be updated.

[edegeltje]

One final thing: the command should be in Batteries.Tactic.HelpCmd along with the other #help commands and the module doc there should be updated.

in my opinion, it is more natural to have the tool here, in order to make sure it is available wherever library notes are...
this is not meant to be a #help command. this is meant to be a command which lets you read library notes. it only became a help command by lack of a better name.

[fgdorais]

In any case, the module doc at Batteries.Tactic.HelpCmd needs to be updated.

I don't understand why you claim it's not a help command. Just like the other help commands, it's handy for users when writing code but it is not useful as code. That's why HelpCmd is not imported anywhere in Batteries and Mathlib except in the global import files. I don't see why #help note should be any different than the others.

[fgdorais]

I'm afraid I must insist on moving to Batteries.Tactic.HelpCmd for maintainability reasons. Your proposed alternative has some issues (1) importing Batteries.Tactic.HelpCmd doesn't import all help commands and (2) importing Batteries.Util.LibraryNotes into Batteries.Tactic.HelpCmd would not pass shake. I see no more practical way around these problems.

[edegeltje]

@fgdorais how about we put an alias of the command in Batteries.Tactic.HelpCmd? that should fix both issues, and still make sure that the functionality exists wherever you can make library notes. the "original" can then be something like #find_note "label", and there can be a simple macro turning #help note into that...
or does that still give maintainability issues?

[fgdorais]

That's too hacky for Batteries. Like I said before the reason why help commands like this one aren't available everywhere is that they are only useful for users while writing code, but of no use in the code itself. You will just have to get used to importing help commands while writing a Batteries or Mathlib PR and then deleting the import before submitting.

[edegeltje]

awaiting-review

[edegeltje]

i don't see the issue with having this command always available. AFAIK, it shouldn't be that impactful if these are or aren't imported.

[fgdorais]

FWIW, I think Batteries.Tactic.HelpCmd would be a nice addition to Mathlib.Init.