coq / coq.github.io

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

Make it easier to get Coq. #202

Closed Zimmi48 closed 2 years ago

Zimmi48 commented 2 years ago

Following a point made by Pierre Rousselin on the private mailing list gt-maths-coq, this PR makes two small modifications to the website to make it clearer how to get Coq.

  1. Do not mention the "Platform" on the homepage because prospective users do not know yet what it is and there is no space to explain.
  2. On the download page, clarify what is the recommended installation method for beginners, including for those who do not want to read the page closely.
  3. This is outside the scope of this PR: the third change should be in the formatting of the Coq Platform releases (cc @MSoegtropIMC). We should insert three prominent links at the top of the GitHub releases pointing to the Windows (64 bit) installer, the macOS installer, and the Snap package. Something like:

    ### Recommended binary installers
    
    - [Windows (64 bit) installer for Coq 8.15](https://github.com/coq/platform/releases/download/2022.04.1/Coq-Platform-release-2022.04.1-version_8.15_2022.04-arch-x86_64_signed.exe)
    - [macOS installer for Coq 8.15](https://github.com/coq/platform/releases/download/2022.04.1/Coq-Platform-release-2022.04.1-version.8.15.2022.04-signed.dmg)
    - [Linux (Snap) installer for Coq 8.15](https://snapcraft.io/coq-prover)

    Currently, there is a lot of text and the installers are at the bottom, and even then, there are too many of them, thus it is too difficult for a prospective user to know what to install.

Screenshots

Homepage

image

Download page

image

MSoegtropIMC commented 2 years ago

It might make sense to leave a few words on working with opam directly. Something like:

"If you are already using opam, the OCaml Package Manager, you can also install coq directly via opam. There is nothing wrong with that, but the common basis provided by Coq Platform makes it easier for others to use or reproduce your work and to maintain your work long term."

Zimmi48 commented 2 years ago

@MSoegtropIMC Probably you are missing out on the context. I have only put screenshots of the parts I changed, but the download page already contains the "Other installation methods" section that talks about opam and which I haven't touched. See https://coq.inria.fr/download.

MSoegtropIMC commented 2 years ago

@Zimmi48 : I wanted to emphasize a bit what the downsides are - it is not only to get it working for you (as said in the existing text) - IMHO the larger problem of not using platform is that people make it harder for others to reuse their work. This is not a problem at all if you do SF homework, but it starts to be a problem e.g. for thesis work. I think it is hard to make proper judgments without such information.

Zimmi48 commented 2 years ago

OK, but this is out of the scope of this PR* which was aiming to help beginners know what the default recommended installation method is. And I'd like BTW to hear what you think of point 3 above which is outside what this PR can change.

*Unless we rework this page even more to make a section "Beginners" followed by a section "Experienced users", in which case the section for experienced users could emphasize what are the benefits of the Coq Platform compared to the other methods (this would go beyond the time I can allocate to this in the short-term, but I'm happy to leave someone else do these changes). Cc @gares and @palmskog BTW.

MSoegtropIMC commented 2 years ago

@Zimmi48 : OK, let's do it later then. Regarding the Platform release notes: sure we can do this. I tend to copy the previous notes and edit them, so if this is done once, it will be like this. I would say it is best you just edit the notes for the next release (will come soon).

Zimmi48 commented 2 years ago

What about editing the notes of the current one now? The next release is going to be a beta, so there's going to be some more delay before it is the one that is shown to users by default, isn't it?

MSoegtropIMC commented 2 years ago

@Zimmi48 : please go ahead and edit the notes for the 2022.04 release - let me know when you are done. I copied the status quo and compare when you are done.

Zimmi48 commented 2 years ago

Done. I've just inserted my suggestion on top. I'll also merge this PR.

MSoegtropIMC commented 2 years ago

@Zimmi48 : thanks! Your changes to the release notes look good to me.