coq-community / coq-100-theorems

Statements of famous theorems proven in Coq [maintainer=@jmadiot]
https://madiot.fr/coq100/
Other
55 stars 14 forks source link

fix all Coqtail references #18

Closed palmskog closed 4 years ago

jmadiot commented 4 years ago

I worry it would make the statements harder to understand: the previous links were pointing to coqdoc documentations where each identifier/notation has a link to its definition (to other files and to the stdlib), which I find very useful when trying to understand the statement. However the previous links were to an older version of coqtail, which, even though it does not really change much, is not ideal. I wonder if there is a standard and simple solution where we could get an automatically up-to-date documentation in coqtail-math? I'm sure it is possible in theory but I don't want it to be a mess (the way we had the documentation set up in coqtail was using coqdoc and then running a script on the generated files).

palmskog commented 4 years ago

The reason I link to the GitHub files is because they actually contain the proof scripts in executable form (i.e., are reproducible for proof checking), while copy-pasting coqdoc HTML invariably results in a mess. Moreover, unless one sets up coqdoc generation on each commit (which is possible but has many technical hurdles), the HTML is likely to be stale with respect to a modern version of Coq.

palmskog commented 4 years ago

@jmadiot we are working on automation for coqdoc generation, you can see the discussion here. However, this is still some time away, so my suggestion is to merge this in the meantime (to have canonical references) and circle back to this topic later.

jmadiot commented 4 years ago

I don't think people would consider copy-pasting HTML (even copy-pasting raw text rarely works due to required Requires) the documentation is for navigation, and finding the repository from the documentation is easy. Nevertheless I'll merge this and then maybe try to get a recent coqdoc version to provide an additional link.