mathlib notes

Stream: general

[Reid Barton]

One practice I miss from GHC is the use of named "notes", as described here and also blogged about here. GHC has around 2000 of these notes.
I'd like to adopt this in mathlib. For example, in category theory we have a convention of declaring universe variables in a particular order; this needs to happen in every file and -- see Note [universe order in category theory] would be a convenient way to document each occurrence.
Since we currently have none of these notes, maybe it would be good to establish a conventional format, so that they're easy to search for.

[Floris van Doorn]

That seems useful!
So in GHC these notes are at the bottom of source files?

[Johan Commelin]

I think this is a good idea. I suggest that it should be easy to grep for the "definition" of the note, and for the references to the note.

[Johan Commelin]

In particular, it might be good to have a slight syntactical difference. Maybe just NoteDef [universe order ...] vs Note [universe order...]

[Johan Commelin]

Also, there shouldn't be line breaks in Note.*]

[Reid Barton]

The notes go can go near the top or end of a file, or near wherever they are most relevant, but never in the middle of a declaration

[Reid Barton]

Another way to be able to search for the "definition" of the note is to standardize on, say, /- Note [foo] appearing at the start of a line

[Reid Barton]

although that doesn't help if you want to search on github, since it doesn't support regular expression search

[Floris van Doorn]

I like --see [universe order] and /- Note [universe order], so remove the word "note" from the reference.

[Simon Hudon]

Do we need any tool support?

[Reid Barton]

I hope we don't need tool support, but if we had a conversion to hyperlinked HTML, for example, it would be nice to be able to hyperlink the notes also

[Reid Barton]

which might influence the choice of syntax, e.g., Floris's suggestion might not be easily recognizable as a note reference

[matt rice]

Hmm, looking at the markdown parser I use for parsing doc_strings,
It supports the pandoc footnote syntax, which seems to support a kind of citation mechanism according to this
However i haven't seen the parser exercised in the above way. [^fn1]

Anyhow consistency with doc_strings might be nice to consider.

[^fn1]: Its worth noting that this is an extension to the markdown specification, as such...

[Floris van Doorn]

Added my first note

[Yury G. Kudryashov]

Do we already have a way to convert markdown doc strings to html files?

[Simon Hudon]

I don't think so

[matt rice]

Will look into it for lumpy, initial stuff is done, but lacks syntax highlighting single line code blocks like foo → bar need work, latex in comments, linking, needs more work.