From 062a16aa6fb3ed2ac58f0c918cf5764d843ae0f9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 10 Sep 2020 11:13:28 +0200
Subject: [PATCH] proof state recorder: fix double prompt detection
---
scripts/record-proof-state.py | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/scripts/record-proof-state.py b/scripts/record-proof-state.py
index 13a9ec1f1..19668dcbf 100755
--- a/scripts/record-proof-state.py
+++ b/scripts/record-proof-state.py
@@ -209,7 +209,7 @@ def wait_for_prompt(opts, pipe, timeout):
more = read_from_pipe(pipe, 0, seen_enough, expect_timeout=True)
output += more
if more:
- print("unexpected:", more)
+ print("Unexpected coqtop output:", more)
assert False # we lost sync; this should not be happening
else:
break
@@ -220,7 +220,9 @@ def wait_for_prompt(opts, pipe, timeout):
# 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
+ if START_OF_PROMPT in output[idx+1:]:
+ print("Unexpected number of prompts in coqtop output: \n", output)
+ assert False # only one prompt expected
return (prompt_number, output[:idx])
else:
return (prompt_number, output)
--
GitLab