Stream: Coq devs & plugin devs

Topic: metacoq ci

view this post on Zulip Gaëtan Gilbert (Oct 04 2021 at 09:32):

Wy do I get "unbound module Erasure" when I run ci-metacoq locally? it seems to work fine in the pipelines

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2021 at 15:41):

No idea, seems to work fine here.

view this post on Zulip Matthieu Sozeau (Oct 13 2021 at 19:51):

Strange, maybe it's an ocaml issue? Which version are you using Gaëtan ?

view this post on Zulip Gaëtan Gilbert (Oct 13 2021 at 20:28):

4.09.1

view this post on Zulip Matthieu Sozeau (Oct 18 2021 at 17:38):

I got it too, on 4.09 and an unclean archive

view this post on Zulip Gaëtan Gilbert (Nov 10 2021 at 09:01):

still getting this (it was on the second run of ci-metacoq)

Last updated: Dec 07 2023 at 04:02 UTC