Coq IRC Bot

.gitignore

*.cmx
*.cmxs
*.o
*.cmi
*.cmo
*.d
Makefile
coqpy
twistd.log
*.pyc
twistd.pid
coqpy.ml
config.json

__init__.py

ampconnector.py

import itertools
from twisted.internet import protocol, defer, error
from twisted.python import log

gen = itertools.count()
TO_CHILD = 0
FROM_CHILD = 1

class AMPConnector(protocol.ProcessProtocol):
    """
    A L{ProcessProtocol} subclass that can understand and speak AMP.

    @ivar amp: the children AMP process
    @type amp: L{amp.AMP}

    @ivar finished: a deferred triggered when the process dies.
    @type finished: L{defer.Deferred}

    @ivar name: Unique name for the connector, much like a pid.
    @type name: int
    """

    def __init__(self, proto, name=None):
        """
        @param proto: An instance or subclass of L{amp.AMP}
        @type proto: L{amp.AMP}

        @param name: optional name of the subprocess.
        @type name: int
        """
        self.finished = defer.Deferred()
        self.amp = proto
        self.name = name
        if name is None:
            self.name = gen.next()

    def signalProcess(self, signalID):
        """
        Send the signal signalID to the child process

        @param signalID: The signal ID that you want to send to the
                        corresponding child
        @type signalID: C{str} or C{int}
        """
        return self.transport.signalProcess(signalID)

    def connectionMade(self):
        log.msg("Subprocess %s started." % (self.name,))
        self.amp.makeConnection(self)

    # Transport
    disconnecting = False

    def write(self, data):
        self.transport.writeToChild(TO_CHILD, data)

    def loseConnection(self):
        self.transport.closeChildFD(TO_CHILD)
        self.transport.closeChildFD(FROM_CHILD)
        self.transport.loseConnection()

    def getPeer(self):
        return ('subprocess',)

    def getHost(self):
        return ('no host',)

    def childDataReceived(self, childFD, data):
        if childFD == FROM_CHILD:
            self.amp.dataReceived(data)
            return
        self.errReceived(data)

    def errReceived(self, data):
        for line in data.strip().splitlines():
            log.msg("FROM %s: %s" % (self.name, line))

    def processEnded(self, status):
        log.msg("Process: %s ended" % (self.name,))
        self.amp.connectionLost(status)
        if status.check(error.ProcessDone):
            self.finished.callback('')
            return
        self.finished.errback(status)

client.py

from twisted.protocols import amp
from twisted.internet import reactor
from twisted.application import service

from rooster.ampconnector import AMPConnector
from rooster.commands import *

class RoosterClient(service.Service):
    libs = ['Program', 'List', 'Arith']

    def __init__(self, libs = None):
        self.rooster = amp.AMP()
        if libs:
            self.libs = libs
    def startService(self):
        reactor.spawnProcess(AMPConnector(self.rooster), './coqpy', ['python', '-m', 'rooster.server' ])
        for lib in self.libs:
            self.rooster.callRemote(RequireImport, module = lib).addErrback(lambda _ : None)
    def stopService(self):
        self.rooster.transport.signalProcess('TERM')

commands.py

from twisted.protocols import amp

class CoqCommand(amp.Command):
    errors = { RuntimeError: 'COQ_ERROR' }

class EvalCommand(CoqCommand):
    arguments = [('constr', amp.String())]
    response = [('term', amp.String()),
                ('type', amp.String())]
class Check(EvalCommand):
    pass
class Compute(EvalCommand):
    pass

class About(CoqCommand):
    arguments = [('reference', amp.String())]
    response = [('description', amp.String())]

class Print(CoqCommand):
    arguments = [('reference', amp.String())]
    response = [('description', amp.String())]

class RequireImport(CoqCommand):
    arguments = [('module', amp.String())]
    response = []

class Define(CoqCommand):
    arguments = [('definition', amp.String())]
    response = []

config.json.sample

{
     "host": "irc.freenode.net",
     "port": 6697,
     "useSSL": 1,
     "nick": "sample-roosterbot",
     "password": "sample-password",
     "channels": ["#bottest"]
}

coq-libs.list

