h&93$      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                               !NoneNone )None KNone ?l! Safe-InferredNoneproof-assistant-botRequest from Telegram. proof-assistant-bot*Telegram ChatId (for reply and isolation). proof-assistant-botTelegram MessageId (for reply). proof-assistant-botMessage content. proof-assistant-botCast Telegram Update to .  None #$  proof-assistant-botResponse for Telegram.proof-assistant-botTelegram ChatId (for reply).proof-assistant-botTelegram MessageId (for reply).proof-assistant-bot output data.proof-assistant-botCast   to . If first argument is ? then it will wrap message in Monospace font and mark it with  MarkdownV2 parse mode. Otherwise, text message will be sent. For all responses from Backends  should be specified.proof-assistant-botCast  and output data to  .  None #8:<proof-assistant-botHelper to get queue size (communication model between bot and backend worker).proof-assistant-bot3Combination of all supported interpreters settings.proof-assistant-botLimits."proof-assistant-botResource settings.5proof-assistant-botArend requires different directories to work correctly. One of them used to store libraries, settings, user projects. We call it "root directory".6proof-assistant-bot?For each project Arend requires yaml file with a specific name.7proof-assistant-botFor each project Arend requires yaml file to store specific settings inside.8proof-assistant-botSince Arend requires project per chat, it will have a single module inside and we want to give it a common specific configurable name.<proof-assistant-botLean requires project where to store source files for typechecking.Cproof-assistant-botTimeout in seconds.Dproof-assistant-bot9Max number of GHC allocations for the interpreter thread.Eproof-assistant-botinput size in bytes.Fproof-assistant-botPrefix to filepath to avoid confusion between different interpreters.Gproof-assistant-bot#File extension used by interpreter.Jproof-assistant-botCLI arguments.Kproof-assistant-botPath to executable.Lproof-assistant-botTime, in seconds.Mproof-assistant-botPriority for the thread.Nproof-assistant-botDifferent resources.Oproof-assistant-botPrefix to filepath to avoid confusion between different interpreters.Pproof-assistant-bot#File extension used by interpreter.Qproof-assistant-botinput size in bytes.Tproof-assistant-bot!Telegram bot name. Used to parse /command@botname.Uproof-assistant-bot Bot token.Vproof-assistant-botoutput size in bytes.Wproof-assistant-bot Help message.Xproof-assistant-botHelp messages for sub-commands.Yproof-assistant-botVersion message.Zproof-assistant-bot"Settings for backend interpreters.[proof-assistant-botLoad settings from file.\proof-assistant-botLoad default settings.! "#(&%$')*+,-./0123498765:;=<>?@ABGFDECHIQPONMJKLRSZXWVUTY[\RSZXWVUTYHIQPONMJKLABGFDEC>?@:;=<349876512/0-.+,)*"#(&%$'! [\None ? proof-assistant-botCast something to .proof-assistant-botCast something to .proof-assistant-botWait N seconds.proof-assistant-botIf input starts with / drop the whole command with a space and return the remaining part.proof-assistant-bot*Drop not only command but sub-command too.proof-assistant-bot Cast UTF-8  to .proof-assistant-bot Cast UTF-8  to .proof-assistant-bot Cast UTF-8  to .proof-assistant-bot Cast UTF-8  to .proof-assistant-botCast some exception to .proof-assistant-botWrap IO action with  and return error message as .   None#$kproof-assistant-bot*Make ResourceLimits from soft/hard limits.proof-assistant-botRead Resources from ".proof-assistant-botRead limits from "! and set them for current thread.proof-assistant-botSet ) for current thread. None %proof-assistant-botMost interpreters work with files. Therefore, we need to store user input as a file. Remember that input could come from different chats, so we need to store input separately. Unless directory specified, temporary directory will be used to store the files.proof-assistant-botMake absolute filepath based on settings, request and directory.proof-assistant-bot%Helper to convert Telegram ChatId to  (for filepath).proof-assistant-bot'Helper to cut filepath from the output. None None  None None ?CNone eNoneNone NoneNone None #$8proof-assistant-bot#Supported sub-commands for Idris 2.proof-assistant-botMap of supported Idris 2 sub-commands. We use it instead of parser.proof-assistant-botCheck user input to identify .proof-assistant-bot!Choose an action based on either  or raw input.proof-assistant-bot$Helper to wrap given text as stdout.proof-assistant-botWrapper around temp directory that will try to identify whether associated file exists. And if file exists given action will be performed.proof-assistant-botWrapper around CLI execution.proof-assistant-botWe are trying to filter out some potentially dangerous operations such as :x.  None#$proof-assistant-botSimple state with settings and queue as communication model between bot and backend. proof-assistant-bot)Initialise a state based on its settings.None #$~proof-assistant-botCall Polilyngual API. Rzk will do all the job and return response or an error as result.None #$None #$proof-assistant-botCall Idris 2 as CLI application. It prepares the CLI command, executes it and waits for response.proof-assistant-bot.Parse command. It could be unknown command or  sub-command with its arguments or even expression to evaluate.None #$")proof-assistant-botCall Arend typechecker as CLI application. It prepares the CLI command, executes it and waits for response.proof-assistant-botArend requires a project for every file to typecheck. It reads project configuration, finds all files in a project directory and tries to typecheck all of them.Since we need to isolate different chats from each other we need to ensure that every chat has its own project. And every project has its own configuration.?As result, project directory will be created, set and returned.None#$$ proof-assistant-botAgda has its own env ( ) and state (). We are using them in combination with communication channel between Agda and bot.proof-assistant-bot Initiate  from >.proof-assistant-botHelper to get access to .proof-assistant-botHelper to store new .proof-assistant-botHelper to get access to .proof-assistant-botHelper to store new .proof-assistant-bot:Run chosen typechecking action in the typechecking monad ().proof-assistant-bot/Catch error from Agda and make it looks pretty.proof-assistant-botHelper to modify .  None 8?&proof-assistant-bot Supported sub-commands for Agda.proof-assistant-botMap of supported Agda sub-commands. We use it instead of parser.proof-assistant-botCheck user input to identify .proof-assistant-bot!Choose an action based on either  or raw input.proof-assistant-bot*Store raw user input in the file given by .None #$)+proof-assistant-botCall Agda with its state. It will parse and execute command from the .proof-assistant-botSince every chat associated with its own Agda state, we need to modify TCEnv by setting 1 with an absolute path to the corresponding file.proof-assistant-bot0Parse user input as command and execute in Agda.proof-assistant-bot.Parse command. It could be unknown command or  sub-command with its arguments or even expression to evaluate.None #$+ proof-assistant-botBot has its own state.proof-assistant-bot1Queue to read messages from backend interpreters.proof-assistant-bot Bot settings.proof-assistant-bot#All interpreters with their states.proof-assistant-bot2Combination of all supported backend interpreters.proof-assistant-bot(Initiate new interpreters from settings.proof-assistant-bot Initiate  from R.proof-assistant-bot Read message from "input" queue.proof-assistant-bot!Read message from "output" queue.proof-assistant-botWrite message to "input" queue.proof-assistant-bot Write message to "output" queue.None #$%>?.cproof-assistant-botWorker abstraction over Proof assistant as Interpreter. Could be CLI, Haskell function, network, whatever. It should have the state and associated settings with the state.proof-assistant-botMain worker function. Reads input from Telegram, calls CLI or API, could be anything. Returns , wraps it in   and sends back to Telegram.proof-assistant-bot1Call some external CLI application, probably Coq. Safe-Inferred /Eproof-assistant-botVersion of Rzk.proof-assistant-botVersion of this package.proof-assistant-bot.Helper to build version from template message. None #$2proof-assistant-botSupported backends.proof-assistant-botSupported actions by bot.proof-assistant-bot$Call backend and send request to it.proof-assistant-botSend response back as reply.proof-assistant-botReply with help message.proof-assistant-botReply with version message.proof-assistant-botWrite in STDOUT unknown input.proof-assistant-botTelegram Model.proof-assistant-botInitiate bot app based on a .proof-assistant-bot$How to handle updates from Telegram.proof-assistant-bot,How to handle actions after parsing updates.proof-assistant-botHelper that will try to deliver message even when Telegram failed to send it.proof-assistant-botInitiate Telegram Env, ), start Bot, start backends concurrently.proof-assistant-botMain function."#$%&'())*+,-../01234566789:;<==>?@@ABCDEFFGGHHIIJJKKLMNOPQQRSTTUVVWXYZ[\\]^_`abcdeefghijklmnopqrstuvwxyz{|}~                               !!!!!!!!!proof-assistant-bot-0.2.0-inplace(Agda.Interaction.Command.Internal.Parser)Agda.Interaction.Command.RetryConstraints(Agda.Interaction.Command.ShowConstraints$Agda.Interaction.Command.ShowContextProof.Assistant.RequestProof.Assistant.ResponseProof.Assistant.SettingsProof.Assistant.HelpersProof.Assistant.ResourceLimitProof.Assistant.RefreshFileAgda.Interaction.Command.TypeOfAgda.Interaction.Command.TypeIn"Agda.Interaction.Command.ShowScope"Agda.Interaction.Command.ShowMetasAgda.Interaction.Command.Reload#Agda.Interaction.Command.RefineMeta!Agda.Interaction.Command.GiveMeta!Agda.Interaction.Command.EvalTermAgda.Interaction.Command.EvalInIdris.Interaction.CommandProof.Assistant.StateProof.Assistant.RzkProof.Assistant.LeanProof.Assistant.IdrisProof.Assistant.ArendAgda.Interaction.StateAgda.Interaction.CommandProof.Assistant.AgdaProof.Assistant.TransportProof.Assistant.InterpreterProof.Assistant.VersionProof.Assistant.BotPaths_proof_assistant_bot metaParseExpr actOnMeta parseExprreadMretryConstraintsshowConstraints showContextInterpreterRequest interpreterRequestTelegramChatId#interpreterRequestTelegramMessageIdinterpreterRequestMessageupdateToRequestInterpreterResponse!interpreterResponseTelegramChatId$interpreterResponseTelegramMessageIdinterpreterResponseResponsetoSendMessageRequestmakeTelegramResponseToInterpreterState getQueueSizeInterpretersSettings$sel:agda:InterpretersSettings$sel:arend:InterpretersSettings$sel:idris:InterpretersSettings$sel:coq:InterpretersSettings$sel:lean:InterpretersSettings$sel:rzk:InterpretersSettingsLimit$sel:soft:Limit$sel:hard:LimitResourceSettings!$sel:totalMemory:ResourceSettings$sel:dataSize:ResourceSettings$sel:openFiles:ResourceSettings$sel:fileSize:ResourceSettings$sel:cpuTime:ResourceSettingsPriorityTime ExecutableCmdArgs IdrisSettings ArendSettings&$sel:arendRootProjectDir:ArendSettings$$sel:arendYamlFilename:ArendSettings#$sel:arendYamlContent:ArendSettings"$sel:arendModuleName:ArendSettings $sel:externalArend:ArendSettings LeanSettings$sel:projectDir:LeanSettings$sel:externalLean:LeanSettings AgdaSettings$sel:internal:AgdaSettingsInternalInterpreterSettings($sel:timeout:InternalInterpreterSettings,$sel:allocations:InternalInterpreterSettings*$sel:inputSize:InternalInterpreterSettings1$sel:sourceFilePrefix:InternalInterpreterSettings4$sel:sourceFileExtension:InternalInterpreterSettingsExternalInterpreterSettings%$sel:args:ExternalInterpreterSettings+$sel:executable:ExternalInterpreterSettings%$sel:time:ExternalInterpreterSettings)$sel:priority:ExternalInterpreterSettings*$sel:resources:ExternalInterpreterSettings/$sel:tempFilePrefix:ExternalInterpreterSettings.$sel:fileExtension:ExternalInterpreterSettings*$sel:inputSize:ExternalInterpreterSettingsSettings$sel:botName:Settings$sel:botToken:Settings$sel:outputSize:Settings$sel:help:Settings$sel:helpMessages:Settings$sel:version:Settings"$sel:interpretersSettings:Settings loadSettingsloadDefaultSettings!$fToInterpreterStateArendSettings $fToInterpreterStateLeanSettings $fToInterpreterStateAgdaSettings/$fToInterpreterStateExternalInterpreterSettings/$fToInterpreterStateInternalInterpreterSettings$fGenericSettings$fFromDhallSettings$fGenericInterpretersSettings$fFromDhallInterpretersSettings$fFromDhallIdrisSettings!$fToInterpreterStateIdrisSettings$fGenericIdrisSettings$fGenericLeanSettings$fFromDhallLeanSettings$fGenericArendSettings$fFromDhallArendSettings$$fGenericExternalInterpreterSettings&$fFromDhallExternalInterpreterSettings$fGenericResourceSettings$fFromDhallResourceSettings$fGenericLimit$fFromDhallLimit$fGenericPriority$fFromDhallPriority $fGenericTime$fFromDhallTime$fGenericExecutable$fFromDhallExecutable$fGenericCmdArgs$fFromDhallCmdArgs$fGenericAgdaSettings$fFromDhallAgdaSettings$$fGenericInternalInterpreterSettings&$fFromDhallInternalInterpreterSettingstoIntt2s asyncWait dropCommanddropSubCommandtoBSfromBSbsToTexttextToBS processErrorhandleErrorMaybemakeResourceLimits makeLimits setLimits setPriorityrefreshTmpFilegetTempFilePathchatIdToStringvalidatetypeOftypeIn showScope showMetasreload checkFile refineMetagiveMetaevalTermevalIn IdrisCommandLoadTypeOfHelpsupportedCommandsmatchSupported chooseCommand textResponse withResource runProcess validateCmd$fEqIdrisCommand$fShowIdrisCommand$fGenericIdrisCommandInterpreterStatesettingsinputnewInterpreterStatecallRzkcallLean callIdris2 parseRequest callArendsetArendProject AgdaStateinterpreterState agdaEnvRef agdaStateRef newAgdaState readTCState writeTCState readTCEnv writeTCEnvrunAgdacatchAgdaErrorsetEnv AgdaCommandReload ConstraintsContextGiveRefineMetaEvalTypeInWakeUpScopestoreRequestContent$fEqAgdaCommand$fShowAgdaCommand$fGenericAgdaCommandcallAgdawithChat interpretAgdaBotStateoutput botSettings interpreters InternalState ExternalState InterpretersagdaarendidriscoqleanrzknewInterpreters newBotState readInput readOutput writeInput writeOutput Interpreter interpretSafe getSettingsrunInterpretercallExternalInterpreter*$fInterpreterInterpreterStateArendSettings)$fInterpreterInterpreterStateLeanSettings*$fInterpreterInterpreterStateIdrisSettings8$fInterpreterInterpreterStateExternalInterpreterSettings"$fInterpreterAgdaStateAgdaSettings8$fInterpreterInterpreterStateInternalInterpreterSettings rzkVersionproofAssistantBotVersion makeVersionBackendAgdaArendIdrisCoqLeanRzkActionCallSendBackVersionDebugModelproofAssistantBotupdateToAction handleActionsendResponseBackrunTelegramBotrunversiongetDataFileName getBinDir getLibDir getDynLibDir getDataDir getLibexecDir getSysconfDirtlgrm-bt-smpl-0.6-c77a7ba0Telegram.Bot.API.MethodsSendMessageRequestghc-prim GHC.TypesTrueIntbaseGHC.BaseStringbytestring-0.10.12.0Data.ByteString.Internal ByteString text-1.2.4.1Data.Text.InternalTextAgd-2.6.2.2-5a936f9dAgda.TypeChecking.Monad.BaseTCEnvTCStateTCMenvCurrentPath