From 5c6d8f41aff3984d30398a075fc0718c988a1bcc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 10 Sep 2020 10:42:40 +0200
Subject: [PATCH] proof state recorder: check expected interaction number
If coqtop reports a different number of interactions in its prompt
than we provided, we're out of sync.
---
scripts/record-proof-state.py | 29 +++++++++++++++++++++++++----
1 file changed, 25 insertions(+), 4 deletions(-)
diff --git a/scripts/record-proof-state.py b/scripts/record-proof-state.py
index fb31cd7da..2efd7605f 100755
--- a/scripts/record-proof-state.py
+++ b/scripts/record-proof-state.py
@@ -198,6 +198,8 @@ def read_from_pipe(pipe, timeout, seen_enough = lambda _: False, expect_timeout=
output += data
return output.decode("utf-8")
+COQ_PROMPT_RE = re.compile(r"<prompt>\S* < ([0-9]+) ")
+
def wait_for_prompt(opts, pipe, timeout):
seen_enough = lambda output: output.endswith(END_OF_PROMPT_BYTES)
output = read_from_pipe(pipe, timeout, seen_enough)
@@ -211,13 +213,16 @@ def wait_for_prompt(opts, pipe, timeout):
else:
break
+ # check for interaction number in output
+ m = COQ_PROMPT_RE.search(output)
+ prompt_number = int(m.group(1)) if m else -1
# remove any prompts; we don't want to record those
if output.endswith(END_OF_PROMPT) and not opts.verbose:
idx = output.find(START_OF_PROMPT)
assert not START_OF_PROMPT in output[:idx] # only one prompt expected
- return output[:idx]
+ return (prompt_number, output[:idx])
else:
- return output
+ return (prompt_number, output)
INFO_MSG_PATTERN = re.compile(
r"""
@@ -235,7 +240,7 @@ def extract_info_messages(output):
def wait_for_coqtop(opts, coqtop):
# wait until prompt (re-)appears
- error = wait_for_prompt(opts, coqtop.stderr, opts.timeout)
+ num, error = wait_for_prompt(opts, coqtop.stderr, opts.timeout)
# read output produced so far
# FIXME: this only works if all output fits into the OS's pipe buffer
output = read_from_pipe(coqtop.stdout, 0)
@@ -246,6 +251,8 @@ def wait_for_coqtop(opts, coqtop):
error = error.rstrip()
if error:
interaction['error'] = error
+ if num >= 0:
+ interaction['prompt_number'] = num
return interaction
def interact(opts, coqtop, src, start, end):
@@ -255,7 +262,7 @@ def interact(opts, coqtop, src, start, end):
coqtop.stdin.write(bytes(input.replace('\n', ' ') + '\n', "utf-8"))
coqtop.stdin.flush()
# wait until prompt (re-)appears
- error = wait_for_prompt(opts, coqtop.stderr, opts.timeout)
+ num, error = wait_for_prompt(opts, coqtop.stderr, opts.timeout)
# read output produced so far
# FIXME: this only works if all output fits into the OS's pipe buffer
output = read_from_pipe(coqtop.stdout, 0)
@@ -280,6 +287,9 @@ def interact(opts, coqtop, src, start, end):
if error:
interaction['error'] = error
+ if num >= 0:
+ interaction['prompt_number'] = num
+
return interaction
def report(n, interaction):
@@ -294,6 +304,16 @@ def report(n, interaction):
print("PROMPT: [%s]" % interaction['error'].strip())
print("-" * 80)
+
+def check_sync(opts, input_number, interaction):
+ if 'prompt_number' in interaction:
+ if interaction['prompt_number'] != input_number:
+ print("Out of sync: prompt %d in response to input %d" %
+ (interaction['prompt_number'], input_number))
+ if not opts.verbose:
+ report(input_number, interaction)
+ assert False # out of sync: we missed an answer somewhere
+
def feed_to_coqtop(opts, src):
coqtop = launch_coqtop(opts)
interactions = []
@@ -310,6 +330,7 @@ def feed_to_coqtop(opts, src):
interaction = interact(opts, coqtop, src, last, end)
interactions.append(interaction)
last = end + 1
+ check_sync(opts, len(interactions), interaction)
if opts.verbose:
report(len(interactions), interaction)
--
GitLab