pycoq
pycoq copied to clipboard
ejgallego
nixify
one take on this is in https://github.com/ejgallego/pycoq/pull/10 - However, @ejgallego said
I think also that opam2nix should not be used, but start from the coq-serapi derivation
which is not in that approach (which wasn't totally working anyway, for reasons).
Perhaps flake will be the way to go. I'll do some investigating.
The advantage of opam2nix is that there's a single source of truth, only one thing to update (pycoq.opam) when things change. With dependencies by hand specified in .nix files, there's two sources of truth to update.
I'm not nix expert, I'll cc @zimmi48 and @vbgl who are the resident Coq experts, but I think the way coq-serapi was implemented is the way to do.
pycoq now embeds coq-serapi, but I hope in a few weeks I will instead use the derivation in nix.
Thus, to get a nix derivation for pycoq you need:
- the deps in the coq-serapi derivation or the coq-serapi derivation once it is updated.
- python3 deps
- ocaml's pythonlib derivation
So it seems to me that going that way should work much better.
The approach that we've been generally following in nixpkgs for the OCaml and the Coq ecosystems (with @vbgl, @CohenCyril and others) has been to manage the packages and their dependencies manually. While this may sound cumbersome, it brings lots of benefits such as more control and easier overrides.
The *2nix approach doesn't help get rid of the corresponding package manager, which was the whole point of wanting to use Nix (at least in my case, when I started looking into it more than five years ago). It also doesn't help to get a manually curated package collection that works well together (resorting to using the version constraint resolution mechanisms from package managers instead) and defeats all hopes of shared pre-built derivations (if each project is going to be using its own version of basic packages such as Coq, compiled with slightly different versions of dependencies...). IMHO this approach is a band-aid to be able to manage huge ecosystems with crazy dependency chains, or to be able to quickly hack on a project without investing the effort in adding all the required dependencies to nixpkgs.
Flakes are also not the way to go, again IMHO. It seems to me that the idea that each project is going to be distributing its own flake is the best way to create most of the problems I was listing in the previous paragraph, by making Nix, just an average package manager, and losing all the benefits of being the largest, largely manually curated, collection of packages that has ever existed. Maybe flakes can make sense to modularize nixpkgs a little by splitting some package collections into their own flake, but even there, it's not clear to me that the benefits will overweight the costs.
The way to go (IMHO) is to get the missing PyCoq dependencies in nixpkgs (pythonlib and pyml are probably the only ones missing) then add an unstable derivation for PyCoq and run nix-shell '<nixpkgs>' -A coqPackages.PyCoq to get the environment to build it, if you need to hack on it (or just install the Coq Nix Toolbox in this repo and define the appropriate ocaml-overlays and coq-overlays). While PyCoq is at the intersection of three ecosystems (Coq, OCaml and Python), I'd suggest putting it in coqPackages because the Coq dependency is the one whose version is going to be the most impactful, and there is good support anyway in coqPackages to override the other dependencies as well.
I don't have so much time at the moment, but if this is not an urgent request, I could try to have a look later.
Thanks a lot @Zimmi48 for the detailed write up, indeed I also believe this is the way to go, pyml is already in ocaml packages, so only pythonlib [which is really straightforward] is needed.
In fact nix likely provides a much better experience here than opam , as it can manage both the ocaml installation and the python installation better than opam which is exclusive to ocaml and forbids us from calling pip3 install from their setup script due to sandboxing.