Erik Martin-Dorel (Dec 03 2020 at 01:20): Erik Martin-Dorel (Dec 03 2020 at 01:20):Erik Martin-Dorel said:
Karl Palmskog said:
unfortunately, the default script does not work well when there are multiple opam files. Basically, one needs to be able to specify both:
- "current opam file", i.e., the opam file to pin, install dependencies for, and then actually build/install
- "base opam files", i.e., list of local opam files which may be dependencies for the current opam file; all of these need to be pinned (some may get built when all deps of the current file is built)
OK Karl, so I guess you'll need to provide your
custom_script(unless the feature request https://github.com/coq-community/docker-coq-action/issues/22#issuecomment-695803544 would be handy for your use case?)
Hi @Karl Palmskog , since my previous message above I believed it was possible to directly reuse the default layout of docker-coq-action (i.e., without needing to add other YAML fields), and I've just thought about an idea that could support the use case you described (installing several opam packages successively to closely verify their dependencies consistency, and possibly combine this with a matrix specification to run several of these tests apart in parallel). Maybe you already thought about a similar idea, BTW.
Namely, it consists into passing a GHA matrix variable opam_files that contains a list of .opam packages to be built in the given order.
The custom_script is just slightly modified to incorporate two bash loops over that string (since we can assume there is no "space" within that string; but obviously we could be more careful by enforcing that that string does not contain "*" or so either).
Here are the links:
I don't know if that could/should be integrated somehow (at least from a documentation point of view) in docker-coq-action.
Anyway, let me know if you have any feedback about that PoC example.
Last updated: Apr 18 2024 at 15:01 UTC