Created
November 6, 2011 15:32
-
-
Save tomprince/1343032 to your computer and use it in GitHub Desktop.
Coq IRC Bot
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
*.cmx | |
*.cmxs | |
*.o | |
*.cmi | |
*.cmo | |
*.d | |
Makefile | |
coqpy | |
twistd.log | |
*.pyc | |
twistd.pid | |
coqpy.ml | |
config.json |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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') |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 = [] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{ | |
"host": "irc.freenode.net", | |
"port": 6697, | |
"useSSL": 1, | |
"nick": "sample-roosterbot", | |
"password": "sample-password", | |
"channels": ["#bottest"] | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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() | |
)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
int main(int argc, char* argv) | |
{ | |
char* camlargs[] ={"coqpy", 0}; | |
caml_startup(camlargs); | |
return Py_Main(argc, argv); | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# 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" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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() |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# 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) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment