Stream: Coq devs & plugin devs

Topic: coqeal universe issues

view this post on Zulip Gaëtan Gilbert (Sep 11 2024 at 12:03):

https://github.com/LPCIC/coq-elpi/pull/685

We are repeatedly experiencing universe issues in CoqEAL on master

what are the issues like? @Pierre Roux

view this post on Zulip Pierre Roux (Sep 11 2024 at 12:09):

I still need to investigate the last one (and remember the previous ones), it may very well come from changes/additions in coq-elpi and not from any Coq bug.

view this post on Zulip Pierre Roux (Sep 11 2024 at 12:09):

The last one was in a combination of paramcoq and hierarchy-builder, so pretty nasty.

view this post on Zulip Pierre Roux (Sep 11 2024 at 12:10):

I mean, I'm not at all convinced this should go in Coq CI, might very well be much more noise than useful feedback.

Last updated: Oct 13 2024 at 01:02 UTC