Skip to content
Snippets Groups Projects
Commit f46ed3b1 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

remove old proof-state scripts 

Superseded by alectryon, no longer needed.
parent d03906d8
No related branches found
No related tags found
No related merge requests found
Pipeline #50871 passed
Stage: build
Stage: process
This commit is part of merge request !136. Comments created here will be created in the context of that merge request.
Hide whitespace changes
Inline Side-by-side
scripts/intersperse-proof-state.py deleted 100755 → 0
+ 0
− 114
View file @ d03906d8
#!/usr/bin/env python3
# Copyright 2019 Björn Brandenburg <bbb@mpi-sws.org>
#
# Redistribution and use in source and binary forms, with or without
# modification, are permitted provided that the following conditions are met:
#
# 1. Redistributions of source code must retain the above copyright notice, this
# list of conditions and the following disclaimer.
#
# 2. Redistributions in binary form must reproduce the above copyright notice,
# this list of conditions and the following disclaimer in the documentation
# and/or other materials provided with the distribution.
#
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
# DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
# FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
# DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
# SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
# OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
import argparse
import os
import sys
import json
SEP_TOP = "[ coqtop ]".center(77, '-')
SEP_BOTTOM= "-" * 77
def intersperse(src, proofstate, out):
last = None
for interaction in proofstate:
if 'start' in interaction and 'end' in interaction:
assert type(interaction['start']) == int
assert type(interaction['end']) == int
assert interaction['start'] < len(src)
assert interaction['end'] <= len(src)
start = interaction['start']
end = min(interaction['end'] + 1, len(src))
input = src[start:end]
print(input, end='', file=out)
last = end
if 'output' in interaction:
print("\n(* %s\n" % SEP_TOP, file=out)
for line in interaction['output']:
print(line, file=out)
print("\n%s *)\n" % SEP_BOTTOM, file=out)
if not last is None and last + 1 < len(src):
# print trailing leftovers of file
input = src[last + 1:]
print(input, end='', file=out)
def process(opts, fname):
print("Interspersing proof state in %s..." % fname)
# read the source
src = open(fname, 'r').read()
# load the proof state
ext = '.proofstate.json'
proofstate_fname = os.path.join(opts.proof_state_prefix,
fname.replace('.v', ext))
proofstate = json.load(open(proofstate_fname, 'r'))
# create the output file
output_file = os.path.join(opts.output_prefix, fname)
path = os.path.dirname(output_file)
os.makedirs(path, exist_ok=True)
out = open(output_file, 'w')
intersperse(src, proofstate, out)
def parse_args():
parser = argparse.ArgumentParser(
description="intersperse recorded proof state with Coq source")
parser.add_argument('input_files', nargs='*',
metavar='Coq-file',
help='input Coq files (*.v)')
parser.add_argument('-o', '--output-prefix', default="./with-proof-state",
action='store', type=str,
help='path prefix for output file(s)')
parser.add_argument('-p', '--proof-state-prefix', default="./proof-state",
action='store', type=str,
help='where to find the *.proofstate.json files')
return parser.parse_args()
def main():
opts = parse_args()
had_problem = False
for f in opts.input_files:
try:
process(opts, f)
except OSError as e:
print(e, file=sys.stderr)
had_problem = True
if had_problem:
# signal something went wrong with non-zero exit code
sys.exit(1)
if __name__ == '__main__':
main()
scripts/record-proof-state.py deleted 100755 → 0
+ 0
− 494
View file @ d03906d8
#!/usr/bin/env python3
# Copyright 2019 Björn Brandenburg <bbb@mpi-sws.org>
#
# Redistribution and use in source and binary forms, with or without
# modification, are permitted provided that the following conditions are met:
#
# 1. Redistributions of source code must retain the above copyright notice, this
# list of conditions and the following disclaimer.
#
# 2. Redistributions in binary form must reproduce the above copyright notice,
# this list of conditions and the following disclaimer in the documentation
# and/or other materials provided with the distribution.
#
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
# DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
# FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
# DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
# SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
# OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
import argparse
import sys
import os
import re
import time
from subprocess import Popen, PIPE
from select import select
import json
# YAML support is not part of the standard library, so try loading it carefully
try:
import yaml
have_yaml = True
except:
have_yaml = False
def statement_end_offsets(opts, src):
"""A naive splitter for Coq .v files.
Pays attention to nested comments and considers each period followed
by whitespace to be the end of something that should be sent to coqtop.
Returns an iterator over the indices within the src string where
statements end.
"""
def cur_is(i, c):
return src[i] == c
def next_is(i, c):
if i + 1 < len(src):
return src[i + 1] == c
else:
return False
def prev_is(i, c):
if i > 0:
return src[i - 1] == c
else:
return False
def next_is_whitespace(i):
if i + 1 < len(src):
return src[i + 1].isspace()
else:
# For practical purposes, let's count EOF as white space.
return True
def prev_is_whitespace(i):
if i > 0:
return src[i - 1].isspace()
else:
return False
def cur_is_bullet(i):
return src[i] in "-+*"
def only_whitespace_since_newline(i):
while i > 0:
i -= 1
if not src[i].isspace():
return False
if src[i] == '\n':
return True
return True
def end_of_bullet(i):
while i < len(src) and cur_is_bullet(i):
i += 1
if i >= len(src):
return False
if src[i].isspace():
return i
else:
return False
def start_of_proof(i):
return src[:i].endswith("Proof") \
or src[:i].endswith("Next Obligation")
in_comment = 0
in_proof = 0
def end_of_proof(i):
return src[:i].endswith("Qed") \
or (in_proof and src[:i].endswith("Defined"))
last = -1
seen_non_whitespace_since_last = False
i = 0
while i < len(src):
comment_just_ended = False
if opts.parse_only and opts.verbose:
print("%7d [%s] comment:%d proof:%d ns:%d nsnl:%d bullet:%d last:%d" % (
i,
src[i].replace('\n', '\\n'),
in_comment,
in_proof,
seen_non_whitespace_since_last,
not only_whitespace_since_newline(i),
cur_is_bullet(i),
last
))
assert in_comment >= 0
assert in_proof >= 0
# comment starting?
if cur_is(i, '(') and next_is(i, '*'):
in_comment += 1
i += 1 # skip next
# comment ending?
elif cur_is(i, '*') and next_is(i, ')'):
in_comment -= 1
i += 1 # skip next
comment_just_ended = True
# look for statements ending in a period
elif not in_comment and cur_is(i, '.') and next_is_whitespace(i):
if start_of_proof(i):
in_proof += 1
elif end_of_proof(i):
in_proof -= 1
yield i + 1
last = i + 1
# look for closing braces -- this is a brittle heuristic, but
# we need to catch sub-proofs because coqtop in emacs mode
# produces a prompt every time we enter a sub-proof
elif not in_comment and in_proof and cur_is(i, '}') and \
(next_is_whitespace(i) or next_is (i, '}')) and \
(prev_is_whitespace(i) or prev_is(i, '}')):
if next_is_whitespace(i):
yield i + 1
last = i + 1
else:
yield i
last = i
# similarly, look for opening braces
elif not in_comment and in_proof and cur_is(i, '{') \
and next_is_whitespace(i) and prev_is_whitespace(i):
yield i + 1
last = i + 1
# detect bulleted sub-proofs for the same reason
elif not in_comment and in_proof and cur_is_bullet(i) \
and only_whitespace_since_newline(i) \
and not seen_non_whitespace_since_last:
# bullets can consist of multiple characters
end = end_of_bullet(i)
if not end is False:
yield end
last = end
i = end # skip over entire bullet
# otherwise just skip over this
# reset flags
if i == last:
seen_non_whitespace_since_last = False
elif not (in_comment or comment_just_ended) and not src[i].isspace():
seen_non_whitespace_since_last = True
# advance to next character
i += 1
def launch_coqtop(opts):
# Let the shell figure out where coqtop is and resolve the options.
# A bit naive but works for now.
return Popen("coqtop -emacs %s" % opts.coqtop_opts, stdin=PIPE, stdout=PIPE,
stderr=PIPE, shell=True, bufsize=0)
START_OF_PROMPT = "<prompt>"
END_OF_PROMPT = "</prompt>"
END_OF_PROMPT_BYTES = bytes(END_OF_PROMPT, 'utf-8')
def read_from_pipe(pipe, timeout, seen_enough = lambda _: False, expect_timeout=False):
output = bytearray()
while not seen_enough(output):
(readable, writable, exceptional) = select([pipe], [], [], timeout)
if not readable:
# we timed out, nothing to read
if timeout > 0:
if not expect_timeout:
print('=' * 30 + "[ TIMEOUT ]" + '=' * 30)
break
else:
data = readable[0].read(512)
if len(data) == 0:
# reached end of pipe
break
else:
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)
while True:
more = read_from_pipe(pipe, 0, seen_enough, expect_timeout=True)
output += more
if more:
print("Unexpected coqtop output:", more)
assert False # we lost sync; this should not be happening
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)
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)
INFO_MSG_PATTERN = re.compile(
r"""
<infomsg> # Opening tag
(.*?) # whatever message — don't be greedy to not skip over closing tag
</infomsg> # Closing tag
\n? # if the message is at the end of a line, remove the newline as well
"""
, re.VERBOSE | re.DOTALL)
def extract_info_messages(output):
infos = [m.group(1).rstrip() for m in INFO_MSG_PATTERN.finditer(output)]
rest = INFO_MSG_PATTERN.sub('', output)
return (infos, rest)
def wait_for_coqtop(opts, coqtop):
# wait until prompt (re-)appears
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)
interaction = {}
output = output.rstrip()
if output:
interaction['output'] = output.split('\n')
error = error.rstrip()
if error:
interaction['error'] = error
if num >= 0:
interaction['prompt_number'] = num
return interaction
def interact(opts, coqtop, src, start, end):
input = src[start:end+1]
# feed line to coqtop
# remove any line breaks, we only want coqtop to prompt us once
coqtop.stdin.write(bytes(input.replace('\n', ' ') + '\n', "utf-8"))
coqtop.stdin.flush()
# wait until prompt (re-)appears
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)
# extract any info messages from the output
(infos, output) = extract_info_messages(output)
interaction = {
'start' : start,
'end' : end,
'input' : input.rstrip().split('\n'),
}
if infos:
interaction['messages'] = infos
output = output.rstrip()
if output:
interaction['output'] = output.split('\n')
error = error.rstrip()
if error:
interaction['error'] = error
if num >= 0:
interaction['prompt_number'] = num
return interaction
def report(n, interaction):
print("+" * 80)
if 'input' in interaction:
print("INPUT < %d : [%s]" % (n, "\n".join(interaction['input'])))
if 'output' in interaction:
print("OUTPUT:\n%s" % "\n".join(interaction['output']))
else:
print("<NO-OUTPUT>")
if 'error' in interaction:
print("PROMPT: [%s]" % interaction['error'].strip())
print("-" * 80)
def prompt_out_of_sync(opts, input_number, interaction):
if 'prompt_number' in interaction:
if interaction['prompt_number'] != input_number:
print("[%s] Out of sync: prompt %d in response to input %d" %
(opts.fname, interaction['prompt_number'], input_number))
return True
return False
def output_out_of_sync(opts, cmd, interactions):
if cmd == 'Qed.':
# QED: there should be no more proof obligations.
if 'output' in interactions[-2] and \
interactions[-2]['output'] != ['No more subgoals.']:
print("[%s] Out of sync: 'Qed.' before 'No more subgoals.'" % opts.fname)
return True
# QED: there should be no output.
if 'output' in interactions[-1]:
print("[%s] Out of sync: 'Qed.' produced output.'" % opts.fname)
return True
elif cmd.startswith('End '):
# End of section.
if 'output' in interactions[-1]:
print("[%s] Out of sync: 'End' produced output.'" % opts.fname)
return True
return False
# Some vernacular commands that we need to check for because they change
# coqtop's prompt counter. This list is likely incomplete.
VERNACULAR_COMMANDS_RE = re.compile(r"(Opaque|Transparent) \S+\.")
def feed_to_coqtop(opts, src):
coqtop = launch_coqtop(opts)
interactions = []
# wait for coqtop startup to finish
interaction = wait_for_coqtop(opts, coqtop)
if opts.verbose:
report(0, interaction)
interactions.append(interaction)
coq_prompt_offset = 0
# feed statements
last = 0
for end in statement_end_offsets(opts, src):
if opts.pause:
time.sleep(0.1)
cmd = src[last:end+1].strip()
if VERNACULAR_COMMANDS_RE.match(cmd):
coq_prompt_offset += 1
interaction = interact(opts, coqtop, src, last, end)
interactions.append(interaction)
last = end + 1
sync_failure = False
sync_failure |= prompt_out_of_sync(opts, len(interactions) + coq_prompt_offset, interaction)
sync_failure |= output_out_of_sync(opts, cmd, interactions)
if opts.verbose or sync_failure:
report(len(interactions) + coq_prompt_offset, interaction)
assert not sync_failure
# signal end of input
coqtop.stdin.close()
# wait for coqtop to terminate
trailing_interactions = 0
while coqtop.poll() is None:
interaction = wait_for_coqtop(opts, coqtop)
if 'output' in interaction or 'error' in interaction:
trailing_interactions += 1
interactions.append(interaction)
if opts.verbose:
report(len(interactions), interaction)
assert trailing_interactions <= 1
return interactions
def process(opts, fname):
print("Collecting proof state for %s..." % fname)
opts.fname = fname
src = open(fname, 'r').read()
interactions = feed_to_coqtop(opts, src)
ext = '.proofstate.yaml' if opts.yaml else '.proofstate.json'
output_file = os.path.join(opts.output_prefix,
fname.replace('.v', ext))
path = os.path.dirname(output_file)
os.makedirs(path, exist_ok=True)
out = open(output_file, 'w')
if opts.yaml:
yaml.dump(interactions, out, sort_keys=False)
else:
json.dump(interactions, out, sort_keys=False, indent=4)
out.close()
def dump_structure(opts, fname):
print("=" * 80)
print("Statements in %s: \n" % fname)
print("-" * 80)
src = open(fname, 'r').read()
last = 0
for end in statement_end_offsets(opts, src):
print("%s" % src[last:end+1].replace('\n', ' '))
last = end + 1
print("-" * 80)
def parse_args():
parser = argparse.ArgumentParser(
description="record proof state by interacting with coqtop")
parser.add_argument('input_files', nargs='*',
metavar='Coq-file',
help='input Coq files (*.v)')
parser.add_argument('-t', '--timeout', default=5,
action='store', type=float,
help='how long for coqtop to wait to respond (in seconds)')
parser.add_argument('-c', '--coqtop-opts', default="",
action='store', type=str,
help='options to pass to coqtop')
parser.add_argument('-o', '--output-prefix', default="./proof-state",
action='store', type=str,
help='path prefix for output file(s)')
parser.add_argument('--yaml', default=False, action='store_true',
help='store results as YAML instead of JSON (requires pyyaml)')
parser.add_argument('--verbose', default=False, action='store_true',
help='report on interaction with coqtop')
parser.add_argument('--pause', default=False, action='store_true',
help='pause briefly before feeding data to coqtop')
parser.add_argument('--parse-only', default=False, action='store_true',
help='report how the script splits the input '
'(--verbose for per-character info)')
return parser.parse_args()
def main():
opts = parse_args()
# YAML is not part of the Python standard library, so complain if we don't
# have it.
if opts.yaml and not have_yaml:
print("Error: could not import pyyaml library.", file=sys.stderr)
sys.exit(2)
had_problem = False
for f in opts.input_files:
try:
if opts.parse_only:
dump_structure(opts, f)
else:
process(opts, f)
except OSError as e:
print(e, file=sys.stderr)
had_problem = True
if had_problem:
# signal something went wrong with non-zero exit code
sys.exit(1)
if __name__ == '__main__':
main()
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment