Stream: Nix toolbox devs & users

Topic: Release 1.0?


view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:09):

What's missing? The test-suite?

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:09):

Yes

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:09):

The VST problem

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:10):

Oh shoot.

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:10):

Yes, I did not have the faith to tackle it yet

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:10):

I can try to fix that, but I was wondering if I should hold off until your own refactoring PR on nixpkgs is merged.

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:11):

the work could range between 15 min and 1/2 day... and I don't have half a way, so I bury my head in the sand

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 11:38):

I'm currently having a look at this.

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 12:57):

@Cyril Cohen At this point, I'm blocked because I need to know which version of CompCert I'm building. Is this the trick to use in this case?

https://github.com/NixOS/nixpkgs/blob/fbfb79400a08bf754e32b4d4fc3f7d8f8055cf94/pkgs/applications/science/logic/coq/default.nix#L49-L53

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 13:01):

Hum, this looks too specific to the case of Coq.

view this post on Zulip Cyril Cohen (Jun 08 2021 at 13:03):

meta-fetch is completely generic

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 13:05):

What is specific though is that version cannot be null, it is not an optional argument, contrary to the case of Coq packages...

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 13:05):

So basically, here I need to know which version is built, including in the case where the defaultVersion mechanism kicks in.

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 13:05):

And that's what I'm having trouble with.

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 13:06):

This is, e.g., to decide whether to use an external flocq, and which set of patches to use.

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 13:08):

Is there an example of Coq package that does this?

view this post on Zulip Cyril Cohen (Jun 08 2021 at 13:11):

yes mathcomp analysis

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 13:13):

OK thanks

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 14:19):

See https://github.com/NixOS/nixpkgs/pull/126214

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 14:20):

I've tried testing it with the coq-nix-toolbox by running updateNixpkgs Zimmi48 mv-compcert followed by genNixActions but the latter failed with:

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 14:20):

error: value is a list while a set was expected, at /home/theo/git/coq-nix-toolbox/deps.nix:10:44

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 14:27):

Hum, it still does some update so I've opened https://github.com/coq-community/coq-nix-toolbox/pull/35 with it.

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 17:19):

So it looks like I did make it work, but I also discovered an issue with the current derivation for CompCert 3.7 :confused:


Last updated: Jan 29 2023 at 15:02 UTC