search

coq / coq.github.io

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

update opam-using.html since opam-depext is no longer used #185

Closed Alizter closed 2 years ago

Alizter commented 2 years ago

hopefully addresses #175

fixes #175

I don't currently have a way of checking that this is really how it works, I am writing the doc from memory. Perhaps someone who has installed coq a few times recently can chip in. cc @MSoegtropIMC

MSoegtropIMC commented 2 years ago

IMHO the instructions should address both, opam 2.0.X and opam 2.1. Some people install opam via system packages and especially on unix distributions it might take a while until the majority ends up with opam 2.1 this way.

Otherwise one should explain how to install opam 2.1 on any systems (via the opam installation script).

Alizter commented 2 years ago

Alright, I've gone ahead and recommended opam 2.1, and also mentioned that opam 2.0 can be used, but like for differing operating systems, external packages will have to be installed manually. I've also added a little help section at the end, linking to our communication channels.

Alizter commented 2 years ago

@Zimmi48 I've rewrapped the file and taken your suggestions into account. The diff might be noisy, but they are in separate commits for easier review.

MSoegtropIMC commented 2 years ago

Can I somewhere see the full compiled text? It would make it easier for me to review.

Zimmi48 commented 2 years ago

Can I somewhere see the full compiled text? It would make it easier for me to review.

You would need to check out the PR and run make && make run (see the README in this repository). This is what I usually do to review changes in this repo.

Alizter commented 2 years ago

OK, I'll address the wrapping problems later since I'm out of time today. I think it's mostly making sure the code blocks are kept in check. Overall, I think the page is still a bit word heavy for a first-time-using-opam tutorial.

Alizter commented 2 years ago

What do you think about the overall flow @Zimmi48 is it worth merging or shall we spend some more time later making it more lean?

Zimmi48 commented 2 years ago

IMHO, the document is not so wordy if you consider only the parts you are interested in. I don't know how we could make it shorter. In any case, this should be considered as improvements to do later on. In the meantime, this is an important reference, so the PR should be worth merging as is.

Alizter commented 2 years ago

@Zimmi48 OK feel free to merge then

Zimmi48 commented 2 years ago

OK further improvements / refinements can come in other PRs if needed.