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

[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

[edegeltje]

unfortunately it seems i can't write a test to make sure the command indeed does work across imports, as i can't figure out how to import a test file in another test file, and writing a library note in the actual module for the sole purpose of testing might not be desirable. In particular, it is impossible to write a library note in the same file that the environment extension is defined.

[fgdorais]

This is what Batteries.Test.Internal is for! You can add DummyLibraryNote.lean in that folder and import it in the test file.

[edegeltje]

WIP

[edegeltje]

awaiting-review

[fgdorais]

You need to add the dummy files to Batteries.lean.

This looks really good! Other #help subcommands support prefix search, I don't think that's essential but it would be nice.

I'll be busy for the rest of the day, so I'll come back for a review tomorrow.

[edegeltje]

i added code for prefix search, but left it in comments since it depends on List.ne_nil_of_mem_groupBy (substituted with sorry) from mathlib... if the lemma could get upstreamed, we can enable the feature (and add appropriate tests)

[fgdorais]

You can use List.head! instead of List.head.

[edegeltje]

ok, it should have all the desired features now. please make sure the documentation and tests are sufficient.

[fgdorais]

I don't see the utility of wrapping each note in /-- ... -/. How about just separating with a blank line or ---?

[edegeltje]

i think the benefit is that this is less likely to cause confusion as to where one note stops and another begins, and this mimics the way you'd find the note in the actual code.

[fgdorais]

I guess my issue is that /-- ... -/ has a specific meaning in Lean, which is not relevant here. So, for example, copy pasting the output in a Lean file would lead to multiple errors. How about /- ... -/? (No errors then, though that still seems visually cluttered.)

[digama0]

We aren't doing this for any of the other #help commands, I think the docs should just be indented relative to the library_note header.

[fgdorais]

I reflected on this a bit and I think #help subcommands should give output that is better than plain code lookup in some useful way. In many cases organization is the key difference but formatting is relevant too. I don't know what would be the best formatting for library notes. How about asking on Mathlib Zulip what users would like to see for library notes?

[fgdorais]

By the way, no worries about the current breaks-mathlib label. That will be fixed downstream once mathlib4#17257 gets merged.

[edegeltje]

By the way, no worries about the current breaks-mathlib label. That will be fixed downstream once mathlib4#17257 gets merged.

actually, it looks to me like the script trying to find the mathlib branch fails...
see for example how this run fails with an error trying to get info about the PR triggering the ci, from what i can tell... so even before looking at mathlib

[fgdorais]

Yes, the script is broken right now, we're doing manual testing for the time being.