Coqd: Coqtop Server

Coqd allows you to connect with a coqtop interactive session

API Reference

Base

Deals with Coq

class coqd.base.CoqProc(group=None, target=None, name=None, args=(), kwargs={})

Handles the shell process conncetion

run(conn)

Attempts to connect with the fork and send a command

start()

Execs a new child for coqtop

terminate(Force=False)

Have the child terminate

Connserv

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}
class coqd.connserv.CoqProtocol

Implementation of the Coq Protocol which handles connection and disconnection of the server and roudtrips to and from the backend.

class ActiveConn(userid)

Talks to the specific backend instance associated with a userid

read()

poll results from the coqtop backend

send(data)

send results to our coqtop instance

CoqProtocol.cleanup_session(userid)

Close out sessions and remove the userid from the tracking table

CoqProtocol.connectionLost(reason)

When the connection closes log the exit status

CoqProtocol.dataReceived(data)

Parse data we’ve recieved and send to proof engine Expects JSON will be in the schema {“command”:”“, “userid”:”“}

CoqProtocol.do_parse(output)

Parse coqtop results and serialize

CoqProtocol.handle_command(userid, command)

When a command is received send it to the specific backend for the given userid

Runner

Main entry points for coqd

class coqd.runner.Configurator(config_files)

Responsible for coqd configuration

coqd.runner.main()

Setup and run coqd

Gram

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

Lexer

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

Table Of Contents

Previous topic

Cockerel

This Page