Stream: Elpi users & devs

Topic: ✔ Coq Platform CI failure


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Nov 02 2022 at 07:29):

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

view this post on Zulip Enrico Tassi (Nov 02 2022 at 07:29):

I couldn't fillow exactly the reason

view this post on Zulip 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).

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reynald Affeldt (Nov 02 2022 at 07:47):

let me check

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 02 2022 at 08:52):

for analysis 0.5.0?

view this post on Zulip Reynald Affeldt (Nov 02 2022 at 08:53):

yes (HEAD detached at 0.5.0)

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 02 2022 at 08:58):

this HB version is used by the Platform for 8.15.2

view this post on Zulip Karl Palmskog (Nov 02 2022 at 08:58):

how about we use the following:

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

view this post on Zulip Reynald Affeldt (Nov 02 2022 at 08:59):

I see

view this post on Zulip Karl Palmskog (Nov 02 2022 at 08:59):

can you do the PR or should I?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Reynald Affeldt (Nov 02 2022 at 09:02):

thank you

view this post on Zulip Karl Palmskog (Nov 02 2022 at 09:28):

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

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Nov 02 2022 at 13:46):

@Karl Palmskog : I restart CI.

view this post on Zulip Michael Soegtrop (Nov 02 2022 at 13:48):

running ...

view this post on Zulip Michael Soegtrop (Nov 03 2022 at 08:52):

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

view this post on Zulip Michael Soegtrop (Nov 03 2022 at 08:52):

Thanks for the support!

view this post on Zulip Notification Bot (Nov 03 2022 at 18:18):

Karl Palmskog has marked this topic as resolved.


Last updated: Nov 29 2023 at 18:01 UTC