What's missing? The test-suite?
The VST problem
Yes, I did not have the faith to tackle it yet
I can try to fix that, but I was wondering if I should hold off until your own refactoring PR on nixpkgs is merged.
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
I'm currently having a look at this.
@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?
Hum, this looks too specific to the case of Coq.
meta-fetch is completely generic
What is specific though is that
version cannot be
null, it is not an optional argument, contrary to the case of Coq packages...
So basically, here I need to know which version is built, including in the case where the defaultVersion mechanism kicks in.
And that's what I'm having trouble with.
This is, e.g., to decide whether to use an external flocq, and which set of patches to use.
Is there an example of Coq package that does this?
yes mathcomp analysis
I've tried testing it with the coq-nix-toolbox by running
updateNixpkgs Zimmi48 mv-compcert followed by
genNixActions but the latter failed with:
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.
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