Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[question] How to test validate / coqchk targets on Coq's CI? #14592

Open
JasonGross opened this issue Jul 2, 2021 · 2 comments
Open

[question] How to test validate / coqchk targets on Coq's CI? #14592

JasonGross opened this issue Jul 2, 2021 · 2 comments
Labels
kind: infrastructure CI, build tools, development tools. kind: question Issues seeking an answer to a question. Consider asking on zulip instead. part: checker The coqchk binary for validating .vo files.

Comments

@JasonGross
Copy link
Member

I noticed today that there's an issue with building the validate target in Coq's CI: if one CI job A depends on another CI job B, and B builds the validate target, then this call to coqchk gets re-run when testing A, because the ci-A target depends on the ci-B target (I think mainly to install things?). How should coqchk be tested on Coq's CI?

cc @coq/ci-maintainers
@JasonGross JasonGross added kind: infrastructure CI, build tools, development tools. part: checker The coqchk binary for validating .vo files. kind: question Issues seeking an answer to a question. Consider asking on zulip instead. labels Jul 2, 2021
@SkySkimmer
Copy link
Contributor

We should separate ci-A into ci-A-main and ci-A-extra, then both ci-A-extra and ci-B depend on ci-A-main (or some such scheme)
The ci-A job could still run both ci-A targets, or could also be split in 2 jobs

@JasonGross
Copy link
Member Author

That seems good. The relevant targets currently are ci-coq_performance_tests, ci-iris, and ci-hott. I'm not sure if we have anything depending on them, but it's probably good to split them preemptively.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: infrastructure CI, build tools, development tools. kind: question Issues seeking an answer to a question. Consider asking on zulip instead. part: checker The coqchk binary for validating .vo files.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@JasonGross @SkySkimmer