Where to find "notes"

Stream: general

[Felix Weilacher]

Several declarations named Simps.apply have "See Note [custom simps projection]" as a docstring. Where can I find this note?

[Kim Morrison]

file#Mathlib/Tactic/Simps/Basic

particularly line 814

[Kim Morrison]

(I found this by grepping for library_note.*custom simps projection

[Johan Commelin]

There used to be a jump-to-defn function for these, right?

[Kim Morrison]

These notes used to just be clickable, but that seems to have been lost :-(

[Kim Morrison]

I think this was back in Lean 3

[Eric Wieser]

I think the issue here is that making them clickable would require hard-coding knowledge about mathlib into the extension. My understanding (based on similar tensions with doc-gen) is that this is no longer considered acceptable, even as a short term hack

[Felix Weilacher]

thanks!

[Edward van de Meent]

Perhaps it would be useful to gather all these notes to one place, so people will know where to look? I think having to search for documentation is an anti-pattern...

[Edward van de Meent]

This could conceivably allow us to tell docgen in some kind of setting where to look for these notes, and link them, which means it doesn't need to be a mathlib-specific solution

[Johan Commelin]

I think getting jump-to-defn to work shouldn't be too hard. And that seems like a solution that scales well

[Daniel Kang]

When lean meets openai o1?

[Edward van de Meent]

btw, the library_note command is defined in Batteries.Util.LibraryNote, so it is not quite a Mathlib-only thing.

[Edward van de Meent]

it might be predominantly used in mathlib (for all i know; i only ever head about it being used in this context), but it is technically a Batteries thing.

[Edward van de Meent]

As another alternative, maybe a command #check_note [some_note] might be used to display the note in the infoview?

[Edward van de Meent]

i have a prototype command which manages to find the notes in the same file, (presumably because Lean.Environment is local to a file). i'm quite new to metaprogramming and lean internals, so perhaps someone could take my prototype to a new level?

import Batteries.Util.LibraryNote
import Mathlib.Tactic.Simps.Basic

open Batteries.Util.LibraryNote

open Lean Parser Command

elab "#check_note" name:strLit : command => do
  let env ← getEnv
  let entries := libraryNoteExt.getEntries env
  let entry_name := name.getString
  let valid_entries := entries.filter (fun x => x.fst == entry_name)
  if valid_entries.isEmpty then
    logInfo "404 Note not found"
  else
    let compiled_entries := "/--\n" ++ "-/\n\n/--\n".intercalate (valid_entries.map (fun x => x.snd)) ++ "-/"
    logInfo compiled_entries

library_note "test"
/--
note1
-/


library_note "test"/--
note2
-/


#check_note "custom simps projection"
#check_note "test"

[Edward van de Meent]

import Batteries.Util.LibraryNote
import Mathlib.Tactic.Simps.Basic

open Batteries.Util.LibraryNote

open Lean Parser Command

elab "#check_note" name:strLit : command => do
  let env ← getEnv
  let entries := libraryNoteExt.getEntries env
  let imported := (libraryNoteExt.toEnvExtension.getState env).importedEntries
  let entry_name := name.getString

  let imported_filtered := (imported.map (Array.filterMap (fun x => if x.fst == entry_name then Option.some x.snd else Option.none))).flatten.toList

  let valid_entries := entries.filterMap (fun x => if x.fst == entry_name then some x.snd else none) ++ imported_filtered

  if valid_entries.isEmpty then
    logInfo "404 Note not found"
  else
    let compiled_entries := "/--\n" ++ "-/\n\n/--\n".intercalate valid_entries.reverse ++ "-/"
    logInfo compiled_entries

library_note "test"
/--
note1
-/


library_note "test"/--
note2
-/


#check_note "custom simps projection"
#check_note "test"

i figured out how to do it by myself :confetti:

[Edward van de Meent]

is this something that would be welcome in batteries (in Batteries.Util.LibraryNote?)

[Edward van de Meent]

fwiw, there now is this PR to batteries, adding the command to the file.

[Edward van de Meent]

as a side note, the README for batteries says that PRs should preferably use the tags system, but i don't have the right to add or change those, it seems.

[Jz Pan]

To make this work for doc-gen4, I think the easiest way is to hack the bibliography system, since [custom simps projection] syntax is the same as the bibliography syntax. Perhaps we can add a way to allow docstring or something else register global links with names.

[Jz Pan]

Unfortunately, this (along with some other enhancements) may need a two-pass approach for doc-gen...