feat: add #help note command

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/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

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner
+Authors: Gabriel Ebner, Edward van de Meent
 -/
 import Lean.Elab.Command
 
@@ -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,47 @@ 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.
 -/
 elab "library_note " title:strLit ppSpace text:docComment : command => do
   modifyEnv (libraryNoteExt.addEntry · (title.getString, text.getDocString))
+
+/--
+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 in
+/--
+`#help note "foo"` searches (case-insensitively) 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 note" 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))
+    -- this could use List.head when List.ne_nil_of_mem_groupBy gets upstreamed from mathlib

test/library_note.lean

@@ -0,0 +1,47 @@
+import Batteries.Util.LibraryNote
+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"