search

coq / coq.github.io

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

Apply feedback from Rajeev Gore on Coq-Club. #138

Closed Zimmi48 closed 4 years ago

Zimmi48 commented 4 years ago

I applied some suggestion from a recent Coq-Club user who had trouble following the opam instructions. I am submitting this for review though, because I am not myself an opam user.

Regarding the m4 package, is it frequent that this is not installed by default?

@Lysxia or @palmskog or anyone else that is experienced with opam: would you mind reviewing this PR?

Zimmi48 commented 4 years ago

However, it should also work on a wide assortment of distributions, and maybe even MacOS?

Indeed, I think so.

I'm not really fond of this PR

As I said, I am not an opam user myself so it is a bit hard to know what should be said and what should not. All I notice is that we keep getting users asking basic questions after following the instructions on this page, so something should likely still be improved.

I tried highlighting further the need for opam 2 (because most Ubuntu versions still contain opam 1.2, this seems like a common issue), clarifying that Coq is built from sources, and indeed that there may be external dependencies.

I do like your suggestion of recommending opam-depext better than talking about m4 and apt. May I ask you to push an edit to the PR to better fit your taste? (I could do this myself as well, but I am not sure how many rounds of feedback would be needed then.)

palmskog commented 4 years ago

@Zimmi48 OK, I can do a quick pass over the PR, if you do a quick review of the results (and merge if it looks good).

Zimmi48 commented 4 years ago

Sounds good!

palmskog commented 4 years ago

@Zimmi48 I finished a pass, but I don't seem to have access rights to push to your branch (and hence this PR). Should I push elsewhere?

Zimmi48 commented 4 years ago

Oh! That's because you don't have write-access ot this repo. I'll add you as a collaborator so that you can push.

Zimmi48 commented 4 years ago

Instead, I've created the new team @coq/website-maintainers and added you to this team (with write-access to this repo for this team), since it is likely that we will want to add more people to it, and this will make things more straightforward.

palmskog commented 4 years ago

Thanks @Zimmi48, I pushed the revision now. Could you take a look and (possibly) merge?

Zimmi48 commented 4 years ago

Very nice improvements, thank you very much!