Proof.Assistant.RefreshFile

Documentation

refreshTmpFile :: ExternalInterpreterSettings -> InterpreterRequest -> Maybe FilePath -> IO (FilePath, FilePath)

Most 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.

getTempFilePath :: ExternalInterpreterSettings -> InterpreterRequest -> FilePath -> FilePath

Make absolute filepath based on settings, request and directory.

chatIdToString :: ChatId -> String

Helper to convert Telegram ChatId to String (for filepath).

validate :: FilePath -> ByteString -> ByteString

Helper to cut filepath from the output.