Marie Kerjean (Oct 23 2020 at 08:03): Marie Kerjean (Oct 23 2020 at 08:03):The recommended way to install Coq and its libraries is through opam. However, this makes it difficult to consult the libraries locally. Taking the example of a new user trying to master the MathComp library, the easiest way to do so seems to be to consult them on github and copy the code. Is there a way to install the library in an easy to access repository ? Or should the user simply clone the library and write his own makefile ?
Christian Doczkal (Oct 23 2020 at 09:10):I would say that installing Coq and libraries via opam is the preferred way if you want to develop something on top of existing stable releases. Going with your example of mathcomp, I built stuff on mathcomp for a long time by just installing it and then using the HTML documentation from the website.
For experimenting and contributing to mathcomp, I use a dedicated opam switch that has basically only coq.dev installed and then work on a local copy of my github fork of the math-comp repository that has both the official repo and my for as remotes to pull from upstream and push to my fork. This makes it very easy to create PRs for mathcomp. Just push the branch to your fork and click on the link the command-line client spits out after the push.
Christian Doczkal (Oct 23 2020 at 09:13):This is to avoid the issues arising from compiling libraries locally that are already installed
Karl Palmskog (Oct 23 2020 at 09:35):using the master branch of MathComp on GitHub, whether to build something new or not, is to me already an advanced task not recommended for most users. (Same goes for using the dev opam packages, which can yield something similar.)
Karl Palmskog (Oct 23 2020 at 09:41):personally, I think nearly everyone should be recommended to use the latest stable Coq and the latest stable release of whatever library they need, and develop completely on top of those as already mentioned. Ideally, each stable package should have its own online HTML documentation like Stdlib does (opam has a field doc for this)
Emilio Jesús Gallego Arias (Oct 23 2020 at 09:49):Unfortunately I think OPAM does not cover @Marie Kerjean use case very well, if I understand correctly; when I was learning math-comp indeed I kinda wanted to have the library in my context as indeed very often you need to check existing proofs [for inspiration ;) etc...]
Emilio Jesús Gallego Arias (Oct 23 2020 at 09:50):I think that Dune does cover that use case pretty well, you can just drop the desired mathcomp folder in your environment and things should work out of the box.
Théo Zimmermann (Oct 23 2020 at 10:05):Does it though? I thought that compositionality was not yet support inter-projects?
Théo Zimmermann (Oct 23 2020 at 10:05):Otherwise, I would have suggested this as well.
Karl Palmskog (Oct 23 2020 at 10:07):as probably one of the top users of Dune-for-Coq, I can say that we are quite far from just throwing something inside an environment and making it work like what Emilio suggests
Emilio Jesús Gallego Arias (Oct 23 2020 at 10:08):Why do you think we are so far @Karl Palmskog ? I need to submit the patch, but it is almost ready. Most complications arise due to the high cost of scanning user-contrib to see what was available but I've fixed that.
Emilio Jesús Gallego Arias (Oct 23 2020 at 10:09):Other than that the missing code is simple as we don't have private libs, etc... which complicates the things a lot
Emilio Jesús Gallego Arias (Oct 23 2020 at 10:09):it is true that the library model is a tad more restrictive for now [in terms of overloading] but that shouldn't matter much in practice
Karl Palmskog (Oct 23 2020 at 10:09):we may not be far in principle, but you need to have all libraries catch up, in particular mathcomp itself has no dune files
Emilio Jesús Gallego Arias (Oct 23 2020 at 10:09):well there was a PR submitted quite a few time ago
Emilio Jesús Gallego Arias (Oct 23 2020 at 10:10):we use that files regularly , for example in jscoq addons
Emilio Jesús Gallego Arias (Oct 23 2020 at 10:10):all addons are required to use dune
Karl Palmskog (Oct 23 2020 at 10:12):I would expect a similar story for other big libraries: a PR can be whipped up, but will not be merged right away and will coexist with existing build scripts for some time and encounter issues
Karl Palmskog (Oct 23 2020 at 10:15):CoqHammer was one of the most challenging projects I've ever dunerized, and there the main developer prefers coq_makefile for local development going forward, so Dune maintenance will be challenging
Paolo Giarrusso (Oct 23 2020 at 10:51):I think that Dune does cover that use case pretty well, you can just drop the desired
mathcompfolder in your environment and things should work out of the box.
Paolo Giarrusso (Oct 23 2020 at 10:51):Why do you think we are so far Karl Palmskog ? I need to submit the patch, but it is almost ready.
Paolo Giarrusso (Oct 23 2020 at 10:53):So any ETA on when things will work out of the box?
Emilio Jesús Gallego Arias (Oct 23 2020 at 10:55):For this feature 2.8 seems very feasible
Marie Kerjean (Oct 23 2020 at 12:18):Emilio Jesús Gallego Arias said:
Unfortunately I think OPAM does not cover Marie Kerjean use case very well, if I understand correctly; when I was learning math-comp indeed I kinda wanted to have the library in my context as indeed very often you need to check existing proofs [for inspiration ;) etc...]
This is exactly it. The question is not for myself, but for a new user who needs to have the libraries in the context to understand their use. Using the html documentation is not enough as one wants to compile, unfold, and play with previous formalized proofs in order to understand them.
Karl Palmskog (Oct 23 2020 at 12:23):this use case unfortunately only pertains to a few libraries, so I think it would make sense if those libraries themselves documented how they recommend new users to "play around". In particular, they can/should recommend a particular tag/branch which is not master
Karl Palmskog (Oct 23 2020 at 12:27):I'd also encourage libraries to use tools like Alectryon (preferred) or Proviola (legacy) to generate proof movie documentation
Christian Doczkal (Oct 23 2020 at 12:38):Marie Kerjean said:
This is exactly it. The question is not for myself, but for a new user who needs to have the libraries in the context to understand their use. Using the html documentation is not enough as one wants to compile, unfold, and play with previous formalized proofs in order to understand them.
Ah, I had mistakenly assumed that you were looking a setup for yourself to mix developing on top of mathcomp and contributing. My bad. I still think that having two opam branches, one to use the stable mathcomp and another to experiment with it, is a reasonably simple approach. But if that person is not interested in pushing changes, then just downloading and using the exact archive corresponding to the release may be more appropriate.
Christian Doczkal (Oct 23 2020 at 12:40):(or checking out a release tag for that matter)
Karl Palmskog (Oct 23 2020 at 12:41):the advantage of checking out a tag is that you can roll back breaking changes easily
Christian Doczkal (Oct 23 2020 at 12:45):Indeed, also it is simpler to transition to contributing, because one only has to switch branches.
Marie Kerjean (Oct 23 2020 at 15:00):Thanks for your advices !
Last updated: Sep 23 2023 at 14:01 UTC