Stream: Coq devs & plugin devs

Topic: ssreflect rewrite problem


view this post on Zulip Ralf Jung (Feb 17 2021 at 14:39):

In Iris, we keep running into this longstanding ssreflect rewrite problem. Would anyone have an idea who could know the relevant code that is causing the bug?

view this post on Zulip Enrico Tassi (Feb 17 2021 at 14:54):

Well, I pinged the right group of maintainer. Let's see if we @Gaëtan Gilbert or @Maxime Dénès can allocate some time. I'm probably the one that knows the buggy code better, I'm happy to help pointing them to the right piece of code, but I don't have much time myself to devote to this bugfix :-/

view this post on Zulip Ralf Jung (Feb 27 2021 at 09:30):

@Gaëtan Gilbert came up with a fix :hearts: https://github.com/coq/coq/pull/13882

view this post on Zulip Guillaume Melquiond (Feb 27 2021 at 09:54):

Note that it breaks quite a few developments. So, with my release manager hat on, I don't feel too thrilled about it right now.

view this post on Zulip Gaëtan Gilbert (Feb 27 2021 at 10:04):

the iris failure looks strange, possibly a bug is involved


Last updated: Oct 16 2021 at 03:02 UTC