Stream: Coq devs & plugin devs

Topic: hb_test failing in CI


view this post on Zulip Gaëtan Gilbert (Jun 19 2023 at 11:52):

cf https://github.com/math-comp/hierarchy-builder/issues/367

view this post on Zulip Enrico Tassi (Jun 19 2023 at 11:55):

HB: synthesized in file File "(stdin)", line 5, column 0, [-character 127:-]

I think it has something to do with https://github.com/math-comp/hierarchy-builder/pull/362 being merged into coq-master
CC @Pierre Roux

view this post on Zulip Enrico Tassi (Jun 19 2023 at 11:55):

or maybe not that one, but another commit which landed in coq-master

view this post on Zulip Enrico Tassi (Jun 19 2023 at 12:14):

Given the conflicts, I suspect this is the culprit:
https://github.com/math-comp/hierarchy-builder/commit/dac6bf6f3ee47e54523f19bf24ac3f07018d4dfa#diff-7ca2d406a1abeba994287e988d14a035c86f5ccb893d22f2fcc6cf451755f6c8

view this post on Zulip Pierre Roux (Jun 19 2023 at 12:26):

Yes looks like a merge conflict when merging HB master branch into coq-master. This was done without PR hence no CI so that may explain why we missed it. Sorry about that, let me open a PR on HB to fix that.

view this post on Zulip Pierre Roux (Jun 19 2023 at 19:26):

Here it is: https://github.com/math-comp/hierarchy-builder/pull/369

view this post on Zulip Enrico Tassi (Jun 20 2023 at 09:17):

@Gaëtan Gilbert how do I re-run a job which was updated upstream?
I get this:

Warning: download and unpacking of hierarchy_builder skipped because /builds/coq/coq/_build_ci/hierarchy_builder already exists.

so downloading is somehow cached, making CI "reproducible" I guess. but I don't want to rebase my PR just for one job.

view this post on Zulip Gaëtan Gilbert (Jun 20 2023 at 09:43):

locally? or in CI?
if in CI can you link the job which says that warning?

view this post on Zulip Gaëtan Gilbert (Jun 20 2023 at 09:44):

I guess in CI since the path is /builds/... but in CI shouldn't be caching so that's strange

view this post on Zulip Enrico Tassi (Jun 20 2023 at 09:45):

https://gitlab.com/coq/coq/-/jobs/4503940136

view this post on Zulip Gaëtan Gilbert (Jun 20 2023 at 09:47):

rerun elpi_hb first

view this post on Zulip Enrico Tassi (Jun 20 2023 at 11:04):

well, I see the logic now


Last updated: Jun 13 2024 at 03:02 UTC