Cyril Cohen (Jan 27 2021 at 14:10): 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.
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.
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
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.
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.
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
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: )
Enrico Tassi (Jan 27 2021 at 14:17):(B & G are the initials of the authors of the first book)
Enrico Tassi (Jan 27 2021 at 14:18):#[cite(doi=".....",ref="13.1") ]
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
Cyril Cohen (Jan 27 2021 at 14:19):the doi is standard enough for papers I think, and isbn for books
Karl Palmskog (Jan 27 2021 at 14:19):most scientific books have DOIs these days I believe
Enrico Tassi (Jan 27 2021 at 14:19):yes, but repeating it before each theorem would make me puke
Cyril Cohen (Jan 27 2021 at 14:20):#[cite(abbrev="B&G")]
Enrico Tassi (Jan 27 2021 at 14:20):we need to craft something a bit smarter I'm afraid
Enrico Tassi (Jan 27 2021 at 14:20):sure, but where is the bib file ;-)
Cyril Cohen (Jan 27 2021 at 14:21):And somewhere a mathcomp.bib
Cyril Cohen (Jan 27 2021 at 14:21):that would make sense!
Enrico Tassi (Jan 27 2021 at 14:21):sure, but if you want Search to use that info...
Cyril Cohen (Jan 27 2021 at 14:21):I have dozens of standalone .bib files in many repos...
Cyril Cohen (Jan 27 2021 at 14:22):why coundn't search be "educated"
Cyril Cohen (Jan 27 2021 at 14:22):We need to boost the command anyway!
Enrico Tassi (Jan 27 2021 at 14:23):this is a good start: bibtex_parser.mly
Enrico Tassi (Jan 27 2021 at 14:23):This feature of Zulip is, hem...
Notification Bot (Jan 27 2021 at 14:26):This topic was moved by Cyril Cohen to #Miscellaneous > Zulip preview feature
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: Oct 13 2024 at 01:02 UTC