1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
|
##########################################################################
## # The Rocq Prover / The Rocq Development Team ##
## v # Copyright INRIA, CNRS and contributors ##
## <O___,, # (see version control and CREDITS file for authors & dates) ##
## \VV/ ###############################################################
## // # This file is distributed under the terms of the ##
## # GNU Lesser General Public License Version 2.1 ##
## # (see LICENSE file for the text of the license) ##
##########################################################################
"""
Drive rocq top with Python!
=========================
This module is a simple pexpect-based driver for rocq top, based on the old
REPL interface.
"""
import os
import re
import tempfile
import pexpect
class CoqTopError(Exception):
def __init__(self, err, last_sentence, before):
super().__init__()
self.err = err
self.before = before
self.last_sentence = last_sentence
class CoqTop:
"""Create an instance of rocq top.
Use this as a context manager: no instance of rocq top is created until
you call `__enter__`. rocq top is terminated when you `__exit__` the
context manager.
Sentence parsing is very basic for now (a "." in a quoted string will
confuse it).
When environment variable COQ_DEBUG_REFMAN is set, all the input
we send to rocq top is copied to a temporary file "/tmp/coqdomainXXXX.v".
"""
COQTOP_PROMPT = re.compile("\r\n[^< \r\n]+ < ")
def __init__(self, rocqbin=None, color=False, args=None) -> str:
"""Configure a rocq top instance (but don't start it yet).
:param rocqbin: The path to rocq; uses $COQBIN by default, falling
back to "rocq"
:param color: When True, tell "rocq top" to produce ANSI color
codes (see the ansicolors module)
:param args: Additional arguments to "rocq top".
"""
self.rocqbin = rocqbin or os.path.join(os.getenv("COQBIN", ""), "rocq")
if not pexpect.utils.which(self.rocqbin):
raise ValueError("'{}: not found".format(rocqbin))
self.args = ["top"] + (args or []) + ["-q"] + ["-color", "on"] * color
self.rocqtop = None
self.debugfile = None
def __enter__(self):
if self.rocqtop:
raise ValueError("This module isn't re-entrant")
self.rocqtop = pexpect.spawn(self.rocqbin, args=self.args, echo=False, encoding="utf-8")
# Disable delays (http://pexpect.readthedocs.io/en/stable/commonissues.html?highlight=delaybeforesend)
self.rocqtop.delaybeforesend = 0
if os.getenv ("COQ_DEBUG_REFMAN"):
self.debugfile = tempfile.NamedTemporaryFile(mode="w+", prefix="coqdomain", suffix=".v", delete=False, dir="/tmp/")
self.next_prompt()
return self
def __exit__(self, type, value, traceback):
if self.debugfile:
self.debugfile.close()
self.debugfile = None
self.rocqtop.kill(9)
def next_prompt(self):
"""Wait for the next rocq top prompt, and return the output preceding it."""
self.rocqtop.expect(CoqTop.COQTOP_PROMPT, timeout = 10)
return self.rocqtop.before
def sendone(self, sentence):
"""Send a single sentence to rocq top.
:sentence: One Rocq sentence (otherwise, rocq top will produce multiple
prompts and we'll get confused)
"""
# Suppress newlines, but not spaces: they are significant in notations
sentence = re.sub(r"[\r\n]+", " ", sentence).strip()
try:
if self.debugfile:
self.debugfile.write(sentence+"\n")
self.rocqtop.sendline(sentence)
output = self.next_prompt()
except Exception as err:
raise CoqTopError(err, sentence, self.rocqtop.before)
return output
def send_initial_options(self):
"""Options to send when starting the toplevel and after a Reset Initial."""
self.sendone('Set Coqtop Exit On Error.')
self.sendone('Set Warnings "+default".')
def sendmany(*sentences):
"""A small demo: send each sentence in sentences and print the output"""
with CoqTop() as rocqtop:
for sentence in sentences:
print("=====================================")
print(sentence)
print("-------------------------------------")
response = rocqtop.sendone(sentence)
print(response)
def main():
"""Run a simple performance test and demo `sendmany`"""
with CoqTop() as rocqtop:
for _ in range(200):
print(repr(rocqtop.sendone("Check nat.")))
sendmany("Goal False -> True.", "Proof.", "intros H.",
"Check H.", "Chchc.", "apply I.", "Qed.")
if __name__ == '__main__':
main()
|
