bedrock2 icon indicating copy to clipboard operation
bedrock2 copied to clipboard

Bytedump.v fails to build on Windows

Open JasonGross opened this issue 4 years ago • 2 comments

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?

JasonGross avatar Mar 16 '20 19:03 JasonGross

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?

samuelgruetter avatar Mar 16 '20 22:03 samuelgruetter

At least when I designed this, I intended it to print risc-v binaries.

andres-erbsen avatar Mar 17 '20 18:03 andres-erbsen

reimplemented in ltac2

andres-erbsen avatar Nov 15 '22 23:11 andres-erbsen