proof-assistant-bot 0.2.0 → 0.2.1

raw patch · 8 files changed

+38/−15 lines, 8 filesdep ~Agdadep ~telegram-bot-simple

Dependency ranges changed: Agda, telegram-bot-simple

Files

• CHANGELOG.md +4/−0
• proof-assistant-bot.cabal +3/−3
• src/Agda/Interaction/Command/Internal/Parser.hs +9/−6
• src/Agda/Interaction/Command/ShowContext.hs +2/−2
• src/Proof/Assistant/Agda.hs +3/−2
• src/Proof/Assistant/Lean.hs +15/−2
• src/Proof/Assistant/Response.hs +1/−0
• src/Proof/Assistant/Settings.hs +1/−0

@@ -1,5 +1,9 @@ # Revision history for proof-assistant-bot +## 0.2.1 -- 2023-02-07++- Agda bumped to 2.6.3, telegram-bot-simple bumped to 0.9 (see [#29](https://github.com/swamp-agr/proof-assistant-bot/pull/29)).+ ## 0.2.0 -- 2022-12-10   - Import Agda primitives for every `/(re)load` (see [#21](https://github.com/swamp-agr/proof-assistant-bot/pull/21));

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               proof-assistant-bot-version:            0.2.0+version:            0.2.1 synopsis:           Telegram bot for proof assistants description:        Bridge between Telegram Bot and several proof assistants.                     .@@ -32,12 +32,12 @@                     , process                     , rzk                     , stm-                    , telegram-bot-simple >= 0.5.2+                    , telegram-bot-simple >= 0.9                     , text                     , unix                     , unordered-containers                     -- interpreters-                    , Agda+                    , Agda >= 2.6.3     exposed-modules:  Proof.Assistant.Agda                     , Proof.Assistant.Arend                     , Proof.Assistant.Idris

@@ -4,9 +4,10 @@ import Agda.Syntax.Common (InteractionId (..)) import Agda.Syntax.Parser (exprParser, parse, parsePosString) import Agda.Syntax.Position (getRange, noRange, rStart)-import Agda.Syntax.Translation.ConcreteToAbstract (concreteToAbstract, localToAbstract)+import Agda.Syntax.Translation.ConcreteToAbstract+  (checkCohesionAttributes, concreteToAbstract, localToAbstract) import Agda.TypeChecking.Monad.Base-import Agda.TypeChecking.Monad.MetaVars (lookupInteractionId, lookupMeta, withInteractionId)+import Agda.TypeChecking.Monad.MetaVars (lookupInteractionId, lookupLocalMeta, withInteractionId) import Agda.TypeChecking.Warnings (runPM) import Agda.Utils.Impossible (__IMPOSSIBLE__) import Agda.Utils.Pretty (text)@@ -20,11 +21,12 @@ metaParseExpr ::  InteractionId -> ByteString -> TCM Expr metaParseExpr ii s =     do  m <- lookupInteractionId ii-        scope <- getMetaScope <$> lookupMeta m-        r <- getRange <$> lookupMeta m+        scope <- getMetaScope <$> lookupLocalMeta m+        r <- getRange <$> lookupLocalMeta m         -- liftIO $ putStrLn $ prettyShow scope         let pos = fromMaybe (__IMPOSSIBLE__) (rStart r)-        e <- runPM $ parsePosString exprParser pos (BS8.unpack s)+        (e, coh) <- runPM $ parsePosString exprParser pos (BS8.unpack s)+        checkCohesionAttributes coh         concreteToAbstract scope e  actOnMeta :: [ByteString] -> (InteractionId -> Expr -> TCM a) -> TCM a@@ -37,7 +39,8 @@  parseExpr :: String -> TCM Expr parseExpr s = do-    e <- runPM $ parse exprParser s+    (e, coh) <- runPM $ parse exprParser s+    checkCohesionAttributes coh     localToAbstract e return  readM :: Read a => String -> TCM a

