Stream: Coq devs & plugin devs

Topic: coq master CI failure in std++

Ralf Jung (Nov 11 2020 at 14:01):

I just got a CI failure in std++ when building against Coq master: https://gitlab.mpi-sws.org/iris/stdpp/-/jobs/101569
Shouldn't Coq CI have prevented this?

Ralf Jung (Nov 11 2020 at 14:02):

hm, also then it should have already failed last night...

Ralf Jung (Nov 11 2020 at 14:13):

ah the regression only arises with name mangling enabled

Ralf Jung (Nov 11 2020 at 14:16):

https://github.com/coq/coq/issues/13348

Last updated: Apr 19 2024 at 00:02 UTC