Please create a tag for Coq 8.16 in Coq Platform 2022.09 about bedrock2 HOT 6 CLOSED

I replaced sed with python and checked that it builds on the CI Mac. #273 remains a mystery.

from bedrock2.

@samuelgruetter @andres-erbsen @JasonGross : I am not sure what to do about this - there are still cross platform issues and possibly others. I had little time to look after this recently (moving homes ...) but we might still be able to get things fixed.

from bedrock2.

Yeah, I'm not sure what to do here.

• The sed -z hack could probably be replaced by awk '{q=p;p=$0}NR>1{print q}END{ORS = ""; print p}'
• I don't understand why Bytedump.v (which is not autogenerated) is considred a syntax error on Windows (and not on Linux, and not on Windows with coq 8.12).

from bedrock2.

The second one can probably be reported as a regression in Coq, attaching a standalone .v file?

from bedrock2.

Actually, I think I was confused -- the fiat-crypto windows CI doesn't seem to build bedrock2 after all. Perhaps it's possible this file never parsed under Windows, and we didn't notice for three and a half years?

from bedrock2.

I can confirm that this works now on MacOS (and all other platforms except 32 bit Windows - see (coq/platform#178). The version picked is coq-bedrock2.0.0.3 (the only version compatible with fiat-crypto).

So I am closing this as solved.

from bedrock2.