library notes

Stream: mathlib4

[Kevin Buzzard]

I literally cannot find a library note. My algorithm usually is just "search for the name of the note and spot it in the search results" but I just tried searching for [lower instance priority] in order to figure out why an instance was prio 100 (this library note was mentioned) and the search just gives 500 results. What's the trick to find the actual library note rather than just the 499 things telling us to look at it? NB ideally this would not involve having to remember the name of a file because I am really bad at this.

[Jireh Loreaux]

How about search for library_note "lower instance priority"

[Edward van de Meent]

There's this handy command I wrote called #help note which will let you search and display the appropriate note

[Kevin Buzzard]

Am I not using #help note properly or is it not in master or do I have to import something?

[Edward van de Meent]

It should be available wherever help commands are

[Edward van de Meent]

The search is limited by imports though

[Kevin Buzzard]

aah searching for libary_note seems to work. Lol Mathlib.Algebra.HeirarchyDesign is only imported by Mathlib :-)

[Kevin Buzzard]

(it's just a file full of library notes so who needs to import it?)

[Edward van de Meent]

That sounds like somethin that can be fixed, right?

[Edward van de Meent]

Kevin Buzzard said:

(it's just a file full of library notes so who needs to import it?)

The files which refer to the notes, of course

[Jovan Gerbscheid]

Why aren't library_notes designed with a ctrl+click feature? This shouldn't be that hard to implement, right? And this would force the library note to be imported where it is referenced.

[Jovan Gerbscheid]

Although it may be annoying to make shake aware that the imports aren't unnecessary.

[Johan Commelin]

I'm inclined to have

def LibraryNote := String

And then in certain files

def LibraryNote.lowerInstancePriority : LibraryNote := "bla bla bla"

And then in other files

#library_note lowerInstancePriority

Or some variation on that design.

[Kevin Buzzard]

I should say that it's not the first time I've failed to find a library note and I remember at least one other occasion when someone asked how to find them. My mistake this time was including the square brackets in my search string

[Michael Rothgang]

Repeating what I hear: so your proposal is to

• make a new definition `LibraryNote := String
• defining a new library changes from #library_note "lower instance priority" "Text of the library note" to def LibraryNote.lowerInstancePriority := "Text of the library note" (and similarly for all notes)
• referencing a library note becomes #libraryNote LibraryNote.lowerInstancePriority (which is a no-op command, but enforces that the declaration is a LibraryNote, enabling Ctrl-Click)

I wonder if writing See LibraryNote.lowerInstancePriority`` would also be a suitable alternative: doc-gen would (hopefully) linkify that, so we'd have library notes in the generated documentation. You cannot Ctrl-click it, but you could #print LibraryNote.lowerInstancePriority, which is perhaps good enough.

I presume you'd also want to

• change #help note LibraryNote.lowerInstancePriority to look up all LibraryNote declarations in the environment. (Or perhaps still allow "lower instance priority", all lower-cased, and manually do name processing? Not a big deal implementation-wise.)

[Edward van de Meent]

Do note (hah) that the implementation for these things is in batteries, not mathlib

[Michael Rothgang]

For #help note: yes, I know. But I presume that's an issue one could deal with.

[Edward van de Meent]

if we're going the direction of defining a type LibraryNote, we might as well define it as Unit and have the contents be actual docstrings which show on hover

[Johan Commelin]

One downside of my proposal is that you don't see the value of the library note in the hover tooltip.

[Johan Commelin]

I wanted to make the Unit suggestion, and then Edward posted it already :rofl:

[Edward van de Meent]

great minds think alike :rolling_on_the_floor_laughing:

[Johan Commelin]

fools never differ... :thinking:

[Edward van de Meent]

i guess the question becomes if this is going to be a mathlib specific definition, or if we want to upstream this change to batteries, if batteries maintainers think this is a good idea

[Michael Rothgang]

#23767 is a prototype for this change: it might not build yet (then I'll need to add import Mathlib.Tactic.Basic; this is where I chose to stick the LibraryNote definition for now), and I have only replaced ~one sixth of the see note [library note name] references. That said: opinions on that change are welcome!

[Edward van de Meent]

i have some ideas for possible style requirements for library notes, if we make this change:

• all library notes should be in the LibraryNote namespace
• library notes should not become part of any declarations (so no putting def foo : Unit := LibraryNote.someNote) or such shenanigans. This could be tracked using linters?
• library notes should be marked protected, so it is clear whenever it is referred to that it is a note

[Johan Commelin]

Will protected play well with a potential #library_note fooBar? Or will we then need #library_note LibraryNote.fooBar?

[Edward van de Meent]

where #library_note is a command adding the note or searching for the note?

[Edward van de Meent]

if it's the first, i imagine we can just make it a macro. if it's the second, i imagine that would just be written #check LibraryNote.[autocomplete]

[Johan Commelin]

When referencing the library note.
At the moment we have See LibaryNote.fooBar as a substring of other docstrings. But then you can't get the hover text.
So I'm imagining that we just leave a #library_note fooBar next to the docstring instead.

[Johan Commelin]

Edward van de Meent said:

if it's the first, i imagine we can just make it a macro. if it's the second, i imagine that would just be written #check LibraryNote.[autocomplete]

Right, so it's the third (-;

[Edward van de Meent]

i don't think removing the reference from the docstring is very useful? i imagine it is commonly really part of the text, and i don't think there's a good place to add #library_note fooBar around a declaration which might reference it... Therefore, if it is going to be used, it's going to be written locally by the user when they want to check it, at which point you've rediscovered #help note. All of which is to say, it would really just be a lot easier if the hovers do show up for declarations referenced in docstrings.

[Jovan Gerbscheid]

I don't see the need to change the current syntax too much. We could still have

library_note "name of note"/--
Actual note
-/

and then referring to the note could become

#see_note "name of note"

And we could have an environment extension with a HashMap String String to keep track of the notes.

To achieve the hovering and ctrl+clicking would just be a meta-programming excercise.

[Edward van de Meent]

this is what currently exists

[Jovan Gerbscheid]

Except for the #see_note command that allows hovering to see the note, and ctrl+clicking to go to the note.

[Jovan Gerbscheid]

And I propose replacing all occurences of -- see note [name of note] by #see_note "name of note"

[Edward van de Meent]

well... since #help note "name of note" calls logInfo, i think it does get a hover displaying the contents of the note?

[Edward van de Meent]

try it out:

import Mathlib

#help note "low"

[Jovan Gerbscheid]

That's very nice. The only thing missing is ctrl+click to go the the library note.

And I don't like the name #help note for something that lives in Mathlib permanently, since it suggests a call for help. So rather something similar to -- see note

[Edward van de Meent]

welllllll this was a whole discussion when i wrote this command

[Edward van de Meent]

and the batteries maintainers insisted upon it

[Jovan Gerbscheid]

So what was the discussion about? Is there a disadvantage to ctrl+click?

[Edward van de Meent]

no, the name

[Edward van de Meent]

i do agree that ctrl+click would be beneficial to have, but i don't know how one might implement it

[Edward van de Meent]

particularly since you're not adding a declaration if you just store the info in an environment extension

[Jovan Gerbscheid]

The name #help makes sense for its current use, which is to have a user type this out to ask for help. However in the use that I'm envisioning, it's just a reference, so #see_note makes more sense.

[Jovan Gerbscheid]

Edward van de Meent said:

particularly since you're not adding a declaration if you just store the info in an environment extension

Yeah, we could secretly add some declaration to help with this, but a more principled way would be to store the Lean.DeclarationLocation in the environment extension.

[Edward van de Meent]

again, i agree with you there, so let me tell you more about approximately how this came to be:

• be me, can't find library notes
• decide to make a command which displays them
• make such a command, named #find_note or #check_note
• get feedback saying "maybe it's also nice if it just displays all of the notes with the provided prefix, instead of just the ones which match exactly"
• implement this
• get feedback saying "this really is a lot like #help attr" and other help commands, so it should be a #help command
• reluctantly change the name

[Edward van de Meent]

which is to say, since a #see_note command is made redundant by the #help note command, no such command exists

[Jovan Gerbscheid]

Maybe #see_note isn't fully redundant.

1. #help note "nam" will also show notes where the name starts with "nam". But I want #see_note to only show the exact note it refers to.
2. #help note logs a message, but if we will have #see_note permanently in mathlib, it shouldn't log a message (but still have a hover message). Or maybe it can show a message in the infoview only if the cursor is on it?

[Jovan Gerbscheid]

And for #see_note "name of note", we could also have hovering over "name of note" show the note, while hovering over #see_note gives information about library notes, and about the commands #see_note and #help note. This would massively improve the discoverability.

[Edward van de Meent]

i don't believe there is a nice way to use #see_note when relevant, in a way that it can stick around in mathlib... i believe that these references need to be in the docstring, not next to it.

[Edward van de Meent]

and if someone wants to know the content, they can use #help note, or if we proceed with the earlier suggestion, #check LibraryNote.foo

[Jovan Gerbscheid]

I don't know, but all I see in mathlib is -- See note [lower instance priority], which very much can be replaced by #see_note "lower instance priority".

[Jovan Gerbscheid]

And as long as we can't have hovers or ctrl+click inside of docstrings, I think a #see_note command is a clear improvement.

[Eric Wieser]

Maybe it's worth pointing out that VSCode exposure of notes is only half the problem, we also want them visible and linked in doc-gen like they were in Lean 3

[Jovan Gerbscheid]

Right, so then I think referring to them via a command would be a good first step. Although I don't know how lean 3 did it.

[Eric Wieser]

Lean 3 had native support for library notes in the vscode extension and doc-gen

[Edward van de Meent]

Where the native support in the extension was, apparently, just a regex

[Michael Rothgang]

Let me try to summarize the discussion. We are talking about four distinct operations.

• (1) define a new library note
• (2) reference a library note in other files
• (3) view a library notes/search for library notes
• (4) expose library notes in the generated documentation

As I understand it, the current status is:

• (1) use #library_note /-- definition -/ in the relevant mathlib file. This works well enough.

• (2) done manually using See note [lower instance priority]
  Issues: to see the note's content, you need to #help note "lower" separately. You cannot use go to definition (neither on the doc-string nor on the help output). The generated documentation does not

• (3) #help note lower does this; hovering over the output shows the note. No go-to-definition.

• (4) completely missing; not ported form Lean 3

Issues with the current design:

• finding the definition of notes: just searching for "[lower instance priority]" yields too many hits; you need to know about #help note. And even then, you will only find the library notes imported so far. (Requiring library note references to be imported upon reference would help.)
• show a note: #help note "lower" shows the note upon hover (nice), but you cannot go to definition.
• the generated documentation does not show library notes at all (that feature was not translated)
• documentation references "see note [lower instance priority]" do not point anywhere.

Is this a complete summary so far? If so, I'll look at the various proposals in this thread next.

[Edward van de Meent]

I think that's about right

[Edward van de Meent]

I think that's about right

[Edward van de Meent]

Modulo the precise syntax of #help note

[Edward van de Meent]

I think that's about right

[Edward van de Meent]

Modulo the precise syntax of #help note

[Michael Rothgang]

Proposal 1: a #see_note command

Remove references in the docs, and add a command #see_note lowerInstancePriority (or perhaps #see_note "lower instance priority") instead.
That command would (1) check that the relevant library note exists (resolving the discovery/imports problem), (2) show hover text (by re-using the logic of #help note).

Migration effort: all documentation references (so ~1500 lines, but fairly automatable; can be done incrementally)

Advantanges

• Solves the imports/discovery problem; prevents typos
• Go to definition is still missing.

Disadvantage: documentation handling needs custom handling in doc-gen --- both for displaying the library notes and showing references to them.

Open questions: should this live in batteries also? And should this re-use #help note, or replace it?

[Michael Rothgang]

Proposal 2a: make library notes a definition

Create a new type LibraryNote - which is a Unittype, whose doc-string will be the note's contents. #23767 prototypes this.

Migration effort: all library notes (done already, < 100 lines diff overall) + modifying #help note
(Plus migrating library note references: part of proposal 2b; similar to proposal 1.)

Advantages

• solves the "definition" half of the imports/discovery problem; prevents typos
• hovers and go to definition are included
• doc-gen displays library notes "for free"

Disadvantages

• syntax changes, migration effort
• is this necessary? can the #library_note command also achieve this? (Yes, it can. But that requires work elsewhere.)

[Michael Rothgang]

Proposal 2b: additionally, change library notes in doc-strings

Change library note references to See LibraryNote.lowerInstancePriority in doc-strings.

Migration effort: all documentation references (similarly automatable to the above)

Advantages

• doc-gen will allow go to definition in the generated documentation for free

Disadvantages

• cannot hover over a doc-string to show a library note (but could do #check LibraryNote.lowerInstancePriority and hover over 'that' output)
• import problem for library note references unsolved

[Michael Rothgang]

#23767 implements proposal 2a; #23786 also implements most of 2b.

[Michael Rothgang]

Is that a fair summary of the above? If not, please add points I forgot!

[Johan Commelin]

To me it seems that proposal 2a lets us piggy-back on a lot of existing infrastructure, instead of building bespoke versions.

[Jovan Gerbscheid]

For proposal 2, we can still have a macro library_note nameOfNote that expands to def LibraryNote.nameOfNote : LibraryNote := ()

[Damiano Testa]

A minor point on naming: if there ends up a custom command for flagging library notes, the command should probably not start with #, since there is a fairly widespread convention that commands starting with # are transient and not intended to stay in final code (and the hashCommand linter will flag them).

[Damiano Testa]

So, I would suggest using something like see_note, as opposed to #see_note, if that ends up being the final implementation.

[Michael Rothgang]

I have now pared #23767 down to step 2a, i.e. making library notes a definition. I have a macro library_note nameOfNote that expands to def LibraryNote.nameOfNote : LibraryNote := ()- but would like to extend that to add in the doc-string. Help with that is welcome, feel free to push right to my branch.

[Jovan Gerbscheid]

What's wrong with just writing the docstring above library_note nameOfNote?

[Yaël Dillies]

Jovan Gerbscheid said:

What's wrong with just writing the docstring above library_note nameOfNote?

In fact that's exactly how I envisioned Lean 4 would do it, before I saw the actual syntax

[Michael Rothgang]

Try it: writing

/-- test -/
library_note /-- test -/ `lowerInstancePriority

will error with unexpected token 'library_note'; expected 'lemma'.

[Yaël Dillies]

Well I assume that Jovan's question doesn't call for the answer "Because that's not how it's done right now" :sweat_smile:

[Jovan Gerbscheid]

Yes, I meant to implement and use the library_note nameOfNote macro in your PR #23767.

[Jovan Gerbscheid]

Jovan Gerbscheid said:

For proposal 2, we can still have a macro library_note nameOfNote that expands to def LibraryNote.nameOfNote : LibraryNote := ()

This one

[Yaël Dillies]

Can't wait for exact? to return Try this: exact lowerInstancePriority

[Jovan Gerbscheid]

That's a separate problem that already exists, where exact? gives suggestions appearing inside stuff like the Tactic namespace (or lemmas used for omega). So we would have to exclude those and also the LibraryNote namespace.

[Damiano Testa]

Michael Rothgang said:

Try it: writing

/-- test -/
library_note /-- test -/ `lowerInstancePriority

will error with unexpected token 'library_note'; expected 'lemma'.

Something like this works

import Mathlib

def LibraryNote := Unit

open Lean

-- XXX: how to add the doc-string into the generated macro?
macro dc:docComment " library_note " name:ident : command =>
  `($dc:docComment def $(mkIdent (Name.append `LibraryNote name.getId)) : LibraryNote := ())

/-- hello -/ library_note D

/-- info: hello -/
#guard_msgs in
run_cmd
  let env ← getEnv
  if let some doc := ← findDocString? env `LibraryNote.D then
    logInfo doc

[Damiano Testa]

Although probably the command should make LibraryNote be the "outermost" namespace of the library note?

[Yaël Dillies]

And maybe it should be declared an implementation detail?

[Jireh Loreaux]

I think this is one of those things that it makes sense to put in the Mathlib namespace. Other repos can also have LibraryNotes since this is/will be in Batteries.

[Jireh Loreaux]

That is, I'm advocating for Mathlib.LibraryNote.nameOfNote or even ⟨LakeProjectName⟩.LibraryNote.nameOfNote

[Aaron Liu]

Damiano Testa said:

A minor point on naming: if there ends up a custom command for flagging library notes, the command should probably not start with #, since there is a fairly widespread convention that commands starting with # are transient and not intended to stay in final code (and the hashCommand linter will flag them).

Really? What about #guard_msgs?

[Jireh Loreaux]

I think material specific for tests is exempt from this requirement.

[Michael Rothgang]

Damiano Testa said:

Michael Rothgang said:

Try it: writing

/-- test -/
library_note /-- test -/ `lowerInstancePriority

will error with unexpected token 'library_note'; expected 'lemma'.

Something like this works

import Mathlib

def LibraryNote := Unit

open Lean

-- XXX: how to add the doc-string into the generated macro?
macro dc:docComment " library_note " name:ident : command =>
  `($dc:docComment def $(mkIdent (Name.append `LibraryNote name.getId)) : LibraryNote := ())

/-- hello -/ library_note D

/-- info: hello -/
#guard_msgs in
run_cmd
  let env ← getEnv
  if let some doc := ← findDocString? env `LibraryNote.D then
    logInfo doc
`````

Ah, the `:docComment`was the missing part, I think!

[Edward van de Meent]

In order to somewhat maintain backwards compatibility, can we keep the doc-comment after library_note?

[Yaël Dillies]

I don't know, it's very off with all the other syntaxes, plus library_note is only used in mathlib as far as I'm aware

[Jz Pan]

Michael Rothgang said:

Proposal 1: a #see_note command

Remove references in the docs, and add a command #see_note lowerInstancePriority (or perhaps #see_note "lower instance priority") instead.
That command would (1) check that the relevant library note exists (resolving the discovery/imports problem), (2) show hover text (by re-using the logic of #help note).

Migration effort: all documentation references (so ~1500 lines, but fairly automatable; can be done incrementally)

Advantanges

• Solves the imports/discovery problem; prevents typos
• Go to definition is still missing.

Disadvantage: documentation handling needs custom handling in doc-gen --- both for displaying the library notes and showing references to them.

Open questions: should this live in batteries also? And should this re-use #help note, or replace it?

You can let #see_note command injects a custom module docstring (/-! ... -/) to current place.

[Michael Rothgang]

Edward van de Meent said:

In order to somewhat maintain backwards compatibility, can we keep the doc-comment after library_note?

I independently reached the same conclusion, for slightly different reasons: with a long library note, having some trailing identifier after the doc-string feels more confusing than helpful.

[Michael Rothgang]

#23767 is updated with the recent discussions: doc-strings are integrated, library notes are in the Mathlib.LibraryNote namespace, everything uses the macro. From my side, the main remaining question is "should we change the definition in batteries instead"/ do we need some kind of backwards compatibility there? (For now, I used a library_note2 command, which is not great.)

[Michael Rothgang]

Once this thread has converged on the details for proposal 2a; I'll re-examine proposals 1 and 2b.

[Mario Carneiro]

Edward van de Meent said:

Where the native support in the extension was, apparently, just a regex

I would argue that the use of "just a regex" here actually results in a much better scenario, even better than what #see_note would give us, because it means you can use these comments anywhere, including in the middle of declarations or doc strings, and get go to def all the same. This is the part that is missing in lean 4

[Johan Commelin]

Until we get go-to-def on decl names in docstrings (-;

[Damiano Testa]

Aaron Liu said:

Damiano Testa said:

A minor point on naming: if there ends up a custom command for flagging library notes, the command should probably not start with #, since there is a fairly widespread convention that commands starting with # are transient and not intended to stay in final code (and the hashCommand linter will flag them).

Really? What about #guard_msgs?

Linters are special-cased with #guard_msgs, since they caused a bit of a headache with parsing multiple times the same command. See docs#Lean.Elab.Command.elabCommandTopLevel and this line in particular.

[Johan Commelin]

Michael Rothgang said:

Edward van de Meent said:

In order to somewhat maintain backwards compatibility, can we keep the doc-comment after library_note?

I independently reached the same conclusion, for slightly different reasons: with a long library note, having some trailing identifier after the doc-string feels more confusing than helpful.

This would be automatic with def LibraryNote := String.

Of course, then we wouldn't get tooltips to display the library note automatically...

[Jon Eugster]

I've only skimmed parts of the conversation, but if the syntax was something like

#add_note lowerInstancePriority My.declaration

you could use the existing infrastructure to append a note about that to the docstring of the declaration if desirable. I forgot the name of the command, is it #extend_doc or something?

[Michael Rothgang]

Johan Commelin said:

Michael Rothgang said:

Edward van de Meent said:

In order to somewhat maintain backwards compatibility, can we keep the doc-comment after library_note?

I independently reached the same conclusion, for slightly different reasons: with a long library note, having some trailing identifier after the doc-string feels more confusing than helpful.

This would be automatic with def LibraryNote := String.

Of course, then we wouldn't get tooltips to display the library note automatically...

Correct. But my impression is that having a macro generating the LibraryNote definitions also handles this.

[Michael Rothgang]

Jon Eugster said:

I've only skimmed parts of the conversation, but if the syntax was something like

#add_note lowerInstancePriority My.declaration

you could use the existing infrastructure to append a note about that to the docstring of the declaration if desirable. I forgot the name of the command, is it #extend_doc or something?

This is about the "how to refer to an existing library note in a declaration", right?

[Jon Eugster]

yes, about how to get the library note link into the hover in VSCode and into the docgen page for the declaration which has the note

[Michael Rothgang]

This thread seems to have stalled. It seems the first part ("proposal 2a") had no objections, and the only open questions are about 1/2b, i.e. referencing library notes. Can I ping #23767 (which implements the first part) for review again?

In terms of landing this, I'm envisioning (barring any reasons to change plans, as usual):

• review on the mathlib PR, to see if there are any substantial issues; that PR gets merged
• I'll make a PR to batteries, changing the definition of library notes to the proposed design in #23767
• a mathlib PR switches mathlib to the batteries definition
  This avoids complicated adaptations.

I'm happy to make the second two PRs, if there's an indication of support for this plan.