Stream: math-comp analysis

Topic: Nix

view this post on Zulip Marie Kerjean (Feb 07 2022 at 08:54):

Is Nix still recommended to use mc-analysis or should I switch to opam ?

view this post on Zulip Karl Palmskog (Feb 07 2022 at 08:55):

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.

view this post on Zulip Marie Kerjean (Feb 07 2022 at 09:15):

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 ?

view this post on Zulip Reynald Affeldt (Feb 07 2022 at 09:19):

To develop I am mostly relying on opam, but Nix is very useful for the CI.

view this post on Zulip Karl Palmskog (Feb 07 2022 at 09:22):

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.

view this post on Zulip Cyril Cohen (Feb 07 2022 at 10:20):

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.

view this post on Zulip Cyril Cohen (Feb 07 2022 at 10:37):

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?

view this post on Zulip Karl Palmskog (Feb 07 2022 at 10:44):

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: Apr 19 2024 at 10:02 UTC