Website simplification and Coq platform update.

[Zimmi48]

This is a major update to the website home page and Coq installation pages to put the focus on the Coq platform installation method (cc @gares @MSoegtropIMC). It also reduces the importance of the current version number on the website in relation with CEP#52 (but we still need it, mostly in the opam using page). For the homepage, I also tried to think at what we would like to put forward if the design of the website was reworked, but without doing any change to the design yet.

The diff for the index page and the download page might be a bit hard to follow, so here are some preview screenshots:

cc @jfehrle (I cannot request a review from you on this repository)

[Zimmi48]

Note that for now, "Binary installers (Windows and macOS)" still link to the Coq GitHub release page, but we may need to update this to point to the Coq platform repository instead in the future.

[Zimmi48]

Another note is that we should get major user interfaces compatible with the Snap package (cf. https://github.com/coq-community/vscoq/issues/192 for VsCoq) before actively recommending the Snap package like this update does.

[Zimmi48]

Also cc @CohenCyril: I point to Nix as an alternative advanced method and link to the nixpkgs-unstable manual.

[gares]

Many thanks for the update!

[gares]

Not sure I love the page layout though.

A "refresh" of the webpage style was planned by @maximedenes (to be outsourced to professionals). While I could not agree more with you Jim on this point, I think this PR should focus on the contents.

[gares]

@Zimmi48 FYI the snap package page has a button to generate html code for pointing to the package (a badge). Maybe it's not good for this page, but if you decide to make sub pages, then it may have its place.

Maybe I'm the only one that sees it being admin, in that case I can give you the pwd to look at the preview.

[MSoegtropIMC]

@Zimmi48 : one thought: should we put this online before a Coq Platform 8.13.0.0 is published? I had a discussion on this with @gares. Essentially the options are:

• Publish Coq Platform 8.13.0.0 now with the traditional feature set (this is tested to work) and publish 8.13.0.1 with extended feature set in one month.
• Publish Coq Platform 8.13.0.0 with an extended feature set in one month.

Since we are in a transitional situation I would tend to the first option, but @gares preferred the second. I think we both don't have very strong opinions on this, but this should be coordinated with this PR.

[Zimmi48]

Maybe I'm the only one that sees it being admin, in that case I can give you the pwd to look at the preview.

I noticed it but it looked too heavy for this page.

[Zimmi48]

Since we are in a transitional situation I would tend to the first option, but @gares preferred the second. I think we both don't have very strong opinions on this, but this should be coordinated with this PR.

I would also prefer the first option.

[gares]

One thing I don't like much is to have two platforms for the same coq release with different feature sets. The 4th digit becomes very important then, to answer the question "is package X in the platform for 8.13". This is probably why I preferred option 2, but it goes in hand with the meaning of that digit. And for the records, I'm also a bit skeptical about inheriting the third digit from Coq (what 8.13.1.0 means? does it have the same features of 8.13.0.1 or 8.13.0.0?)

[gares]

. I think we both don't have very strong opinions on this, but this should be coordinated with this PR.

+1

[MSoegtropIMC]

One thing I don't like much is to have two platforms for the same coq release with different feature sets.

The idea is that the content only ever increases, so that 8.13.1.0 will have the same or larger content than 8.13.0.1. We just need some efficient way to add packages without delaying this too long and it is not unlikely that the Coq platform will need more maintenance releases than Coq itself - that's the reason for the 4th digit.

What I plan is to have one more level (the first question the script asks, coq only, ide or full) called "extended", but I didn't plan as yet what goes in what level and if "full" should be renamed to "standard" or "default".

[Zimmi48]

Yes, the standard vs extended set is a good idea. I agree with the versioning scheme concern, but we should probably move this discussion somewhere else -> coq/platform#22.

[jfehrle]

FWIW, one way to facilitate reviewing website updates is to temporarily make the new material available on a non-standard TCP port or under a different DNS name, which reviewers can include in their URL while others won't find it. This may be easy or way too much work depending on the web site technology.

[Zimmi48]

FWIW, one way to facilitate reviewing website updates is to temporarily make the new material available on a non-standard TCP port or under a different DNS name, which reviewers can include in their URL while others won't find it. This may be easy or way too much work depending on the web site technology.

Unfortunately, the current infrastructure is a big mess. So this is not an option until it is replaced by something simpler. But reviewers can also check out the branch and run make && make run to get a preview, with just a few links broken (only OCaml and Python are needed).

[Zimmi48]

Would be fun to add a photo to add interest. How about this one (a free image from https://www.pexels.com/search/chicken/)?

I like this idea but consider it part of design, so to keep for later.

[jfehrle]

I noticed 2 other typos in documentation.html:

ressources targetted

[Zimmi48]

@gares PR updated.

Two remarks:

• the links to the Coq platform are to https://github.com/coq/platform, but it could also be to https://github.com/coq/platform/releases
• the links to the Windows & macOS binary installers still point to https://github.com/coq/coq/releases/latest since this is anyway the only place where to find a macOS installer and the Windows installer should be mostly identical to the platform ones. The idea is to update this once all the installers can be found on the releases page of the platform.

[Zimmi48]

Following @MSoegtropIMC remark, I will update the PR to point to https://github.com/coq/platform/releases rather than https://github.com/coq/platform.

[Zimmi48]

Done. PS: @MSoegtropIMC, I think the platform scripts should be advertised more clearly from the releases page. The natural way to do this would be to copy the beginning of the usage section in the release notes:

Please refer to the ReadMe file for your OS.

• macOS: see README_macOS.
• Windows: see README_Windows
• Linux: see README_Linux.

It would also be natural to include the complete list of packages and their versions in the release notes.

[MSoegtropIMC]

@Zimmi48 : yes, I can definitely improve on the release notes. Currently CI for the version bumping + readme adjustment PR is running, so I will do the tag tomorrow. It would be great if we could discuss the release message tomorrow morning.

[Zimmi48]

With the change of default branch, it doesn't seem as useful as before to point to the releases section rather than the main repo page, so I'll revert this update to the previous version and merge.