search

coq / coq.github.io

Source files of the coq.inria.fr website
https://coq.inria.fr/
Other
15 stars 37 forks source link

Rework documentation page, create more categories, mention MCB and dev doc. #97

Closed Zimmi48 closed 5 years ago

Zimmi48 commented 5 years ago

cc @palmskog: I'd like to add a mention of FRAP and PnP, can you help provide descriptions?

cc @ejgallego: This might be related to your effort in coq/coq#9824.

cc tutorial authors @casteran @ybertot @bcpierce00 @andrew-appel @achlipala @amahboubi @gares: you might be interested or have comments, sorry for the noise if that's not the case.

This is the result:

rework-doc-page

ejgallego commented 5 years ago

IMHO a more prominent "Getting started with Coq" could be cool.

gares commented 5 years ago

In the picture, the links at the bottom of the frame, in the book section, MCB is not there (not sure why we have 2 copies of each link in the first place).

my2c

Zimmi48 commented 5 years ago

IMHO a more prominent "Getting started with Coq" could be cool.

I agree but right now (and until coq/coq#9824 is finished), I wouldn't know what to put in there.

In the picture, the links at the bottom of the frame, in the book section, MCB is not there (not sure why we have 2 copies of each link in the first place).

We don't actually have 2 copies of each link: what we put at the bottom is a sub-selection of links. I'm not so fond of the current theme either, but until it is reworked, I try to stick with it more or less and to improve the content of the pages nonetheless. I didn't put MCB because I was not sure if I should be using the acronym or a longer name.

achlipala commented 5 years ago

I wouldn't mind having a FRAP link in that spot! I'm not sure what else is worth discussing, so I'll leave it at that.

Zimmi48 commented 5 years ago

Thanks for your suggestions Karl! I will review and integrate them tomorrow.

Zimmi48 commented 5 years ago

Given the long list of books now, should we think of a consistent ordering? For instance, by year? And what about the ones to highlight at the bottom?

books

bcpierce00 commented 5 years ago

It may also be useful to break out the separate volumes of Software Foundations as individual entries in this list: there are now four (shortly to be five), and they cover a range of different topics that might not be apparent from a single-sentence summary of the whole series.

palmskog commented 5 years ago

How about the following categories:

I don't know what the order should be, but personally I would like to see Coq'Art and Software Foundations vol. 1 listed first due to their generality.

palmskog commented 5 years ago

@Zimmi48 if the breakdown into separate lists for "introductory" and "advanced" (still within the "Books" box) sounds good, I can do a GitHub suggestion for that. I'd prefer that you greenlight the idea before I start writing up more summaries.

gares commented 5 years ago

Hum, to me advanced/basic is very subjective (and non trivial to maintain in the long term), while the year of publication/last-update seems easier to maintain and more objective.

For example CPDT is a text that, experts, read it and say "wow"; but I'm not so sure that "DT" fits the "beginner" kind of user. Why you placed it in the first category is unclear to me, while the publishing date would not be debatable.

Just my 2C, in any case, thanks for improving this page!

palmskog commented 5 years ago

@gares although there is some subjectivity for sure, I think there is a clear difference between the general books that start from scratch, as it were, and those that cover a specific application area. I called this "advanced", but we can use some other term.

One example is the difference between the books Introduction to Bisimulation and Coinduction and Advanced Topics in Bisimulation and Coinduction.

gares commented 5 years ago

Sure, that example is striking, but it is also an example for which a casual reader would need no classification in order to pick the most appropriate, if any. Also, the book I took as an example in my previous message, CPDT, contains the word "advanced" in the description, while you placed it in the first category, hence my reaction. Finally, I'm pretty sure MCB is not the only book that starts from scratch but also covers, at the very end, advanced topics, even if it is not split in volumes.

My impression is that the list of books is small enough that one can just go trough it, and what matters the most is to have a description that helps one pick the most appropriate one. If the description of SF is too short, I guess it can be fixed by saying it comprises 4 volumes covering this basic stuff and that advanced topic.

If the list of books grows too much then we shall find a better way to display it, but I don't think we are there yet.

Zimmi48 commented 5 years ago

Sorry I didn't go back to this PR for so long. I'm really too busy right now so if anyone wishes to finish it (either implementing Enrico's or Karl's proposal), I'd appreciate it.

Zimmi48 commented 5 years ago

I didn't really know how to proceed and I have left this PR idling for too long, so I've decided to just reorder by publication year for now and merge. Further refinements with categories, or splitting SF in several entries are welcome as further PRs.