Gaëtan Gilbert (Jun 19 2023 at 11:52): Gaëtan Gilbert (Jun 19 2023 at 11:52):cf https://github.com/math-comp/hierarchy-builder/issues/367
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
Enrico Tassi (Jun 19 2023 at 11:55):or maybe not that one, but another commit which landed in coq-master
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
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.
Pierre Roux (Jun 19 2023 at 19:26):Here it is: https://github.com/math-comp/hierarchy-builder/pull/369
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.
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?
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
Enrico Tassi (Jun 20 2023 at 09:45):https://gitlab.com/coq/coq/-/jobs/4503940136
Gaëtan Gilbert (Jun 20 2023 at 09:47):rerun elpi_hb first
Enrico Tassi (Jun 20 2023 at 11:04):well, I see the logic now
Last updated: Dec 05 2023 at 11:01 UTC