Stream: Coq devs & plugin devs

Topic: fiat-crypto CI broken


view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 22:47):

It seems that fiat-crypto is broken on master, likely due to the last commit that was introduced to fix backwards compat.

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 22:47):

cc @Jason Gross

view this post on Zulip Jason Gross (Jan 20 2021 at 22:48):

Ugh, is there no way to write instantiate (1:=...) in (value of H) which is compatible with both 8.9 and master?

view this post on Zulip Jason Gross (Jan 20 2021 at 22:50):

Ok, I've pushed another commit that hopefully fixes things

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2021 at 22:51):

Current Coq still allows Value but it triggers a warning, and it is seemingly fatal in the CI


Last updated: Oct 16 2021 at 07:02 UTC