Stream: Coq devs & plugin devs

Topic: coq-http broken in CI


view this post on Zulip Gaëtan Gilbert (Jan 26 2024 at 20:17):

no failure on master yet but multiple unrelated PRs with the same error:
https://gitlab.inria.fr/coq/coq/-/jobs/3813602
https://gitlab.inria.fr/coq/coq/-/jobs/3813438
https://gitlab.inria.fr/coq/coq/-/jobs/3813195

File "./JSON.v", line 60, characters 0-141:
Error:
The following term contains unresolved implicit arguments:
  (fun (T : Type) (f : json -> option T) (j : json) =>
   if j is JSON__Array l then sequence (map f l) else None)
More precisely:
- ?Ap: Cannot infer the implicit parameter Ap of sequence whose type is
  "Applicative.Applicative option" (no type class instance found) in
  environment:
  T : Type
  f : json -> option T
  j : json
  l : list json
make[2]: Leaving directory '/builds/coq/coq/_build_ci/quickchick'

weird that it fails in _build_ci/quickchick but the job is http, probably some script is mesed up


Last updated: Oct 13 2024 at 01:02 UTC