Skip to content

Commit

Permalink
Try a more robust way of parsing out the linesep
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross committed Sep 29, 2022
1 parent 1c9893d commit 5fc7137
Showing 1 changed file with 24 additions and 10 deletions.
34 changes: 24 additions & 10 deletions etc/bytedump.sh
Original file line number Diff line number Diff line change
Expand Up @@ -7,33 +7,47 @@ else
DEBUG="False"
fi

needle1="NEEDLE1"
needle2="COQTOP_CRAP_ENDS_HERE"

{
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 "${needle1}".
idtac "${needle2}".
PrintListByte.print_list_byte ${1}.
Abort.
EOF
} | python3 -c '
import os, sys
needle = b"COQTOP_CRAP_ENDS_HERE"
needle1 = b"'"${needle1}"'"
needle2 = b"'"${needle2}"'"
# waiting_on_coqbug_15373 = True
debug = '"$DEBUG"'
full = b""
b = b""
# first read to needle1
while not b.endswith(needle1):
r = os.read(0, 1)
if not r:
if debug: full += b
if debug: print(f"Error: waiting for {needle1!r} when reading {b!r}", file=sys.stderr)
sys.exit(2)
b += r
if debug: full += b
# parse line separator by reading to needle2
b = b""
# first read to needle
while not b.endswith(needle):
while not b.endswith(needle2):
r = os.read(0, 1)
if not r:
print(f"Error: waiting for {needle!r} when reading {b!r}", file=sys.stderr)
if debug: full += b
if debug: print(f"Error: waiting for {needle2!r} when reading {full!r}", file=sys.stderr)
sys.exit(2)
b += r
# parse line separator as the 1 or two characters before the needle which are either \r or \n
sep = b[-(len(needle)-2):-len(needle)]
if sep[1] not in b"\r\n":
print(f"Error: sep ({sep!r}) does not end with \\r nor \\n when reading {b!r}", file=sys.stderr)
sys.exit(3)
if debug: full += b
sep = b[:-len(needle2)]
# skip sep
r = os.read(0, len(sep))
if debug: full = b + r
Expand Down

0 comments on commit 5fc7137

Please sign in to comment.