@@ -6,7 +6,7 @@ import Agda.Syntax.Common (InteractionId (..), argNameToString) import Agda.TypeChecking.Monad.Base (TCM, getMetaInfo) import Agda.TypeChecking.Monad.Context (getContextTelescope)-import Agda.TypeChecking.Monad.MetaVars (lookupInteractionId, lookupMeta, withMetaInfo)+import Agda.TypeChecking.Monad.MetaVars (lookupInteractionId, lookupLocalMeta, withMetaInfo) import Agda.TypeChecking.Pretty (prettyTCM) import Agda.TypeChecking.Reduce (normalise) import Agda.TypeChecking.Substitute.Class (raise)@@ -21,7 +21,7 @@ showContext :: [ByteString] -> TCM ByteString showContext (meta:args) = do     i <- InteractionId <$> readM (BS8.unpack meta)-    mi <- lookupMeta =<< lookupInteractionId i+    mi <- lookupLocalMeta =<< lookupInteractionId i     BS8.unlines <$> withMetaInfo (getMetaInfo mi) displayMore   where     display (x, t) n = do

@@ -19,6 +19,7 @@ import Agda.TypeChecking.Monad.Base (envCurrentPath) import Agda.Utils.FileName (absolute) import Proof.Assistant.Helpers+import Proof.Assistant.RefreshFile (validate) import Proof.Assistant.Request import Proof.Assistant.Settings import Proof.Assistant.State@@ -42,7 +43,7 @@  -- | Since every chat associated with its own Agda state, we need to modify 'TCEnv' -- by setting 'envCurrentPath' with an absolute path to the corresponding file.-withChat :: ChatId -> AgdaState -> IO a -> IO a+withChat :: ChatId -> AgdaState -> IO ByteString -> IO ByteString withChat chatId state action = do   tmpDir <- getTemporaryDirectory   let InternalInterpreterSettings{..} = (internal . settings . interpreterState) state@@ -54,7 +55,7 @@   absSourceFile <- absolute sourceFile   let modifiedEnv s = s { envCurrentPath = Just absSourceFile }   setEnv state modifiedEnv-  action+  pure . validate sourceFile =<< action  -- | Parse user input as command and execute in Agda. interpretAgda :: AgdaState -> ByteString -> IO ByteString

@@ -5,6 +5,7 @@ import Control.Concurrent.Async (race) import Data.ByteString (ByteString) import Data.Coerce (coerce)+import Data.Foldable (foldl') import Data.Text (unpack) import System.Directory (withCurrentDirectory) import System.Process (readProcessWithExitCode)@@ -16,11 +17,13 @@ import Proof.Assistant.Settings import Proof.Assistant.State +import qualified Data.Text as Text+ callLean :: InterpreterState LeanSettings -> InterpreterRequest -> IO ByteString callLean InterpreterState{..} ir = do-  let LeanSettings{..} = coerce settings+  let ls@LeanSettings{..} = coerce settings       s@ExternalInterpreterSettings{..} = externalLean-  (dir, path) <- refreshTmpFile s ir (Just projectDir)+  (dir, path) <- refreshTmpFile s (validateLean ls ir) (Just projectDir)   withCurrentDirectory dir $ do     let fullArgs = (unpack <$> coerce args) <> [path]         runProcess = readProcessWithExitCode (t2s executable) fullArgs ""@@ -33,3 +36,13 @@     case eresult of       Left ()  -> pure "Time limit exceeded"       Right bs -> pure bs++validateLean :: LeanSettings -> InterpreterRequest -> InterpreterRequest+validateLean LeanSettings{..} ir@InterpreterRequest{..}+  = ir { interpreterRequestMessage = validatedMsg }+  where+    remove txt blockedPrefix = Text.replace blockedPrefix "" txt+    removeAllFromLine x = foldl' remove x leanBlockList+    removeUnsafeImports = textToBS . removeAllFromLine . bsToText++    validatedMsg = removeUnsafeImports interpreterRequestMessage

@@ -24,6 +24,7 @@ toSendMessageRequest :: Bool -> InterpreterResponse -> SendMessageRequest toSendMessageRequest isMonospace InterpreterResponse{..} = SendMessageRequest   { sendMessageChatId                   = SomeChatId interpreterResponseTelegramChatId+  , sendMessageMessageThreadId          = Nothing   , sendMessageText       = if isMonospace         then "```\n" <> decodeUtf8 interpreterResponseResponse <> "\n```\n"

@@ -44,6 +44,7 @@  data LeanSettings = LeanSettings   { projectDir :: !FilePath -- ^ Lean requires project where to store source files for typechecking.+  , leanBlockList :: [Text]   , externalLean   :: !ExternalInterpreterSettings   } deriving (Generic, FromDhall)