Coq.Logic.Berardi
Coq.Logic.ChoiceFacts
Coq.Logic.ClassicalChoice
Coq.Logic.ClassicalDescription
Coq.Logic.ClassicalEpsilon
Coq.Logic.ClassicalFacts
Coq.Logic.Classical_Pred_Set
Coq.Logic.Classical_Pred_Type
Coq.Logic.Classical_Prop
Coq.Logic.Classical_Type
Coq.Logic.ClassicalUniqueChoice
Coq.Logic.Classical
Coq.Logic.ConstructiveEpsilon
Coq.Logic.Decidable
Coq.Logic.Description
Coq.Logic.Diaconescu
Coq.Logic.Epsilon
Coq.Logic.Eqdep_dec
Coq.Logic.EqdepFacts
Coq.Logic.Eqdep
Coq.Logic.FunctionalExtensionality
Coq.Logic.Hurkens
Coq.Logic.IndefiniteDescription
Coq.Logic.JMeq
Coq.Logic.ProofIrrelevanceFacts
Coq.Logic.ProofIrrelevance
Coq.Logic.RelationalChoice
Coq.Logic.SetIsType
Coq.Arith.Arith_base
Coq.Arith.Arith
Coq.Arith.Between
Coq.Arith.Bool_nat
Coq.Arith.Compare_dec
Coq.Arith.Compare
Coq.Arith.Div2
Coq.Arith.EqNat
Coq.Arith.Euclid
Coq.Arith.Even
Coq.Arith.Factorial
Coq.Arith.Gt
Coq.Arith.Le
Coq.Arith.Lt
Coq.Arith.Max
Coq.Arith.Minus
Coq.Arith.Min
Coq.Arith.Mult
Coq.Arith.Peano_dec
Coq.Arith.Plus
Coq.Arith.Wf_nat
Coq.Bool.BoolEq
Coq.Bool.Bool
Coq.Bool.Bvector
Coq.Bool.DecBool
Coq.Bool.IfProp
Coq.Bool.Sumbool
Coq.Bool.Zerob
Coq.PArith.BinPosDef
Coq.PArith.BinPos
Coq.PArith.Pnat
Coq.PArith.POrderedType
Coq.PArith.PArith
Coq.NArith.BinNatDef
Coq.NArith.BinNat
Coq.NArith.NArith
Coq.NArith.Ndec
Coq.NArith.Ndigits
Coq.NArith.Ndist
Coq.NArith.Nnat
Coq.NArith.Ndiv_def
Coq.NArith.Nsqrt_def
Coq.NArith.Ngcd_def
Coq.ZArith.auxiliary
Coq.ZArith.BinIntDef
Coq.ZArith.BinInt
Coq.ZArith.Int
Coq.ZArith.Wf_Z
Coq.ZArith.Zabs
Coq.ZArith.ZArith_base
Coq.ZArith.ZArith_dec
Coq.ZArith.ZArith
Coq.ZArith.Zdigits
Coq.ZArith.Zbool
Coq.ZArith.Zcompare
Coq.ZArith.Zcomplements
Coq.ZArith.Zdiv
Coq.ZArith.Zeven
Coq.ZArith.Zgcd_alt
Coq.ZArith.Zpow_alt
Coq.ZArith.Zhints
Coq.ZArith.Zlogarithm
Coq.ZArith.Zmax
Coq.ZArith.Zminmax
Coq.ZArith.Zmin
Coq.ZArith.Zmisc
Coq.ZArith.Znat
Coq.ZArith.Znumtheory
Coq.ZArith.Zquot
Coq.ZArith.Zorder
Coq.ZArith.Zpow_def
Coq.ZArith.Zpower
Coq.ZArith.Zpow_facts
Coq.ZArith.Zsqrt_compat
Coq.ZArith.Zwf
Coq.ZArith.Zeuclid
Coq.Setoids.Setoid
Coq.Lists.ListSet
Coq.Lists.ListTactics
Coq.Lists.List
Coq.Lists.SetoidList
Coq.Lists.StreamMemo
Coq.Lists.Streams
Coq.Strings.Ascii
Coq.Strings.String
Coq.Sets.Classical_sets
Coq.Sets.Constructive_sets
Coq.Sets.Cpo
Coq.Sets.Ensembles
Coq.Sets.Finite_sets_facts
Coq.Sets.Finite_sets
Coq.Sets.Image
Coq.Sets.Infinite_sets
Coq.Sets.Integers
Coq.Sets.Multiset
Coq.Sets.Partial_Order
Coq.Sets.Permut
Coq.Sets.Powerset_Classical_facts
Coq.Sets.Powerset_facts
Coq.Sets.Powerset
Coq.Sets.Relations_1_facts
Coq.Sets.Relations_1
Coq.Sets.Relations_2_facts
Coq.Sets.Relations_2
Coq.Sets.Relations_3_facts
Coq.Sets.Relations_3
Coq.Sets.Uniset
Coq.FSets.FMapAVL
Coq.FSets.FMapFacts
Coq.FSets.FMapFullAVL
Coq.FSets.FMapInterface
Coq.FSets.FMapList
Coq.FSets.FMapPositive
Coq.FSets.FMaps
Coq.FSets.FMapWeakList
Coq.FSets.FSetCompat
Coq.FSets.FSetAVL
Coq.FSets.FSetPositive
Coq.FSets.FSetBridge
Coq.FSets.FSetDecide
Coq.FSets.FSetEqProperties
Coq.FSets.FSetFacts
Coq.FSets.FSetInterface
Coq.FSets.FSetList
Coq.FSets.FSetProperties
Coq.FSets.FSets
Coq.FSets.FSetToFiniteSet
Coq.FSets.FSetWeakList
Coq.MSets.MSetAVL
Coq.MSets.MSetDecide
Coq.MSets.MSetEqProperties
Coq.MSets.MSetFacts
Coq.MSets.MSetInterface
Coq.MSets.MSetList
Coq.MSets.MSetProperties
Coq.MSets.MSets
Coq.MSets.MSetToFiniteSet
Coq.MSets.MSetWeakList
Coq.MSets.MSetPositive
Coq.Relations.Operators_Properties
Coq.Relations.Relation_Definitions
Coq.Relations.Relation_Operators
Coq.Relations.Relations
Coq.Wellfounded.Disjoint_Union
Coq.Wellfounded.Inclusion
Coq.Wellfounded.Inverse_Image
Coq.Wellfounded.Lexicographic_Exponentiation
Coq.Wellfounded.Lexicographic_Product
Coq.Wellfounded.Transitive_Closure
Coq.Wellfounded.Union
Coq.Wellfounded.Wellfounded
Coq.Wellfounded.Well_Ordering
Coq.Reals.Alembert
Coq.Reals.AltSeries
Coq.Reals.ArithProp
Coq.Reals.Binomial
Coq.Reals.Cauchy_prod
Coq.Reals.Cos_plus
Coq.Reals.Cos_rel
Coq.Reals.DiscrR
Coq.Reals.Exp_prop
Coq.Reals.Integration
Coq.Reals.LegacyRfield
Coq.Reals.MVT
Coq.Reals.NewtonInt
Coq.Reals.PartSum
Coq.Reals.PSeries_reg
Coq.Reals.Ranalysis1
Coq.Reals.Ranalysis2
Coq.Reals.Ranalysis3
Coq.Reals.Ranalysis4
Coq.Reals.Ranalysis
Coq.Reals.Raxioms
Coq.Reals.Rbase
Coq.Reals.Rbasic_fun
Coq.Reals.Rcomplete
Coq.Reals.Rdefinitions
Coq.Reals.Rderiv
Coq.Reals.Reals
Coq.Reals.Rfunctions
Coq.Reals.Rgeom
Coq.Reals.RiemannInt_SF
Coq.Reals.RiemannInt
Coq.Reals.R_Ifp
Coq.Reals.RIneq
Coq.Reals.Rlimit
Coq.Reals.RList
Coq.Reals.Rlogic
Coq.Reals.Rpow_def
Coq.Reals.Rpower
Coq.Reals.Rprod
Coq.Reals.Rseries
Coq.Reals.Rsigma
Coq.Reals.Rsqrt_def
Coq.Reals.R_sqrt
Coq.Reals.R_sqr
Coq.Reals.Rtopology
Coq.Reals.Rtrigo_alt
Coq.Reals.Rtrigo_calc
Coq.Reals.Rtrigo_def
Coq.Reals.Rtrigo_fun
Coq.Reals.Rtrigo_reg
Coq.Reals.Rtrigo
Coq.Reals.SeqProp
Coq.Reals.SeqSeries
Coq.Reals.SplitAbsolu
Coq.Reals.SplitRmult
Coq.Reals.Sqrt_reg
Coq.Reals.ROrderedType
Coq.Reals.Rminmax
Coq.Sorting.Heap
Coq.Sorting.Permutation
Coq.Sorting.PermutSetoid
Coq.Sorting.PermutEq
Coq.Sorting.Sorted
Coq.Sorting.Sorting
Coq.Sorting.Mergesort
Coq.QArith.Qabs
Coq.QArith.QArith_base
Coq.QArith.QArith
Coq.QArith.Qcanon
Coq.QArith.Qfield
Coq.QArith.Qpower
Coq.QArith.Qreals
Coq.QArith.Qreduction
Coq.QArith.Qring
Coq.QArith.Qround
Coq.QArith.QOrderedType
Coq.QArith.Qminmax
Coq.Numbers.BinNums
Coq.Numbers.BigNumPrelude
Coq.Numbers.Cyclic.Abstract.CyclicAxioms
Coq.Numbers.Cyclic.Abstract.NZCyclic
Coq.Numbers.Cyclic.DoubleCyclic.DoubleAdd
Coq.Numbers.Cyclic.DoubleCyclic.DoubleBase
Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic
Coq.Numbers.Cyclic.DoubleCyclic.DoubleDivn1
Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv
Coq.Numbers.Cyclic.DoubleCyclic.DoubleLift
Coq.Numbers.Cyclic.DoubleCyclic.DoubleMul
Coq.Numbers.Cyclic.DoubleCyclic.DoubleSqrt
Coq.Numbers.Cyclic.DoubleCyclic.DoubleSub
Coq.Numbers.Cyclic.DoubleCyclic.DoubleType
Coq.Numbers.Cyclic.Int31.Int31
Coq.Numbers.Cyclic.Int31.Cyclic31
Coq.Numbers.Cyclic.Int31.Ring31
Coq.Numbers.Cyclic.ZModulo.ZModulo
Coq.Numbers.Integer.Abstract.ZAddOrder
Coq.Numbers.Integer.Abstract.ZAdd
Coq.Numbers.Integer.Abstract.ZAxioms
Coq.Numbers.Integer.Abstract.ZBase
Coq.Numbers.Integer.Abstract.ZLt
Coq.Numbers.Integer.Abstract.ZMulOrder
Coq.Numbers.Integer.Abstract.ZMul
Coq.Numbers.Integer.Abstract.ZSgnAbs
Coq.Numbers.Integer.Abstract.ZDivFloor
Coq.Numbers.Integer.Abstract.ZDivTrunc
Coq.Numbers.Integer.Abstract.ZDivEucl
Coq.Numbers.Integer.Abstract.ZMaxMin
Coq.Numbers.Integer.Abstract.ZParity
Coq.Numbers.Integer.Abstract.ZPow
Coq.Numbers.Integer.Abstract.ZGcd
Coq.Numbers.Integer.Abstract.ZLcm
Coq.Numbers.Integer.Abstract.ZBits
Coq.Numbers.Integer.Abstract.ZProperties
Coq.Numbers.Integer.BigZ.BigZ
Coq.Numbers.Integer.BigZ.ZMake
Coq.Numbers.Integer.Binary.ZBinary
Coq.Numbers.Integer.NatPairs.ZNatPairs
Coq.Numbers.Integer.SpecViaZ.ZSig
Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms
Coq.Numbers.NaryFunctions
Coq.Numbers.NatInt.NZAddOrder
Coq.Numbers.NatInt.NZAdd
Coq.Numbers.NatInt.NZAxioms
Coq.Numbers.NatInt.NZBase
Coq.Numbers.NatInt.NZMulOrder
Coq.Numbers.NatInt.NZMul
Coq.Numbers.NatInt.NZOrder
Coq.Numbers.NatInt.NZProperties
Coq.Numbers.NatInt.NZDomain
Coq.Numbers.NatInt.NZParity
Coq.Numbers.NatInt.NZDiv
Coq.Numbers.NatInt.NZPow
Coq.Numbers.NatInt.NZSqrt
Coq.Numbers.NatInt.NZLog
Coq.Numbers.NatInt.NZGcd
Coq.Numbers.NatInt.NZBits
Coq.Numbers.Natural.Abstract.NAddOrder
Coq.Numbers.Natural.Abstract.NAdd
Coq.Numbers.Natural.Abstract.NAxioms
Coq.Numbers.Natural.Abstract.NBase
Coq.Numbers.Natural.Abstract.NDefOps
Coq.Numbers.Natural.Abstract.NIso
Coq.Numbers.Natural.Abstract.NMulOrder
Coq.Numbers.Natural.Abstract.NOrder
Coq.Numbers.Natural.Abstract.NStrongRec
Coq.Numbers.Natural.Abstract.NSub
Coq.Numbers.Natural.Abstract.NProperties
Coq.Numbers.Natural.Abstract.NDiv
Coq.Numbers.Natural.Abstract.NMaxMin
Coq.Numbers.Natural.Abstract.NParity
Coq.Numbers.Natural.Abstract.NPow
Coq.Numbers.Natural.Abstract.NSqrt
Coq.Numbers.Natural.Abstract.NLog
Coq.Numbers.Natural.Abstract.NGcd
Coq.Numbers.Natural.Abstract.NLcm
Coq.Numbers.Natural.Abstract.NBits
Coq.Numbers.Natural.BigN.BigN
Coq.Numbers.Natural.BigN.Nbasic
Coq.Numbers.Natural.BigN.NMake_gen
Coq.Numbers.Natural.BigN.NMake
Coq.Numbers.Natural.Binary.NBinary
Coq.Numbers.Natural.Peano.NPeano
Coq.Numbers.Natural.SpecViaZ.NSigNAxioms
Coq.Numbers.Natural.SpecViaZ.NSig
Coq.Numbers.NumPrelude
Coq.Numbers.Rational.BigQ.BigQ
Coq.Numbers.Rational.BigQ.QMake
Coq.Numbers.Rational.SpecViaQ.QSig
Coq.Unicode.Utf8
Coq.Unicode.Utf8_core
Coq.Classes.Equivalence
Coq.Classes.EquivDec
Coq.Classes.Init
Coq.Classes.Morphisms_Prop
Coq.Classes.Morphisms_Relations
Coq.Classes.Morphisms
Coq.Classes.RelationClasses
Coq.Classes.SetoidClass
Coq.Classes.SetoidDec
Coq.Classes.SetoidTactics
Coq.Classes.RelationPairs
Coq.Program.Basics
Coq.Program.Combinators
Coq.Program.Equality
Coq.Program.Program
Coq.Program.Subset
Coq.Program.Syntax
Coq.Program.Tactics
Coq.Program.Utils
Coq.Program.Wf
Coq.Structures.Equalities
Coq.Structures.EqualitiesFacts
Coq.Structures.Orders
Coq.Structures.OrdersEx
Coq.Structures.OrdersFacts
Coq.Structures.OrdersLists
Coq.Structures.OrdersTac
Coq.Structures.OrdersAlt
Coq.Structures.GenericMinMax
Coq.Structures.DecidableType
Coq.Structures.DecidableTypeEx
Coq.Structures.OrderedTypeAlt
Coq.Structures.OrderedTypeEx
Coq.Structures.OrderedType
Coq.Vectors.Fin
Coq.Vectors.VectorDef
Coq.Vectors.VectorSpec
Coq.Vectors.Vector
Coq.Init.Peano

coqpy.ml4

open Coqtop
open Toplevel
open Vernacexpr
open Vernac
open Pcoq
open Pp
open Pycaml
open Environ

let get_current_context_of_args = function
  | Some n -> Pfedit.get_goal_context n
  | None -> Lemmas.get_current_context ()

let vernac_check_may_eval redexp glopt rc =
  let module P = Pretype_errors in
  let (sigma, env) = get_current_context_of_args glopt in
  let sigma', c = Constrintern.interp_open_constr sigma env rc in
  let j =
    try
      Evarutil.check_evars env sigma sigma' c;
      Typeops.typing env c
    with P.PretypeError (_,_,P.UnsolvableImplicit _)
      | Compat.Loc.Exc_located (_,P.PretypeError (_,_,P.UnsolvableImplicit _)) ->
      Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in
  let {uj_val=trm; uj_type=typ} = j in
  let ntrm =
    match redexp with
    | None -> trm
    | Some r ->
        let redfun = fst (Redexpr.reduction_of_red_expr (Tacinterp.interp_redexp env sigma' r)) in
        redfun env sigma' trm
  in
  (Printer.pr_lconstr_env env ntrm, Printer.pr_ltype_env env typ)

let vernac_check = vernac_check_may_eval None None
let vernac_compute = vernac_check_may_eval (Some (Glob_term.Cbv Glob_term.all_flags)) None

  (*python();*)
  (*loop ();*)
let init args = Coqtop.init_toplevel (Array.to_list args)

let with_python_errors f a =
  try
    f a
  with
  | ex -> raise (Pycaml_exn (Pyerr_RuntimeError, string_of_ppcmds
  (print_toplevel_error (Cerrors.process_vernac_interp_error ex))) )

let parse_entry entry = Pcoq.parse_string (Pcoq.eoi_entry entry)
module Parse =
  struct
    let lconstr = parse_entry Pcoq.Constr.lconstr
    let smart_global = parse_entry Pcoq.Prim.smart_global
    let global = parse_entry Pcoq.Prim.reference
  end

let py_pp str = pystring_fromstring (string_of_ppcmds str)

let _py_check_constr =
  python_interfaced_function
  ~register_as:"coq.check_constr"
  ~docstring:"Returns a pair of strings corresponding to the term and type."
  [|StringType|]
  (with_python_errors (fun py_args ->
    let str = pystring_asstring py_args.(0) in
    let (trm, typ) = vernac_check (Parse.lconstr str) in
    pytuple2 (py_pp trm, py_pp typ)
  ))

let _py_compute_constr =
  python_interfaced_function
  ~register_as:"coq.compute_constr"
  ~docstring:"Returns a pair of strings corresponding to the term and type."
  [|StringType|]
  (with_python_errors (fun py_args ->
    let str = pystring_asstring py_args.(0) in
    let (trm, typ) = vernac_compute (Parse.lconstr str) in
    pytuple2 (py_pp trm, py_pp typ)
  ))

let _py_about_global =
  python_interfaced_function
  ~register_as:"coq.about_global"
  [|StringType|]
  (with_python_errors (fun py_args ->
    let str = pystring_asstring py_args.(0) in
    let global = Parse.smart_global str in
    py_pp (Prettyp.print_about global)
    ))

let _py_print_global =
  python_interfaced_function
  ~register_as:"coq.print_global"
  [|StringType|]
  (with_python_errors (fun py_args ->
    let str = pystring_asstring py_args.(0) in
    let global = Parse.smart_global str in
    py_pp (Prettyp.print_name global)
    ))

let vernac_require import qidl =
  let qidl = Libnames.qualid_of_reference qidl in
  Library.require_library [qidl] import

let vernac_import export qidl =
  let qidl = Libnames.qualid_of_reference qidl in
  Library.import_module export qidl

let _py_require =
  python_interfaced_function
  ~register_as:"coq.require"
  [|StringType|]
  (with_python_errors (fun py_args ->
    let str = pystring_asstring py_args.(0) in
    let global = Parse.global str in
    vernac_require None global;
    pynone()
  ))

let _py_import =
  python_interfaced_function
  ~register_as:"coq.import_"
  [|StringType|]
  (with_python_errors (fun py_args ->
    let str = pystring_asstring py_args.(0) in
    let global = Parse.global str in
    vernac_import false global;
    pynone()
  ))

let _py_require_import =
  python_interfaced_function
  ~register_as:"coq.require_import"
  [|StringType|]
  (with_python_errors (fun py_args ->
    let str = pystring_asstring py_args.(0) in
    let global = Parse.global str in
    vernac_require (Some true) global;
    pynone()
  ))

let _py_init =
  python_interfaced_function
  ~register_as:"coq.init"
  [|AnyType |]
  (fun args -> Flags.make_silent true; init (py_string_list_as_array args.(0)); pynone ())

open Gram
let def_body = Gram.entry_create "python:def"

open Pcoq
GEXTEND Gram
  def_body: [
    [ id = Prim.identref; bl = Constr.binders; ":="; c = Constr.lconstr ->
        (match c with
        | Topconstr.CCast(_,c, Glob_term.CastConv (Term.DEFAULTcast,t)) ->
               (id, bl, c, Some t)
        | _ -> (id, bl, c, None))
        | id = Prim.identref; bl = Constr.binders; ":"; t = Constr.lconstr ; ":="; c = Constr.lconstr ->
        (id, bl, c, None)
  ] ]
  ;
END

let vernac_def ((_, id), bl, c, t) =
  let ce,imps = Command.interp_definition bl None c t in
  Command.declare_definition id (Decl_kinds.Local, Decl_kinds.Definition) ce imps (fun _ _ -> ())

let _py_require_import =
  python_interfaced_function
  ~register_as:"coq.define"
  [|StringType|]
  (with_python_errors (fun py_args ->
    let str = pystring_asstring py_args.(0) in
    let def = parse_entry def_body str in
    vernac_def def;
    pynone()
  ))

coqpy_main.c

int main(int argc, char* argv)
{
	char* camlargs[] ={"coqpy", 0};
	caml_startup(camlargs);
	return Py_Main(argc, argv);
}

Make

coqpy.ml4
-I +pycaml
-custom "coqmktop $(OCAMLLIBS) -opt -o coqpy -no-start bigarray.cmxa pycaml.cmxa coqpy.cmx coqpy_main.c" "coqpy.cmxs coqpy_main.c" coqpy

roosterbot.py

# Copyright (c) Twisted Matrix Laboratories.
# See LICENSE for details.

"""
An example IRC log bot - logs a channel's events to a file.

If someone says the bot's name in the channel followed by a ':',
e.g.

  <foo> logbot: hello!

the bot will reply:

  <logbot> foo: I am a log bot

Run this script with two arguments, the channel name the bot should
connect to, and file to log to, e.g.:

  $ python ircLogBot.py test test.log

will log channel #test to the file 'test.log'.
"""


# twisted imports
from twisted.words.protocols import irc
from twisted.internet import reactor, protocol
from twisted.python import log

from rooster.commands import *

def catch_coq_error(func):
    def wrapped(self, arg, who):
        d = func(self, arg, who)
        @d.addErrback
        def catchError(res):
            res.trap(RuntimeError)
            self.send("error: " + res.value.message)
        return d
    return wrapped

def kwargs(func):
    def wrapped(args):
        return func(**args)
    return wrapped


class RoosterBot(object):
    """commands for roosterbot"""

    @catch_coq_error
    def command_CHECK(self, constr, who):
        d = self.rooster.callRemote(Check, constr = constr)
        @d.addCallback
        @kwargs
        def _callback(term, type):
            self.send(term + " : " + type)
        return d
    command_CHECK.usage = "check <term> - Gives deduced term and type"
    command_default = command_CHECK

    @catch_coq_error
    def command_ABOUT(self, constr, who):
        d = self.rooster.callRemote(About, reference = constr)
        @d.addCallback
        @kwargs
        def _callback(description):
            self.send(description)
        return d
    command_ABOUT.usage = "about <identifier-or-notation> - Gives information about identifier"

    @catch_coq_error
    def command_PRINT(self, constr, who):
        d = self.rooster.callRemote(Print, reference = constr)
        @d.addCallback
        @kwargs
        def _callback(description):
            self.send(description)
        return d
    command_ABOUT.usage = "print <identifier-or-notation> - Gives definition of identifier"

    @catch_coq_error
    def command_COMPUTE(self, constr, who):
        d = self.rooster.callRemote(Compute, constr = constr)
        @d.addCallback
        @kwargs
        def _callback(term, type):
            self.send(term + " : " + type)
        return d
    command_COMPUTE.usage = "compute <term> - evaluates term"

    @catch_coq_error
    def command_DEF(self, define, who):
        d = self.rooster.callRemote(Define, definition = define)
        @d.addCallback
        def _callback(_):
            self.send("OK")
        return d
    command_DEF.usage = "def <id> <binder> [ : <type> ] := <term> - evaluates term"

roosterbot.tac

import os

from twisted.application import service
from words import IRC
from roosterbot import RoosterBot
from rooster.client import RoosterClient

# note: this line is matched against to check that this is a buildmaster
# directory; do not edit it.
application = service.Application('buildmaster')

import simplejson as json
config = json.load(open("config.json"))

m = IRC(commands=RoosterBot, **config)
m.setServiceParent(application)

libs = open('coq-libs.list').readlines()

m = RoosterClient(libs)
m.setServiceParent(application)
RoosterBot.rooster = m.rooster

server.py

from rooster.commands import *

import coq

class Rooster(amp.AMP):
    @Check.responder
    def check_constr(self, constr):
        (term, type) = coq.check_constr(constr)
        return {'term': term, 'type': type}
    @Compute.responder
    def compute_constr(self, constr):
        (term, type) = coq.compute_constr(constr)
        return {'term': term, 'type': type}
    @About.responder
    def about_global(self, reference):
        desc = coq.about_global(reference)
        return {'description': desc}
    @Print.responder
    def print_global(self, reference):
        desc = coq.print_global(reference)
        return {'description': desc}
    @RequireImport.responder
    def require_import(self, module):
        coq.require_import(module)
        return dict()

    @Define.responder
    def define(self, definition):
        coq.define(definition)
        return dict()

def main():
    from twisted.internet import reactor, stdio
    from twisted.internet.protocol import Factory
    coq.init(["-q"])
    stdio.StandardIO(Rooster())
    reactor.run()

if __name__ == '__main__':
    main()

words.py

# This file is part of Buildbot.  Buildbot is free software: you can
# redistribute it and/or modify it under the terms of the GNU General Public
# License as published by the Free Software Foundation, version 2.
#
# This program is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
# FOR A PARTICULAR PURPOSE.  See the GNU General Public License for more
# details.
#
# You should have received a copy of the GNU General Public License along with
# this program; if not, write to the Free Software Foundation, Inc., 51
# Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
#
# Copyright Buildbot Team Members


# code to deliver build status through TWISTED.Words (instant messaging
# protocols: irc, etc)

import re, shlex, random
from string import join, capitalize, lower

from twisted.internet import protocol, reactor
from twisted.words.protocols import irc
from twisted.python import log, failure
from twisted.application import internet, service
from twisted.internet import task

version = 1

# twisted.internet.ssl requires PyOpenSSL, so be resilient if it's missing
try:
    from twisted.internet import ssl
    have_ssl = True
except ImportError:
    have_ssl = False

class UsageError(ValueError):
    def __init__(self, string = "Invalid usage", *more):
        ValueError.__init__(self, string, *more)

class Contact(object):
    """I hold the state for a single user's interaction with the buildbot.

    This base class provides all the basic behavior (the queries and
    responses). Subclasses for each channel type (IRC, different IM
    protocols) are expected to provide the lower-level send/receive methods.

    """

    def __init__(self, channel):
        #StatusReceiver.__init__(self) doesn't exist
        self.channel = channel
        self.muted = False

    def getCommandMethod(self, command):
        meth = getattr(self, 'command_' + command.upper(), None)
        return meth

    def command_HELLO(self, args, who):
        self.send("yes?")

    def command_VERSION(self, args, who):
        self.send("roosterbot-v%s at your service" % version)
    command_VERSION.usage = "version - report version number"


    def command_MUTE(self, args, who):
        # The order of these is important! ;)
        self.send("Shutting up for now.")
        self.muted = True
    command_MUTE.usage = "mute - suppress all messages until a corresponding 'unmute' is issued"

    def command_UNMUTE(self, args, who):
        if self.muted:
            # The order of these is important! ;)
            self.muted = False
            self.send("I'm baaaaaaaaaaack!")
        else:
            self.send("You hadn't told me to be quiet, but it's the thought that counts, right?")
    command_UNMUTE.usage = "unmute - disable a previous 'mute'"

    def build_commands(self):
        commands = []
        for k in dir(self):
            if k.startswith('command_'):
                commands.append(k[8:].lower())
        commands.sort()
        return commands

    def command_HELP(self, args, who):
        args = shlex.split(args)
        if len(args) == 0:
            self.send("Get help on what? (try 'help <foo>', or 'commands' for a command list)")
            return
        command = args[0]
        meth = self.getCommandMethod(command)
        if not meth:
            raise UsageError, "no such command '%s'" % command
        usage = getattr(meth, 'usage', None)
        if usage:
            self.send("Usage: %s" % usage)
        else:
            self.send("No usage info for '%s'" % command)
    command_HELP.usage = "help <command> - Give help for <command>"

    def command_SOURCE(self, args, who):
        banner = "My source can be found at https://gist.github.com/1343032"
        self.send(banner)
    command_SOURCE.usage = "source - Gives pointer to bot source code"

    def command_COMMANDS(self, args, who):
        commands = self.build_commands()
        str = "buildbot commands: " + ", ".join(commands)
        self.send(str)
    command_COMMANDS.usage = "commands - List available commands"

class IRCContact(Contact):

    # this is the IRC-specific subclass of Contact

    def __init__(self, channel, dest):
        Contact.__init__(self, channel)
        # when people send us public messages ("buildbot: command"),
        # self.dest is the name of the channel ("#twisted"). When they send
        # us private messages (/msg buildbot command), self.dest is their
        # username.
        self.dest = dest

    def describeUser(self, user):
        if self.dest[0] == '#':
            return "IRC user <%s> on channel %s" % (user, self.dest)
        return "IRC user <%s> (privmsg)" % user

    # userJoined(self, user, channel)

    def send(self, message):
        if not self.muted:
            self.channel.msgOrNotice(self.dest, message)

    def act(self, action):
        if not self.muted:
            self.channel.me(self.dest, action)

    def handleMessage(self, message, who, useDefault=False):
        # a message has arrived from 'who'. For broadcast contacts (i.e. when
        # people do an irc 'buildbot: command'), this will be a string
        # describing the sender of the message in some useful-to-log way, and
        # a single Contact may see messages from a variety of users. For
        # unicast contacts (i.e. when people do an irc '/msg buildbot
        # command'), a single Contact will only ever see messages from a
        # single user.
        message = message.lstrip()

        parts = message.split(' ', 1)
        if len(parts) == 1:
            parts = parts + ['']
        cmd, args = parts
        log.msg("irc command", cmd)

        meth = self.getCommandMethod(cmd)
        if not meth and useDefault:
            args = message
            meth = self.command_default

        error = None
        try:
            if meth:
                meth(args.strip(), who)
        except UsageError, e:
            self.send(str(e))
        except:
            f = failure.Failure()
            log.err(f)
            error = "Something bad happened (see logs): %s" % f.type

        if error:
            try:
                self.send(error)
            except:
                log.err()

        #self.say(channel, "count %d" % self.counter)
        self.channel.counter += 1

class IrcStatusBot(irc.IRCClient):
    """I represent the buildbot to an IRC server.
    """
    contactClass = IRCContact

    def __init__(self, nickname, password, channels,
                 commands = None,
                 noticeOnChannel=False):
        """
        @type  nickname: string
        @param nickname: the nickname by which this bot should be known
        @type  password: string
        @param password: the password to use for identifying with Nickserv
        @type  channels: list of dictionaries
        @param channels: the bot will maintain a presence in these channels
        @type  status: L{buildbot.status.builder.Status}
        @param status: the build master's Status object, through which the
                       bot retrieves all status information
        @type  noticeOnChannel: boolean
        @param noticeOnChannel: Defaults to False. If True, error messages
                                for bot commands will be sent to the channel
                                as notices. Otherwise they are sent as a msg.
        @type  useRevisions: boolean
        @param useRevisions: if True, messages from the bot will use the
                             revisions from the Changes in the build and not
                             the build number.
        """
        self.nickname = nickname
        self.channels = channels
        self.password = password
        self.counter = 0
        self.contacts = {}
        self.commands = commands
        self.noticeOnChannel = noticeOnChannel
        self._keepAliveCall = task.LoopingCall(lambda: self.ping(self.nickname))
        class derived(self.contactClass, commands):
            pass
        self.contactClass = derived
    def connectionMade(self):
        irc.IRCClient.connectionMade(self)
        self._keepAliveCall.start(60)
    def connectionLost(self, reason):
        if self._keepAliveCall.running:
            self._keepAliveCall.stop()
        irc.IRCClient.connectionLost(self, reason)

    def msgOrNotice(self, dest, message):
        if self.noticeOnChannel and dest[0] == '#':
            self.notice(dest, message)
        else:
            self.msg(dest, message)

    def addContact(self, name, contact):
        self.contacts[name] = contact

    def getContact(self, name):
        if name in self.contacts:
            return self.contacts[name]
        new_contact = self.contactClass(self, name)
        self.contacts[name] = new_contact
        return new_contact

    def deleteContact(self, contact):
        name = contact.getName()
        if name in self.contacts:
            assert self.contacts[name] == contact
            del self.contacts[name]

    def log(self, msg):
        log.msg("%s: %s" % (self, msg))


    # the following irc.IRCClient methods are called when we have input

    def privmsg(self, user, channel, message):
        user = user.split('!', 1)[0] # rest is ~user@hostname
        # channel is '#twisted' or 'buildbot' (for private messages)
        channel = channel.lower()
        #print "privmsg:", user, channel, message
        if channel == self.nickname:
            # private message
            contact = self.getContact(user)
            contact.handleMessage(message, user)
            return
        # else it's a broadcast message, maybe for us, maybe not. 'channel'
        # is '#twisted' or the like.
        contact = self.getContact(channel)
        if message.startswith("%s:" % self.nickname) or message.startswith("%s," % self.nickname):
            message = message[len("%s:" % self.nickname):]
            contact.handleMessage(message, user)
        if message.startswith("@"):
            message = message[1:]
            contact.handleMessage(message, user, True)
        # to track users comings and goings, add code here

    def action(self, user, channel, data):
        #log.msg("action: %s,%s,%s" % (user, channel, data))
        user = user.split('!', 1)[0] # rest is ~user@hostname
        # somebody did an action (/me actions) in the broadcast channel
        contact = self.getContact(channel)
        if "buildbot" in data:
            contact.handleAction(data, user)

    def signedOn(self):
        if self.password:
            self.msg("Nickserv", "IDENTIFY " + self.password)
        for c in self.channels:
            if isinstance(c, dict):
                channel = c.get('channel', None)
                password = c.get('password', None)
            else:
                channel = c
                password = None
            self.join(channel=channel, key=password)

    def joined(self, channel):
        self.log("I have joined %s as %s" % (channel, self.nickname))
        # trigger contact contructor, which in turn subscribes to notify events
        self.getContact(channel)

    def left(self, channel):
        self.log("I have left %s" % (channel,))
    def kickedFrom(self, channel, kicker, message):
        self.log("I have been kicked from %s by %s: %s" % (channel,
                                                          kicker,
                                                          message))

    # we can using the following irc.IRCClient methods to send output. Most
    # of these are used by the IRCContact class.
    #
    # self.say(channel, message) # broadcast
    # self.msg(user, message) # unicast
    # self.me(channel, action) # send action
    # self.away(message='')
    # self.quit(message='')

class ThrottledClientFactory(protocol.ClientFactory):
    lostDelay = random.randint(1, 5)
    failedDelay = random.randint(45, 60)

    def __init__(self, lostDelay=None, failedDelay=None):
        if lostDelay is not None:
            self.lostDelay = lostDelay
        if failedDelay is not None:
            self.failedDelay = failedDelay

    def clientConnectionLost(self, connector, reason):
        reactor.callLater(self.lostDelay, connector.connect)

    def clientConnectionFailed(self, connector, reason):
        reactor.callLater(self.failedDelay, connector.connect)

class IrcStatusFactory(ThrottledClientFactory):
    protocol = IrcStatusBot

    status = None
    control = None
    shuttingDown = False
    p = None

    def __init__(self, nickname, password, channels, noticeOnChannel=False,
                 commands = None,
                 lostDelay=None, failedDelay=None):
        ThrottledClientFactory.__init__(self, lostDelay=lostDelay,
                                        failedDelay=failedDelay)
        self.status = None
        self.nickname = nickname
        self.password = password
        self.channels = channels
        self.commands = commands
        self.noticeOnChannel = noticeOnChannel

    def __getstate__(self):
        d = self.__dict__.copy()
        del d['p']
        return d

    def shutdown(self):
        self.shuttingDown = True
        if self.p:
            self.p.quit("buildmaster reconfigured: bot disconnecting")

    def buildProtocol(self, address):
        p = self.protocol(self.nickname, self.password, self.channels,
                          commands = self.commands,
                          noticeOnChannel = self.noticeOnChannel)
        p.factory = self
        p.control = self.control
        self.p = p
        return p

    # TODO: I think a shutdown that occurs while the connection is being
    # established will make this explode

    def clientConnectionLost(self, connector, reason):
        if self.shuttingDown:
            log.msg("not scheduling reconnection attempt")
            return
        ThrottledClientFactory.clientConnectionLost(self, connector, reason)

    def clientConnectionFailed(self, connector, reason):
        if self.shuttingDown:
            log.msg("not scheduling reconnection attempt")
            return
        ThrottledClientFactory.clientConnectionFailed(self, connector, reason)


class IRC(service.MultiService):
    """I am an IRC bot which can be queried for status information. I
    connect to a single IRC server and am known by a single nickname on that
    server, however I can join multiple channels."""

    def __init__(self, host, nick, channels, port=6667,
                 password=None,
                 noticeOnChannel = False,
                 commands = None,
                 useSSL=False,
                 lostDelay=None, failedDelay=None):
        service.MultiService.__init__(self)

        # need to stash these so we can detect changes later
        self.host = host
        self.port = port
        self.nick = nick
        self.channels = channels
        self.password = password
        self.commands = commands
        self.f = IrcStatusFactory(self.nick, self.password, self.channels,
                                  commands = self.commands,
                                  noticeOnChannel = noticeOnChannel,
                                  lostDelay = lostDelay, failedDelay = failedDelay)

        if useSSL:
            # SSL client needs a ClientContextFactory for some SSL mumbo-jumbo
            if not have_ssl:
                raise RuntimeError("useSSL requires PyOpenSSL")
            cf = ssl.ClientContextFactory()
            c = internet.SSLClient(self.host, self.port, self.f, cf)
        else:
            c = internet.TCPClient(self.host, self.port, self.f)

        c.setServiceParent(self)

    def stopService(self):
        # make sure the factory will stop reconnecting
        self.f.shutdown()
        return service.MultiService.stopService(self)