Zulip Chat Archive

Stream: general

Topic: mathlib notes

Reid Barton (Sep 25 2019 at 17:21):

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 (Sep 25 2019 at 17:30):

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

Johan Commelin (Sep 25 2019 at 17:40):

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 (Sep 25 2019 at 17:41):

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

Johan Commelin (Sep 25 2019 at 17:41):

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

Reid Barton (Sep 25 2019 at 17:42):

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 (Sep 25 2019 at 17:45):

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 (Sep 25 2019 at 17:45):

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

Floris van Doorn (Sep 25 2019 at 17:54):

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

Simon Hudon (Sep 25 2019 at 18:30):

Do we need any tool support?

Reid Barton (Sep 25 2019 at 18:48):

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 (Sep 25 2019 at 18:49):

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

matt rice (Sep 26 2019 at 12:09):

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 (Oct 01 2019 at 17:35):

Added my first note

Yury G. Kudryashov (Oct 01 2019 at 19:14):

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

Simon Hudon (Oct 01 2019 at 19:28):

I don't think so

matt rice (Oct 06 2019 at 19:48):

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.

Last updated: Dec 20 2023 at 11:08 UTC