bedrock2
bedrock2 copied to clipboard
Bytedump.v fails to build on Windows
Apparently, ^Z
(\x1a
) is treated as end-of-file by coqc on Windows. This seems probably at least somewhat valid, given that Wikipedia says:
In CP/M, 86-DOS, MS-DOS, PC DOS, DR-DOS, and their various derivatives, the SUB character was also used to indicate the end of a character stream, and thereby used to terminate user input in an interactive command line window (and as such, often used to finish console input redirection, e.g. as instigated by COPY CON: TYPEDTXT.TXT).
I'm going to report this as a Coq bug, but I'm not sure that it is one. Thoughts?
Bytedump.v
and BytedumpTest.v
keep causing trouble...
@andres-erbsen is my understanding correct that its only use case is to print Gallina strings containing C source code without surrounding quotes? If so, can't we just remove all special characters? Or is there another way of printing Gallina strings without surrounding quotes?
At least when I designed this, I intended it to print risc-v binaries.
reimplemented in ltac2