Skip to content

Commit

Permalink
dynamically remove line separator in bytedump.sh
Browse files Browse the repository at this point in the history
  • Loading branch information
andres-erbsen committed Sep 29, 2022
1 parent bf9dfdb commit 7c6a089
Showing 1 changed file with 19 additions and 14 deletions.
33 changes: 19 additions & 14 deletions etc/bytedump.sh
Original file line number Diff line number Diff line change
Expand Up @@ -7,23 +7,28 @@ coqtop -q -quiet $COQFLAGS 2>/dev/null << EOF
Require bedrock2.PrintListByte ${1%.*}.
Local Set Printing Width 2147483647.
Goal True.
idtac "COQTOP_CRAP_ENDS_HERE".
idtac "COQBUG(15373)".
idtac "LINE_SEPARATOR_LOTTERY".
PrintListByte.print_list_byte ${1}.
Abort.
EOF
} | python3 -c '
import os, sys
needle = b"\nCOQTOP_CRAP_ENDS_HERE\n"
waiting_on_coqbug_15373 = True
} | python3 -c '# strip header, detect \r\n or \n, convert to \n, strip last \n
import os, sys # os.linesep is \n on cygwin but \r\n in cygwin coq on github ci
b = b""
while not b.endswith(b"COQBUG(15373)"):
r = os.read(0, 1); b += r
if not r: print(f"{b!r}"); sys.exit(4)
b = b""
while not b.endswith(b"LINE_SEPARATOR_LOTTERY"):
r = os.read(0, 1); b += r
if not r: print(f"{b!r}"); sys.exit(3)
linesep = b[:-len(b"LINE_SEPARATOR_LOTTERY")]
os.read(0, len(linesep)) == linesep or sys.exit(2)
b = b""
while True:
r = os.read(0, 1)
if not r:
sys.exit(waiting_on_coqbug_15373 + 2*(not b.endswith(b"\n")))
b = b[-(len(needle)-len(r)):] + r
if b == needle:
waiting_on_coqbug_15373 = 0
b = b""
if not waiting_on_coqbug_15373:
os.write(1, b[-2:-1])
r = os.read(0, 1); b += r
if not r: sys.exit(not b.endswith(b"\n"))
if b == linesep: b = b"\n"
os.write(1, b[-2:-1])
b = b[-1:]
'

0 comments on commit 7c6a089

Please sign in to comment.