Heads-up: we reorganized the iris git repo a bit. I *think* Coq's CI should keep working as-is, but if you see any strange issues popping up with iris on the Coq CI, please let me know!

looks broken

the coq-iris dep got replaced by some random thing here https://gitlab.mpi-sws.org/iris/examples/-/blob/master/coq-iris-examples.opam

(next timepelase ping me to make sure I see this even when I am not logged in to Zulip)

Gaëtan Gilbert said:

the coq-iris dep got replaced by some random thing here https://gitlab.mpi-sws.org/iris/examples/-/blob/master/coq-iris-examples.opam

the coq CI code is grepping for `coq-iris`

which should still work

do you have a link to a failed build log?

oh I missed the double quotes

https://github.com/coq/coq/pull/13357

Last updated: Oct 21 2021 at 21:03 UTC