Is Nix still recommended to use mc-analysis or should I switch to opam ?
given that mc-analysis is in the Coq Platform, and the Platform uses opam, opam is going to be more tested and packaged quicker. But this doesn't mean Nix is unfeasible, only that it may have more lag than opam with releases.
At the end I found Nix easier to work with when developing, but this was supposing @Cyril Cohen or @Reynald Affeldt were still using it. Is it the case ?
To develop I am mostly relying on opam, but Nix is very useful for the CI.
I can't speak for MathComp, but generally in the Coq community we aim to support both Nix and opam going forward, both in CI and for local development. The main factor that makes opam packaging faster is that the Coq team has its own opam repository.
short answer, yes it works and I personally recommend it.
I'm only using nix, and the CI / which reuses the user nix config (with several parameters), so it is supposed to be guaranteed to work in any project with a nix CI, including mathcomp and mathcomp-analysis.
Karl Palmskog said:
given that mc-analysis is in the Coq Platform, and the Platform uses opam, opam is going to be more tested and packaged quicker. But this doesn't mean Nix is unfeasible, only that it may have more lag than opam with releases.
I think this is a library-user answer, and I believe @Marie Kerjean was asking a dev oriented question, am I right?
there is a dev
opam package as well: https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.dev/opam
I was focusing on differences between the systems, and I don't think there are any obvious ones on the dev side (build from Git in one way or another)
Last updated: Oct 13 2024 at 01:02 UTC