bedrock2
bedrock2 copied to clipboard
bytedump test seems to no longer work on Windows
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