Update the `esy` package

The following discussion from !186 (merged) should be addressed:

• @proux started a discussion: (+2 comments)

  BTW, @Mbodin I don't know how to update the esy package, could you have a look? (you can take inspiration on the coq-prosa.opam file changes)

assigned to @Mbodin

Sorry for the delay. I’ve been running in some issues with esy: it assumes that installing a package can’t affect another, and prevent them to. This is useful to be able to reuse packages among different working directories, as well as ensuring that we won’t get undeclared dependencies: I actually like this assumption.

In the context of a lot of Coq project, this is unfortunately rarely the case as packages tend to install themselves under path-to-coqc/user-contrib/lib-name. What I usually do is to tell esy (through the resolutions key) how to compile/install projects: I basically copy/paste the content of their Opam file, but change the install directory to the one selected by esy. I then update the $COQPATH variable to include this directory. This is usually not a lot of work. Because of how coq_makefile is written, the actual installation folder is usually path-chosen-by-esy/user-contrib/lib-name, which is fine.

In the case of mathcomp, however, each coq-mathcomp-lib wants to install itself under path-to-coqc/user-contrib/mathcomp/lib. This means that if each of them install themselves under path-chosen-by-esy/user-contrib/mathcomp/lib-name, then importing mathcomp later on does not expect as wanted: it just imports one path-chosen-by-esy/user-contrib/mathcomp/lib-name instead of all of them at once.

So I cheated: I grouped all the mathcomp libs under one that installs all the ones we need. I’m not very proud of this solution as it feels not compositional.

I would be interested if you know how this would have been done within Nix: I’m not super happy with what I did here.

created merge request !195 (closed) to address this issue

mentioned in merge request !195 (closed)

mentioned in merge request !196 (merged)

Sorry, I got confused with Gitlab. It seems that I included other commits to the MR.

Thanks for updating the esy package. I unfortunately have no experience with nix.

closed with merge request !196 (merged)

@Mbodin sorry for the late answer, in Nix they adopted the same solution than you: a single package for mathcomp: https://github.com/NixOS/nixpkgs/tree/master/pkgs/development/coq-modules/mathcomp

In fact, the OPAM packages for mathcomp are split only to save compilation time to people only interested in part of the library (as OPAM is a source based package manager), this is considered much less of an issue in Nix that offers caching facilities for binaries.