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

```
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:

https://github.com/math-comp/hierarchy-builder/commit/dac6bf6f3ee47e54523f19bf24ac3f07018d4dfa#diff-7ca2d406a1abeba994287e988d14a035c86f5ccb893d22f2fcc6cf451755f6c8

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

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

rerun elpi_hb first

well, I see the logic now

Last updated: Oct 13 2024 at 01:02 UTC