Théo Zimmermann (Jun 07 2021 at 15:09): Théo Zimmermann (Jun 07 2021 at 15:09):What's missing? The test-suite?
Cyril Cohen (Jun 07 2021 at 15:09):Yes
Cyril Cohen (Jun 07 2021 at 15:09):The VST problem
Théo Zimmermann (Jun 07 2021 at 15:10):Oh shoot.
Cyril Cohen (Jun 07 2021 at 15:10):Yes, I did not have the faith to tackle it yet
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.
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
Théo Zimmermann (Jun 08 2021 at 11:38):I'm currently having a look at this.
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?
Théo Zimmermann (Jun 08 2021 at 13:01):Hum, this looks too specific to the case of Coq.
Cyril Cohen (Jun 08 2021 at 13:03):meta-fetch is completely generic
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...
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.
Théo Zimmermann (Jun 08 2021 at 13:05):And that's what I'm having trouble with.
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.
Théo Zimmermann (Jun 08 2021 at 13:08):Is there an example of Coq package that does this?
Cyril Cohen (Jun 08 2021 at 13:11):yes mathcomp analysis
Théo Zimmermann (Jun 08 2021 at 13:13):OK thanks
Théo Zimmermann (Jun 08 2021 at 14:19):See https://github.com/NixOS/nixpkgs/pull/126214
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:
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
Hum, it still does some update so I've opened https://github.com/coq-community/coq-nix-toolbox/pull/35 with it.
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: Apr 19 2024 at 00:02 UTC