Stream: Coq devs & plugin devs

Topic: Iris folder structure changes


view this post on Zulip Ralf Jung (Nov 11 2020 at 16:27):

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!

view this post on Zulip Gaëtan Gilbert (Nov 11 2020 at 19:24):

looks broken

view this post on Zulip Gaëtan Gilbert (Nov 11 2020 at 19:26):

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

view this post on Zulip Ralf Jung (Nov 12 2020 at 10:30):

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

view this post on Zulip Ralf Jung (Nov 12 2020 at 10:31):

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

view this post on Zulip Ralf Jung (Nov 12 2020 at 10:31):

do you have a link to a failed build log?

view this post on Zulip Ralf Jung (Nov 12 2020 at 10:33):

oh I missed the double quotes

view this post on Zulip Ralf Jung (Nov 12 2020 at 10:35):

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


Last updated: Oct 21 2021 at 21:03 UTC