Stream: Nix toolbox devs & users

Topic: Coq master dependency from flake


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (May 26 2023 at 15:40):

What do you include in "the existing Nix infrastructure" exactly?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Maxime Dénès (May 26 2023 at 18:23):

This time it works at least!

view this post on Zulip Maxime Dénès (May 26 2023 at 18:47):

Yes ok, and the problem is fixed in our CI.

view this post on Zulip Théo Zimmermann (May 26 2023 at 19:09):

The CI remains independent of the flake, doesn't it?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: May 19 2024 at 16:02 UTC