Maxime Dénès (May 25 2023 at 15:22): Maxime Dénès (May 25 2023 at 15:22):VsCoq uses Nix flakes to express dependencies (https://github.com/coq-community/vscoq/blob/main/flake.nix). I would like to make it depend on Coq's master branch. I tried to do it with an override of the Coq derivation but it doesn't work because I can't provide a sha256. Is there any way to do it?
Maxime Dénès (May 25 2023 at 15:23):Is the "right" approach to push a flake on Coq's master branch, then use it as an input?
Ali Caglayan (May 26 2023 at 07:26):You wont be able to write a flake that depends on a branch without a hash. Having a flake for Coq and updating it as an input to your flake is the only way. You dont have to have a flake.nix in the main coq repo however, it can be done from an additional place.
Théo Zimmermann (May 26 2023 at 07:53):The simplest way is probably to add the flake to the Coq repo though. Personally, I am not opposed to such a change in the Nix infrastructure in the Coq repository. Since the Coq Nix Toolbox was introduced, I'm not aware of any user of the default.nix in the Coq repo besides our own CI anyway.
Théo Zimmermann (May 26 2023 at 07:55):Maybe the support for building external projects at https://github.com/coq/coq/tree/master/dev/ci/nix will need to be removed then (I don't know how easy it would be to port), but I wouldn't mind that either (again, it is pretty easy to accomplish the same objective with the Coq Nix Toolbox).
Ali Caglayan (May 26 2023 at 09:09):We can turn default.nix into a compatability layer around a flake.nix for users who don't use flakes. That way we won't have to modify existing nix infrastructure we have. I have written a flake for the coq repo before and it shouldn't be difficult to set up again.
Maxime Dénès (May 26 2023 at 09:13):I tried the other way around for now, i.e. define a flake.nix for Coq using flake-compat, to keep the current default.nix unchanged.
Ali Caglayan (May 26 2023 at 09:51):That's probably the best for your use case for now. I am planning to add proper flake support soon enough. The main bloxker is thinking about how to best integrate this with the existing nix infrastructure but I haven't thought much about all of this yet.
Théo Zimmermann (May 26 2023 at 15:40):What do you include in "the existing Nix infrastructure" exactly?
Maxime Dénès (May 26 2023 at 17:50):Ok so I gave it a try here: https://github.com/maximedenes/coq/commit/59ef6f783caf5f08ca07fece8b7ab09b3459b656
But I'm running in an issue: when I add that as an input to the flake I'm developing, nix develop puts in the path a coqtop which cannot find stdlib.
Maxime Dénès (May 26 2023 at 17:50):(it did compile stdlib)
I'm not sure what I need to do for it to work.
Théo Zimmermann (May 26 2023 at 17:59):That's strange. OTOH, we don't test the result of this default.nix expression much. What about using a nixpkgs.coq.override { version = ./.; }' in the flake?
Maxime Dénès (May 26 2023 at 18:20):Thanks for the suggestion, I'll try. It it especially strange that I thought it worked the first time I entered the shell (but not completely sure).
Maxime Dénès (May 26 2023 at 18:23):This time it works at least!
Maxime Dénès (May 26 2023 at 18:47):Yes ok, and the problem is fixed in our CI.
Théo Zimmermann (May 26 2023 at 19:09):The CI remains independent of the flake, doesn't it?
Maxime Dénès (May 26 2023 at 20:31):Sorry, what I mean is that VsCoq's CI needs the input to correctly set the stdlib location. The flake doesn't impact Coq's CI.
Cyril Cohen (May 29 2023 at 14:17):I'd be happy to have a flakes for coq conversation with people knowledgable about flakes at some point.
Théo Zimmermann (May 29 2023 at 16:11):Yeah, me too. We could try to allocate a slot for a Nix+Coq discussion at CUDW?
Last updated: Oct 08 2024 at 15:02 UTC