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
or maybe not that one, but another commit which landed in coq-master
Given the conflicts, I suspect this is the culprit:
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.
Here it is: https://github.com/math-comp/hierarchy-builder/pull/369
@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.
locally? or in CI?
if in CI can you link the job which says that warning?
I guess in CI since the path is /builds/... but in CI shouldn't be caching so that's strange
rerun elpi_hb first
well, I see the logic now
Last updated: Dec 05 2023 at 11:01 UTC