feat: add #help note command (#948)

Co-authored-by: Blizzard_inc <thrashy4inbox@gmail.com>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>

Batteries.lean

@@ -96,6 +96,8 @@ import Batteries.Tactic.Trans
 import Batteries.Tactic.Unreachable
 import Batteries.Tactic.Where
 import Batteries.Test.Internal.DummyLabelAttr
+import Batteries.Test.Internal.DummyLibraryNote
+import Batteries.Test.Internal.DummyLibraryNote2
 import Batteries.Util.Cache
 import Batteries.Util.ExtendedBinder
 import Batteries.Util.LibraryNote

Batteries/Tactic/HelpCmd.lean

@@ -1,10 +1,11 @@
 /-
-Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Copyright (c) 2024 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
+Authors: Mario Carneiro, Edward van de Meent
 -/
 import Lean.Elab.Syntax
 import Lean.DocString
+import Batteries.Util.LibraryNote
 
 /-!
 
@@ -19,9 +20,11 @@ The `#help` command can be used to list all definitions in a variety of extensib
   * `#help term`, `#help tactic`, `#help conv`, `#help command`
     are shorthand for `#help cat term` etc.
   * `#help cat+ C` also shows `elab` and `macro` definitions associated to the syntaxes
+* `#help note "some note"` lists library notes for which "some note" is a prefix of the label
 
-All forms take an optional identifier to narrow the search; for example `#help option pp` shows
-only `pp.*` options.
+Most forms take an optional identifier to narrow the search; for example `#help option pp` shows
+only `pp.*` options. However, `#help cat` makes the identifier mandatory, while `#help note` takes
+a mandatory string literal, rather than an identifier.
 
 -/
 
@@ -276,6 +279,44 @@ elab_rules : command
   | `(#help cat $[+%$more]? $cat $id:ident) => elabHelpCat more cat (id.getId.toString false)
   | `(#help cat $[+%$more]? $cat $id:str) => elabHelpCat more cat id.getString
 
+/--
+format the string to be included in a single markdown bullet
+-/
+def _root_.String.makeBullet (s:String) := "* " ++ ("\n  ").intercalate (s.splitOn "\n")
+
+open Lean Parser Batteries.Util.LibraryNote in
+/--
+`#help note "foo"` searches for all library notes whose
+label starts with "foo", then displays those library notes sorted alphabetically by label,
+grouped by label.
+The command only displays the library notes that are declared in
+imported files or in the same file above the line containing the command.
+-/
+elab "#help " colGt &"note" colGt ppSpace name:strLit : command => do
+  let env ← getEnv
+
+  -- get the library notes from both this and imported files
+  let local_entries := (libraryNoteExt.getEntries env).reverse
+  let imported_entries := (libraryNoteExt.toEnvExtension.getState env).importedEntries
+
+  -- filter for the appropriate notes while casting to list
+  let label_prefix := name.getString
+  let imported_entries_filtered := imported_entries.flatten.toList.filterMap
+    fun x => if label_prefix.isPrefixOf x.fst then some x else none
+  let valid_entries := imported_entries_filtered ++ local_entries.filterMap
+    fun x => if label_prefix.isPrefixOf x.fst then some x else none
+  let grouped_valid_entries := valid_entries.mergeSort (·.fst ≤ ·.fst)
+    |>.groupBy (·.fst == ·.fst)
+
+  -- display results in a readable style
+  if grouped_valid_entries.isEmpty then
+    logError "Note not found"
+  else
+    logInfo <| "\n\n".intercalate <|
+      grouped_valid_entries.map
+        fun l => "library_note \"" ++ l.head!.fst ++ "\"\n" ++
+          "\n\n".intercalate (l.map (·.snd.trim.makeBullet))
+
 /--
 The command `#help term` shows all term syntaxes that have been defined in the current environment.
 See `#help cat` for more information.

Batteries/Test/Internal/DummyLibraryNote.lean

@@ -0,0 +1,14 @@
+import Batteries.Util.LibraryNote
+
+library_note "test" /--
+1: This is a testnote for testing the library note feature of batteries.
+The `#help note` command should be able to find this note when imported.
+-/
+
+library_note "test" /--
+2: This is a second testnote for testing the library note feature of batteries.
+-/
+
+library_note "temporary note" /--
+1: This is a testnote whose label also starts with "te", but gets sorted before "test"
+-/

Batteries/Test/Internal/DummyLibraryNote2.lean

@@ -0,0 +1,15 @@
+import Batteries.Test.Internal.DummyLibraryNote
+
+library_note "test" /--
+3: this is a note in a different file importing the above testnotes,
+but still imported by the actual testfile.
+-/
+
+library_note "Test" /--
+1: this is a testnote with a label starting with "Te"
+-/
+
+library_note "Other" /--
+1: this is a testnote with a label not starting with "te",
+so it shouldn't appear when looking for notes with label starting with "te".
+-/

Batteries/Util/LibraryNote.lean

@@ -15,6 +15,7 @@ open Lean
 
 /-- A library note consists of a (short) tag and a (long) note. -/
 def LibraryNoteEntry := String × String
+deriving Inhabited
 
 /-- Environment extension supporting `library_note`. -/
 initialize libraryNoteExt : SimplePersistentEnvExtension LibraryNoteEntry (Array LibraryNoteEntry) ←
@@ -35,6 +36,8 @@ creates a new "library note", which can then be cross-referenced using
 -- See note [some tag]
 ```
 in doc-comments.
+Use `#help note "some tag"` to display all notes with the tag `"some tag"` in the infoview.
+This command can be imported from Batteries.Tactic.HelpCmd .
 -/
 elab "library_note " title:strLit ppSpace text:docComment : command => do
   modifyEnv (libraryNoteExt.addEntry · (title.getString, text.getDocString))

test/library_note.lean

@@ -0,0 +1,47 @@
+import Batteries.Tactic.HelpCmd
+import Batteries.Test.Internal.DummyLibraryNote2
+
+/--
+error: Note not found
+-/
+#guard_msgs in
+#help note "no note"
+
+/--
+info: library_note "Other"
+* 1: this is a testnote with a label not starting with "te",
+  so it shouldn't appear when looking for notes with label starting with "te".
+-/
+#guard_msgs in
+#help note "Other"
+
+library_note "test"/--
+4: This note was not imported, and therefore appears below the imported notes.
+-/
+
+library_note "test"/--
+5: This note was also not imported, and therefore appears below the imported notes,
+and the previously added note.
+-/
+
+
+/--
+info: library_note "temporary note"
+* 1: This is a testnote whose label also starts with "te", but gets sorted before "test"
+
+library_note "test"
+* 1: This is a testnote for testing the library note feature of batteries.
+  The `#help note` command should be able to find this note when imported.
+
+* 2: This is a second testnote for testing the library note feature of batteries.
+
+* 3: this is a note in a different file importing the above testnotes,
+  but still imported by the actual testfile.
+
+* 4: This note was not imported, and therefore appears below the imported notes.
+
+* 5: This note was also not imported, and therefore appears below the imported notes,
+  and the previously added note.
+-/
+#guard_msgs in
+#help note "te"