@Enrico Tassi : since last night I get a Coq Platform CI failure around Elpi and OCaml versions - this is with the picks where I request specific versions - the picks did not change.

The error is:

```
- (invariant) → ocaml-variants = 4.13.1+options → ocaml = 4.13.1
122
- coq-mathcomp-analysis = 0.5.0 → coq-hierarchy-builder = 1.2.0 → coq-elpi (< 1.13~ | >= dev) → ocaml < 4.12~
```

See https://github.com/coq/platform/actions/runs/3374071815/jobs/5599308699#step:5:120

Are you aware of changes which could cause this?

The same on one ubuntu build: https://github.com/coq/platform/actions/runs/3374231810/jobs/5599636750#step:5:90.

the math comp analysis dev made a dependency on HB stricter. Cc @Reynald Affeldt

I couldn't fillow exactly the reason

This was to get rid of CI failures. The problem was observed with infotheo and restricting HB was the solution we found with @Karl Palmskog (https://github.com/coq/opam-coq-archive/pull/2367). Since these were errors due to older packages of mathcomp-analysis (also failing on the CI), I also applied the fix to them (https://github.com/coq/opam-coq-archive/pull/2368).

the story was basically: analysis 0.5.1 and below did not work with HB 1.3.0 and later (which we confirmed in opam archive CI and I also checked locally)

so we set a strict dependency for failing packages (old analysis and infotheo) on HB 1.2.0, and CI passed. But I guess HB 1.2.0 has OCaml restrictions.

@Reynald Affeldt but based on the Platform CI, Analysis 0.5.0 may actually work with HB 1.3.0/1.4.0? Maybe the HB problem was restricted to 0.5.1?

let me check

we probably want to drop the HB restriction from infotheo in any case, since infotheo itself is not to blame for the failures. If we get analysis deps right, infotheo should work fine.

hb 1.3.0 + mathcomp 1.14 + coq 8.15.2 fails with the apply-w-params error

for analysis 0.5.0?

yes (HEAD detached at 0.5.0)

@Reynald Affeldt OK I think I understand what is going on. There is a version of HB 1.2.1 that we need to allow for all the packages in your PR

this HB version is used by the Platform for 8.15.2

how about we use the following:

```
"coq-hierarchy-builder" { < "1.3.0" }
```

I see

can you do the PR or should I?

I can do it but not right now (meeting about to begin) (but I can do later in the evening)

if it's OK I'll do it then and ping you in, let's get it sorted ASAP

thank you

https://github.com/coq/opam-coq-archive/pull/2369

@Michael Soegtrop do you plan to restart the failing CI? it should be fine now with archive PR 2369 merged.

@Karl Palmskog : I restart CI.

running ...

There are some general CI runner stability issues, but the dependency issue seems to be resolved.

Thanks for the support!

Karl Palmskog has marked this topic as resolved.

Last updated: Nov 29 2023 at 18:01 UTC