bedrock2 icon indicating copy to clipboard operation
bedrock2 copied to clipboard

bytedump test seems to no longer work on Windows

Open JasonGross opened this issue 8 months ago • 0 comments

COQFLAGS="-Q src/bedrock2 bedrock2 -Q src/bedrock2Examples bedrock2Examples -Q D:/a/fiat-crypto/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil " ../etc/bytedump.py bedrock2.PrintListByte.allBytes > special/BytedumpTest.out.tmp
No module named 'resource'

Coq < Coq < 
Coq < Toplevel input, characters 25-35:
> Local Set Printing Width 2147483647.
>                          ^^^^^^^^^^
Error: This number is too large.

https://github.com/mit-plv/fiat-crypto/actions/runs/14630986227/job/41053094953?pr=2073#step:11:2456

@andres-erbsen Any idea what's going on here? Windows CI uses Coq 8.18.0, so I don't see why this should have suddenly started happening...

https://github.com/mit-plv/fiat-crypto/issues/1394#issuecomment-2825962067

JasonGross avatar Apr 24 '25 01:04 JasonGross