Stream: math-comp users

Topic: Documenting mathcomp theorems


view this post on Zulip Cyril Cohen (Jan 27 2021 at 14:10):

Reynald Affeldt said:

Should these be listed along the odd order theorem on the mathcomp webpage https://math-comp.github.io/?

Actually this is a very nice idea! Maybe not with the odd order theorem, but we should definitely have a list of results somewhere as they do in Lean.

view this post on Zulip Karl Palmskog (Jan 27 2021 at 14:12):

some MathComp theorems are already listed/linked at: https://madiot.fr/coq100/

would be useful if we could use similar info/URLs across that list and the (suggested) MathComp webpage list.

view this post on Zulip Karl Palmskog (Jan 27 2021 at 14:14):

another feature that would be very nice for machine learning: incorporate "famous names" of results as Coq annotations (or at least comments). For example, rank-nullity versions referenced above have names which give little hint that they are noteworthy

view this post on Zulip Cyril Cohen (Jan 27 2021 at 14:15):

I have been wanting annotations for theorems in the form of both docstrings and searchable strings (for the search command) for a while.

view this post on Zulip Cyril Cohen (Jan 27 2021 at 14:16):

Karl Palmskog said:

some MathComp theorems are already listed/linked at: https://madiot.fr/coq100/

Sure but that's not the point of my remark.

view this post on Zulip Enrico Tassi (Jan 27 2021 at 14:16):

In the OOthm we were quite precise in comments like this one https://github.com/math-comp/odd-order/blob/19eb998e2d08c21c6e61806cc7b588238629757e/theories/BGsection13.v#L43
Maybe we should propose some sort of standard format for these

The formal proof of the Odd Order Theorem. Contribute to math-comp/odd-order development by creating an account on GitHub.

view this post on Zulip Cyril Cohen (Jan 27 2021 at 14:17):

Now there are attributes we could have a doctring attribute and as well as alternative_pattern.
(But it requires attributes to be correctly ignored :laughing: )

view this post on Zulip Enrico Tassi (Jan 27 2021 at 14:17):

(B & G are the initials of the authors of the first book)

view this post on Zulip Enrico Tassi (Jan 27 2021 at 14:18):

#[cite(doi=".....",ref="13.1") ]

view this post on Zulip Enrico Tassi (Jan 27 2021 at 14:19):

I'm no energy for that, but if someone digs for a "standard" way of pointing to papers/chapters/sections/.... it is trivial to implement

view this post on Zulip Cyril Cohen (Jan 27 2021 at 14:19):

the doi is standard enough for papers I think, and isbn for books

view this post on Zulip Karl Palmskog (Jan 27 2021 at 14:19):

most scientific books have DOIs these days I believe

view this post on Zulip Enrico Tassi (Jan 27 2021 at 14:19):

yes, but repeating it before each theorem would make me puke

view this post on Zulip Cyril Cohen (Jan 27 2021 at 14:20):

#[cite(abbrev="B&G")]

view this post on Zulip Enrico Tassi (Jan 27 2021 at 14:20):

we need to craft something a bit smarter I'm afraid

view this post on Zulip Enrico Tassi (Jan 27 2021 at 14:20):

sure, but where is the bib file ;-)

view this post on Zulip Cyril Cohen (Jan 27 2021 at 14:21):

And somewhere a mathcomp.bib

view this post on Zulip Cyril Cohen (Jan 27 2021 at 14:21):

that would make sense!

view this post on Zulip Enrico Tassi (Jan 27 2021 at 14:21):

sure, but if you want Search to use that info...

view this post on Zulip Cyril Cohen (Jan 27 2021 at 14:21):

I have dozens of standalone .bib files in many repos...

view this post on Zulip Cyril Cohen (Jan 27 2021 at 14:22):

why coundn't search be "educated"

view this post on Zulip Cyril Cohen (Jan 27 2021 at 14:22):

We need to boost the command anyway!

view this post on Zulip Enrico Tassi (Jan 27 2021 at 14:23):

this is a good start: bibtex_parser.mly

Contribute to backtracking/bibtex2html development by creating an account on GitHub.

view this post on Zulip Enrico Tassi (Jan 27 2021 at 14:23):

This feature of Zulip is, hem...

view this post on Zulip Notification Bot (Jan 27 2021 at 14:26):

This topic was moved by Cyril Cohen to #Miscellaneous > Zulip preview feature

view this post on Zulip Cyril Cohen (Jan 27 2021 at 14:27):

Enrico Tassi said:

this is a good start: bibtex_parser.mly

Sure but I was thinking about way more than just citing.
I want to have an index of math standard results to link to mathcomp documentation.


Last updated: Feb 08 2023 at 07:02 UTC