Michael Soegtrop (Nov 02 2022 at 07:09): Michael Soegtrop (Nov 02 2022 at 07:09):@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?
Michael Soegtrop (Nov 02 2022 at 07:10):The same on one ubuntu build: https://github.com/coq/platform/actions/runs/3374231810/jobs/5599636750#step:5:90.
Enrico Tassi (Nov 02 2022 at 07:29):the math comp analysis dev made a dependency on HB stricter. Cc @Reynald Affeldt
Enrico Tassi (Nov 02 2022 at 07:29):I couldn't fillow exactly the reason
Reynald Affeldt (Nov 02 2022 at 07:35):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).
Karl Palmskog (Nov 02 2022 at 07:39):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)
Karl Palmskog (Nov 02 2022 at 07:41):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.
Karl Palmskog (Nov 02 2022 at 07:46):@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?
Reynald Affeldt (Nov 02 2022 at 07:47):let me check
Karl Palmskog (Nov 02 2022 at 07:51):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.
Reynald Affeldt (Nov 02 2022 at 08:51):hb 1.3.0 + mathcomp 1.14 + coq 8.15.2 fails with the apply-w-params error
Karl Palmskog (Nov 02 2022 at 08:52):for analysis 0.5.0?
Reynald Affeldt (Nov 02 2022 at 08:53):yes (HEAD detached at 0.5.0)
Karl Palmskog (Nov 02 2022 at 08:57):@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
Karl Palmskog (Nov 02 2022 at 08:58):this HB version is used by the Platform for 8.15.2
Karl Palmskog (Nov 02 2022 at 08:58):how about we use the following:
"coq-hierarchy-builder" { < "1.3.0" }
I see
Karl Palmskog (Nov 02 2022 at 08:59):can you do the PR or should I?
Reynald Affeldt (Nov 02 2022 at 09:01):I can do it but not right now (meeting about to begin) (but I can do later in the evening)
Karl Palmskog (Nov 02 2022 at 09:02):if it's OK I'll do it then and ping you in, let's get it sorted ASAP
Reynald Affeldt (Nov 02 2022 at 09:02):thank you
Karl Palmskog (Nov 02 2022 at 09:28):https://github.com/coq/opam-coq-archive/pull/2369
Karl Palmskog (Nov 02 2022 at 13:36):@Michael Soegtrop do you plan to restart the failing CI? it should be fine now with archive PR 2369 merged.
Michael Soegtrop (Nov 02 2022 at 13:46):@Karl Palmskog : I restart CI.
Michael Soegtrop (Nov 02 2022 at 13:48):running ...
Michael Soegtrop (Nov 03 2022 at 08:52):There are some general CI runner stability issues, but the dependency issue seems to be resolved.
Michael Soegtrop (Nov 03 2022 at 08:52):Thanks for the support!
Notification Bot (Nov 03 2022 at 18:18):Karl Palmskog has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC