Coqd allows you to connect with a coqtop interactive session
Deals with Coq
Server for Coq protocol. Clients can connect and request server sessions based on a userid and a Coq command serialized into JSON:
{"command":"", "userid":""}
They then send commands and receive back JSON of
the schema:
{'userid': self.userid, 'response': res}
Implementation of the Coq Protocol which handles connection and disconnection of the server and roudtrips to and from the backend.
Talks to the specific backend instance associated with a userid
poll results from the coqtop backend
send results to our coqtop instance
Close out sessions and remove the userid from the tracking table
When the connection closes log the exit status
Parse data we’ve recieved and send to proof engine Expects JSON will be in the schema {“command”:”“, “userid”:”“}
Parse coqtop results and serialize
When a command is received send it to the specific backend for the given userid
Main entry points for coqd
Responsible for coqd configuration
Setup and run coqd
To use import the parser module object like so:
from coq.parser.gram import parser
The grammar for Coqtop interpreter output. Our grammar is the following:
S' -> proofst
proofst -> subgoal hyp goal term_prompt
proofst -> subgoal goal term_prompt
proofst -> sysmsg term_prompt
subgoal -> NUMBER SUBGOAL
hyp -> ID COLON PROP hyp
hyp -> ID COLON expr hyp
hyp -> ID COLON PROP
hyp -> ID COLON expr
goal -> GOALINE quantified_expr
goal -> GOALINE expr
quantified_expr -> forall
quantified_expr -> exists
forall -> FORALL idlist COLON ID COMMA expr
forall -> FORALL idlist COLON PROP COMMA expr
exists -> EXISTS idlist COLON ID COMMA expr
expr -> expr IMPL expr
expr -> expr AND expr
expr -> expr OR expr
expr -> expr LARRW expr
expr -> expr RARRW expr
expr -> LPAREN expr RPAREN
expr -> LBRKT expr RBRKT
expr -> idlist
idlist -> ID idlist
idlist -> TILDE idlist
idlist -> PLING idlist
idlist -> ID
term_prompt -> PROMPT proverstate PROMPT
sysmsg -> PROOF idlist DOT
proverstate -> thmname LARRW NUMBER PIPE thmlist NUMBER LARRW
statelist -> PIPE thmlist
thmlist -> thmname PIPE thmlist
thmlist -> thmname PIPE
thmname -> ID
thmname -> ID NUMBER
Token definitons for the Coqtop Output Language.
Warning
It is not meant to be used on its own and will not provide a useful language.
However you can use it with a parser by importing the tokens; to import the tokens object:
from coqd.parser.lexer import tokens