Stream: Elpi users & devs

Topic: coq-elpi dev package CI error

view this post on Zulip Karl Palmskog (Jun 15 2023 at 19:59):

Is this error I got in CI with OCaml 4.13.1 for coq-elpi.devexpected?

# 2624 |         ComCoercion.try_add_new_coercion_with_target gr ~local ~poly
  # 2625 |           ~reversible ~source ~target
  # 2626 |      | _, _ ->
  # 2627 |         ComCoercion.try_add_new_coercion gr ~local ~poly ~reversible
  # 2628 |      end.
  # Error: This expression has type nonuniform:bool -> unit
  #        but an expression was expected of type unit
  #        because it is in the left-hand side of a sequence

view this post on Zulip Pierre Roux (Jun 15 2023 at 20:54):

might be a transient error due to some unmerged overlay?

view this post on Zulip Karl Palmskog (Jun 15 2023 at 21:30):

the most recent overlay PR is from April, and is still a draft (https://github.com/LPCIC/coq-elpi/pull/455). Last merge to master was in May.

view this post on Zulip Karl Palmskog (Jun 15 2023 at 21:31):

but I might be missing something still

view this post on Zulip Pierre Roux (Jun 16 2023 at 06:26):

coq-elpi is one of the most common overlays, including one merged yesterday: https://github.com/LPCIC/coq-elpi/commits/coq-master

view this post on Zulip Karl Palmskog (Jun 16 2023 at 06:28):

ah right, I forget the branch for Coq master is not the default one

Last updated: Oct 13 2024 at 01:02 UTC