packages feed

proof-assistant-bot 0.2.1 → 0.2.2

raw patch · 29 files changed

+489/−106 lines, 29 filesdep +telegram-bot-apidep ~Agdadep ~basedep ~mtl

Dependencies added: telegram-bot-api

Dependency ranges changed: Agda, base, mtl, telegram-bot-simple

Files

CHANGELOG.md view
@@ -1,5 +1,15 @@ # Revision history for proof-assistant-bot +## 0.2.2 -- 2024-02-07++- Support GHC 9.4 (see [#43](https://github.com/swamp-agr/proof-assistant-bot/pull/43)).+- Also various dependencies versions bumps:+  - base-4.17+  - Agda-2.6.4+  - mtl-2.3.1+  - rzk-0.7+  - telegram-bot-simple-0.13+ ## 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)).
README.md view
@@ -8,6 +8,7 @@     4. [Lean](#lean)     5. [Arend](#arend)     6. [Rzk](#rzk)+    7. [Alloy](#alloy) 3. [Usage](#usage) 4. [Available instances](#available-instances) 5. [Acknowledgements](#acknowledgements)@@ -41,6 +42,12 @@ export PROOF_ASSISTANT_BOT_TOKEN="..." ``` +3. Another environmental variable that unfortunately needed is `NIX_PROFILE`. Please add it as ++```+export NIX_PROFILE="$HOME/.nix-profile"+```+ ### Coq  1. Install `opam >= 2.1.0`, e.g. [from here](https://ocaml.org/docs/up-and-running#installation-for-unix).@@ -165,6 +172,48 @@  No actions required. See `cabal.project` for more details. +### Alloy 6 / Alloy CLI Wrapper++You can read about CLI Wrapper here: https://github.com/AlloyTools/org.alloytools.alloy/issues/211++1. Get `nix` from [nixos.org](https://nixos.org/download.html#download-nix).++2. Get `java` and `openjdk17` via `nix`:++```bash+nix-env -i openjdk-17.0.4+8+```++3. Set `JAVA_HOME` environment variable to your openjdk location. You can use `readlink $HOME/.nix-profile/bin/java` and strip `/bin/java` from the end.++4. Get `alloy6` via `nix`:++```bash+nix-env -i alloy6+```++5. Create project directory to store Alloy projects (for different telegram chats) and set `ALLOY_PROJECT_DIR`.++6. Create directory for Alloy CLI wrapper and prepare Alloy CLI Wrapper:++```bash+mkdir -p $ALLOY_PROJECT_DIR/bin+cd $ALLOY_PROJECT_DIR+# Download Alloy CLI Wrapper+curl https://gist.githubusercontent.com/swamp-agr/560f0d9bf8dc034f99d6055a5a197285/raw/5b547616063ba834bfa2987bc1eb539f1ec8088d/Main.java > bin/Main.java+javac -cp "$NIX_PROFILE/share/alloy/*" -Xlint:all bin/Main.java+# Test: should be empty output and exit code 0+java -cp $NIX_PROFILE/share/alloy/alloy6.jar:$ALLOY_PROJECT_DIR/bin Main+```++7. Set up `graphviz` and `imagemagick` for generating plots based on Alloy CLI Wrapper output:++```bash+nix-env -i graphviz imagemagick+```++8. Set `ALLOY_PATH` environment variable to `$NIX_PROFILE/share/alloy/alloy6.jar`.+ ## Usage  - Coq supports only typecheck of the user input via `/coq` command. Example:@@ -361,6 +410,114 @@       := \I -> \J -> \psi -> \zeta -> \X -> \chi -> \phi -> \f ->         \k -> \(t, s) -> k t s     ```++- Alloy is available via `/alloy` command.++    - Example:++    ```alloy+    /alloy open util/ordering[Id]++    sig Node {+     id : one Id,+     succ : one Node,+     var inbox : set Id,+     var outbox : set Id+    } +    +    sig Id {}+    +    fact ring {+     all i : Id | lone id.i+     all n : Node | Node in n.^succ+    }+    +    var sig elected in Node {}+    +    fact elected {+     always {+      elected = {n : Node | once (n.id in n.inbox)}+     }+    }+    +    enum Event { Send, Compute }+    +    pred send [n : Node] {+     some i : n.outbox {+      n.outbox' = n.outbox - i+      n.succ.inbox' = n.succ.inbox + i+     }+     all m : Node - n.succ | m.inbox' = m.inbox+     all m : Node - n | m.outbox' = m.outbox+    }+    +    fun send : Event -> Node {+     Send -> { n : Node | send[n] }+    }+    +    pred compute [n : Node] {+     some i : n.inbox {+      n.inbox' = n.inbox - i+      n.outbox' = n.outbox + (i - n.id.*(~next))+     }+     all m : Node - n | m.inbox' = m.inbox+     all m : Node - n | m.outbox' = m.outbox+    }+    +    fun compute : Event -> Node {+     Compute -> { n : Node | compute[n] }+    }+    +    fun events : set Event {+     (send+compute).Node+    }+    +    pred skip {+     inbox' = inbox+     outbox' = outbox+    }+    +    fact init {+     no inbox+     outbox = id+    }+    +    fact behaviour {+     always (skip or some n : Node | send[n] or compute[n])+    }+    +    +    run {} for 4 but exactly 4 Node, 10 steps+    run example {eventually some elected} for 3 but exactly 3 Node, 6 steps+    +    assert safety {+     always lone elected+    }+    check safety for 3 but 15 steps+    +    +    pred sendEnabled [n : Node] {+     some n.outbox+    }+    +    pred computeEnabled [n : Node] {+     some n.inbox+    }+    +    pred fairness {+     always (all n : Node | (always sendEnabled[n] implies eventually send[n]))+     always (all n : Node | (always computeEnabled[n] implies eventually compute[n]))+    }+    +    assert liveness {+     fairness and some Node implies eventually some elected+    }+    check liveness for 3+    ```++    - As result you can see:+    +    ![Alloy temporal model instance with two different states](https://raw.githubusercontent.com/swamp-agr/proof-assistant-bot/master/resources/alloy-repsonse.gif)  ## Available instances
proof-assistant-bot.cabal view
@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               proof-assistant-bot-version:            0.2.1+version:            0.2.2 synopsis:           Telegram bot for proof assistants description:        Bridge between Telegram Bot and several proof assistants.                     .@@ -22,23 +22,25 @@     hs-source-dirs:   src     ghc-options:      -Wall     default-language: Haskell2010-    build-depends:    base < 4.17+    build-depends:    base < 4.18                     , async                     , bytestring                     , dhall                     , directory                     , filepath-                    , mtl+                    , mtl >= 2.3.1                     , process                     , rzk                     , stm-                    , telegram-bot-simple >= 0.9+                    , telegram-bot-api+                    , telegram-bot-simple == 0.13                     , text                     , unix                     , unordered-containers                     -- interpreters-                    , Agda >= 2.6.3+                    , Agda >= 2.6.4     exposed-modules:  Proof.Assistant.Agda+                    , Proof.Assistant.Alloy                     , Proof.Assistant.Arend                     , Proof.Assistant.Idris                     , Proof.Assistant.Lean@@ -86,7 +88,7 @@      -- LANGUAGE extensions used by modules in this package.     -- other-extensions:-    build-depends:    base ^>=4.14.3.0+    build-depends:    base < 4.18                     , proof-assistant-bot     hs-source-dirs:   app     ghc-options:      -Wall -O2 -threaded -rtsopts -with-rtsopts=-N
src/Agda/Interaction/Command/EvalIn.hs view
@@ -4,8 +4,8 @@ import Agda.Interaction.Base (ComputeMode (..)) import Agda.Interaction.BasicOps (evalInCurrent) import Agda.Syntax.Abstract.Pretty (prettyA)+import Agda.Syntax.Common.Pretty (prettyShow) import Agda.TypeChecking.Monad.Base (TCM)-import Agda.Utils.Pretty (prettyShow) import Data.ByteString (ByteString)  import Agda.Interaction.Command.Internal.Parser
src/Agda/Interaction/Command/EvalTerm.hs view
@@ -4,9 +4,9 @@  import Agda.Interaction.Base (ComputeMode (..)) import Agda.Interaction.BasicOps hiding (parseExpr)+import Agda.Syntax.Common.Pretty (prettyShow) import Agda.TypeChecking.Monad.Base (TCM) import Agda.TypeChecking.Pretty (prettyTCM)-import Agda.Utils.Pretty (prettyShow) import Proof.Assistant.Helpers (toBS)  import Data.ByteString (ByteString)
src/Agda/Interaction/Command/GiveMeta.hs view
@@ -1,9 +1,9 @@ {-# LANGUAGE OverloadedStrings #-} module Agda.Interaction.Command.GiveMeta where +import Agda.Syntax.Common.Pretty (prettyShow) import Agda.TypeChecking.Monad.Base (TCM) import Agda.TypeChecking.Pretty (prettyTCM)-import Agda.Utils.Pretty (prettyShow) import Data.ByteString (ByteString)  import Agda.Interaction.Base (UseForce (..))
src/Agda/Interaction/Command/Internal/Parser.hs view
@@ -2,15 +2,15 @@  import Agda.Syntax.Abstract (Expr) import Agda.Syntax.Common (InteractionId (..))+import Agda.Syntax.Common.Pretty (text) import Agda.Syntax.Parser (exprParser, parse, parsePosString) import Agda.Syntax.Position (getRange, noRange, rStart) import Agda.Syntax.Translation.ConcreteToAbstract-  (checkCohesionAttributes, concreteToAbstract, localToAbstract)+  (checkAttributes, concreteToAbstract, localToAbstract) import Agda.TypeChecking.Monad.Base import Agda.TypeChecking.Monad.MetaVars (lookupInteractionId, lookupLocalMeta, withInteractionId) import Agda.TypeChecking.Warnings (runPM) import Agda.Utils.Impossible (__IMPOSSIBLE__)-import Agda.Utils.Pretty (text) import Control.Monad.Except (MonadError(..)) import Data.ByteString (ByteString) import Data.Maybe (fromMaybe)@@ -26,7 +26,7 @@         -- liftIO $ putStrLn $ prettyShow scope         let pos = fromMaybe (__IMPOSSIBLE__) (rStart r)         (e, coh) <- runPM $ parsePosString exprParser pos (BS8.unpack s)-        checkCohesionAttributes coh+        checkAttributes coh         concreteToAbstract scope e  actOnMeta :: [ByteString] -> (InteractionId -> Expr -> TCM a) -> TCM a@@ -40,7 +40,7 @@ parseExpr :: String -> TCM Expr parseExpr s = do     (e, coh) <- runPM $ parse exprParser s-    checkCohesionAttributes coh+    checkAttributes coh     localToAbstract e return  readM :: Read a => String -> TCM a
src/Agda/Interaction/Command/RefineMeta.hs view
@@ -1,8 +1,8 @@ module Agda.Interaction.Command.RefineMeta where +import Agda.Syntax.Common.Pretty (prettyShow) import Agda.TypeChecking.Monad.Base (TCM) import Agda.TypeChecking.Pretty (prettyTCM)-import Agda.Utils.Pretty (prettyShow) import Data.ByteString (ByteString)  import Agda.Interaction.Base (UseForce (..))
src/Agda/Interaction/Command/Reload.hs view
@@ -8,13 +8,14 @@ import Agda.Interaction.FindFile (SourceFile (..)) import Agda.Interaction.Options (optOnlyScopeChecking) import Agda.Syntax.Translation.ConcreteToAbstract (importPrimitives)-import Agda.TypeChecking.Errors (applyFlagsToTCWarnings, prettyError)+import Agda.TypeChecking.Errors (applyFlagsToTCWarnings, renderError) import Agda.TypeChecking.Monad.Base   (ModuleCheckMode (..), TypeError (..), TCM, commandLineOptions, iInsideScope, typeError) import Agda.TypeChecking.Monad.State (setScope) import Agda.Utils.FileName (AbsolutePath) import Agda.Utils.Null (unlessNullM)-import Control.Monad.Except (MonadError(..), unless)+import Control.Monad (unless)+import Control.Monad.Except (MonadError(..)) import Data.ByteString (ByteString)  import Proof.Assistant.Helpers (toBS)@@ -27,7 +28,7 @@   _ <- importPrimitives   pure "Type checked succesfully."   `catchError` \e -> do-    s <- prettyError e+    s <- renderError e     pure $ "Failed. " <> toBS s  checkFile :: AbsolutePath -> TCM CheckResult
src/Agda/Interaction/Command/ShowConstraints.hs view
@@ -3,8 +3,8 @@ module Agda.Interaction.Command.ShowConstraints where  import Agda.Interaction.BasicOps (getConstraints)+import Agda.Syntax.Common.Pretty (prettyShow) import Agda.TypeChecking.Monad.Base (TCM)-import Agda.Utils.Pretty (prettyShow) import Data.ByteString (ByteString)  import qualified Data.ByteString.Char8 as BS8
src/Agda/Interaction/Command/ShowContext.hs view
@@ -4,14 +4,14 @@  import Agda.Interaction.Command.Internal.Parser import Agda.Syntax.Common (InteractionId (..), argNameToString)+import Agda.Syntax.Common.Pretty ((<+>), render, text) import Agda.TypeChecking.Monad.Base (TCM, getMetaInfo) import Agda.TypeChecking.Monad.Context (getContextTelescope) import Agda.TypeChecking.Monad.MetaVars (lookupInteractionId, lookupLocalMeta, withMetaInfo) import Agda.TypeChecking.Pretty (prettyTCM) import Agda.TypeChecking.Reduce (normalise) import Agda.TypeChecking.Substitute.Class (raise)-import Agda.Utils.Pretty ((<+>), render, text)-import Control.Monad.Except (zipWithM)+import Control.Monad (zipWithM) import Data.ByteString (ByteString)  import qualified Agda.Syntax.Internal as I
src/Agda/Interaction/Command/ShowMetas.hs view
@@ -7,12 +7,12 @@   (outputFormId, typeOfMeta, typesOfHiddenMetas, typesOfVisibleMetas) import Agda.Syntax.Abstract.Pretty (prettyA) import Agda.Syntax.Common (InteractionId (..))+import Agda.Syntax.Common.Pretty (prettyShow, render) import Agda.Syntax.Position (noRange) import Agda.TypeChecking.Monad.Base (TCM, nmid) import Agda.TypeChecking.Monad.MetaVars   (getInteractionRange, getMetaRange, withInteractionId, withMetaId) import Agda.Utils.Impossible (__IMPOSSIBLE__)-import Agda.Utils.Pretty (prettyShow, render) import Data.ByteString (ByteString)  import Agda.Interaction.Command.Internal.Parser
src/Agda/Interaction/Command/ShowScope.hs view
@@ -1,8 +1,8 @@ module Agda.Interaction.Command.ShowScope where +import Agda.Syntax.Common.Pretty (prettyShow) import Agda.TypeChecking.Monad.Base (TCM) import Agda.TypeChecking.Monad.State (getScope)-import Agda.Utils.Pretty (prettyShow) import Data.ByteString (ByteString)  import Proof.Assistant.Helpers (toBS)
src/Agda/Interaction/Command/TypeIn.hs view
@@ -3,9 +3,9 @@  import Agda.Interaction.Base (Rewrite (..)) import Agda.Interaction.BasicOps (typeInMeta)+import Agda.Syntax.Common.Pretty (prettyShow) import Agda.TypeChecking.Monad.Base (TCM) import Agda.TypeChecking.Pretty (prettyTCM)-import Agda.Utils.Pretty (prettyShow) import Data.ByteString (ByteString)  import Agda.Interaction.Command.Internal.Parser
src/Agda/Interaction/Command/TypeOf.hs view
@@ -2,9 +2,9 @@  import Agda.Interaction.Base (Rewrite (..)) import Agda.Interaction.BasicOps (typeInCurrent)+import Agda.Syntax.Common.Pretty (prettyShow) import Agda.TypeChecking.Monad.Base (TCM) import Agda.TypeChecking.Pretty (prettyTCM)-import Agda.Utils.Pretty (prettyShow) import Data.ByteString (ByteString)  import Agda.Interaction.Command.Internal.Parser
src/Agda/Interaction/State.hs view
@@ -4,7 +4,7 @@  import Agda.Interaction.Options import Agda.Syntax.Translation.ConcreteToAbstract (importPrimitives)-import Agda.TypeChecking.Errors (prettyError)+import Agda.TypeChecking.Errors (renderError) import Agda.TypeChecking.Monad.Base import Agda.TypeChecking.Monad.Options (setCommandLineOptions) import Control.Monad.Except (MonadError(..))@@ -67,7 +67,7 @@ -- | Catch error from Agda and make it looks pretty. catchAgdaError :: MonadTCM m => TCErr -> m ByteString catchAgdaError e = do-  s <- prettyError e+  s <- renderError e   return $ toBS s  -- | Helper to modify 'TCEnv'.
src/Proof/Assistant/Agda.hs view
@@ -21,13 +21,14 @@ import Proof.Assistant.Helpers import Proof.Assistant.RefreshFile (validate) import Proof.Assistant.Request+import Proof.Assistant.Response import Proof.Assistant.Settings import Proof.Assistant.State  import qualified Data.ByteString.Char8 as BS8  -- | Call Agda with its state. It will parse and execute command from the 'InterpreterRequest'.-callAgda :: AgdaState -> InterpreterRequest -> IO ByteString+callAgda :: AgdaState -> InterpreterRequest -> IO BotResponse callAgda currentAgdaState@AgdaState{..} InterpreterRequest{..} = do   let InternalInterpreterSettings{..} = internal (settings interpreterState)       asyncApi = withChat interpreterRequestTelegramChatId currentAgdaState $ do@@ -38,8 +39,8 @@       asyncTimer = asyncWait (coerce timeout)   eresult <- race asyncTimer (handleErrorMaybe asyncApi)   case eresult of-    Left () -> pure "Time limit exceeded"-    Right result -> pure result+    Left () -> pure (TextResponse "Time limit exceeded")+    Right result -> pure (TextResponse result)  -- | 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.
+ src/Proof/Assistant/Alloy.hs view
@@ -0,0 +1,122 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-}+module Proof.Assistant.Alloy where++import Control.Concurrent.Async (race)+import Control.Monad (forM)+import Data.Coerce (coerce)+import Data.Maybe (mapMaybe)+import Data.Text (unpack, pack)+import System.Directory+  (createDirectoryIfMissing, listDirectory, removeFile, withCurrentDirectory)+import System.Exit (ExitCode)+import System.FilePath+import System.Process (readProcessWithExitCode)+import Text.Read (readMaybe)++import Proof.Assistant.Helpers+import Proof.Assistant.RefreshFile+import Proof.Assistant.Request+import Proof.Assistant.Response+import Proof.Assistant.ResourceLimit+import Proof.Assistant.Settings+import Proof.Assistant.State++callAlloy :: InterpreterState AlloySettings -> InterpreterRequest -> IO BotResponse+callAlloy InterpreterState{..} ir = do+  let AlloySettings{..} = coerce settings+      s@ExternalInterpreterSettings{..} = externalAlloy+      projectDir = alloyProjectDir+        </> (tempFilePrefix  <> chatIdToString (interpreterRequestTelegramChatId ir))+  createDirectoryIfMissing True projectDir+  (dir, path) <- refreshTmpFile s ir (Just projectDir)+  withCurrentDirectory dir $ do+    let run+          :: Executable -> CmdArgs -> FilePath -> Maybe [FilePath]+          -> IO (ExitCode, String, String)+        run exe arguments path' mPath = do+          readProcessWithExitCode (t2s exe) fullArgs ""+          where+            addPathAsArg "" = id+            addPathAsArg p = (<> [p])++            applyOutMaybe = case mPath of+              Nothing -> id+              Just extra -> (<> extra)+            fullArgs = applyOutMaybe $ addPathAsArg path' (unpack <$> coerce arguments)+        runProcess = run executable args path Nothing+        asyncExecutable = do+          setPriority priority+          (_exitCode, stdout, stderr) <- runProcess+          pure . validate path . toBS . unlines $ [stdout, stderr]+        asyncTimer = asyncWait time++        mkImagePath external file =+          let changeAbsolute = if external+                then (alloySharedDir </>) . takeFileName else id+          in changeAbsolute ((dropExtension file) <.> "png")+        mkGifPath file = (alloySharedDir </>) . takeFileName $ (dropExtension file) <.> "gif"++    eresult <- race asyncTimer (handleErrorMaybe asyncExecutable)+    result <- case eresult of+      Left ()  -> pure (TextResponse "Time limit exceeded")+      Right bs -> findDots dir >>= \case+        [] -> return (TextResponse bs)+        dot : [] -> do+          let imagePath = mkImagePath True dot+          _ <- run dotGraphExecutable dotGraphArgs dot $ Just ["-o" <> imagePath]+          pure (ImageResponse "image/png" imagePath Nothing Nothing)+        dots -> do+          images <- forM dots $ \dot -> do+            let imagePath = mkImagePath False dot+            _ <- run dotGraphExecutable dotGraphArgs dot $ Just ["-o" <> imagePath]+            pure imagePath++          let imagesAsArgs = CmdArgs (pack <$> images)+              fullImgHelperArgs = imageHelperArgs <> imagesAsArgs++          (_code, stdout, _stderr) <- run imageHelperExecutable fullImgHelperArgs "" Nothing++          let (mwidth, mheight, canvasArgs) = makeCanvasArgs stdout+              fullGifArgs = canvasArgs <> gifConverterArgs <> imagesAsArgs+              gifPath = mkGifPath path++          _ <- run gifConverterExecutable fullGifArgs gifPath Nothing+          pure (ImageResponse "image/gif" gifPath mwidth mheight)+    removeIntermediateFiles dir+    return result++makeCanvasArgs :: String -> (Maybe Int, Maybe Int, CmdArgs)+makeCanvasArgs stdout = (mwidth, mheight, args) +  where+    splitOn c x = (takeWhile (/= c) x, reverse . takeWhile (/= c) . reverse $ x)+    parse = fmap (splitOn '-') . filter (/= mempty) . lines+    parseInts (w, h) = case (readMaybe w, readMaybe h) of+      (Just wn, Just hn) -> Just (wn, hn)+      (Just wn, Nothing) -> Just (wn, 0 :: Int)+      (Nothing, Just hn) -> Just (0 :: Int, hn)+      _ -> Nothing+    safeMaximum [] = 0+    safeMaximum xs = maximum xs+    textDimensions = parse stdout+    dimensions = mapMaybe parseInts textDimensions+    maxWidth = safeMaximum (fst <$> dimensions)+    maxHeight = safeMaximum (snd <$> dimensions)+    restoreMaybe 0 = Nothing+    restoreMaybe x = Just x++    mwidth = restoreMaybe maxWidth+    mheight = restoreMaybe maxHeight+    dimensionsAsArgs = s2t maxWidth <> "x" <> s2t maxHeight+    args = CmdArgs ["-size", dimensionsAsArgs, "-extent", dimensionsAsArgs, "-sample", dimensionsAsArgs]++findDots :: FilePath -> IO [FilePath]+findDots dir = do+  contents <- listDirectory dir+  pure . filter ((== ".dot") . takeExtension) $ contents++removeIntermediateFiles :: FilePath -> IO ()+removeIntermediateFiles dir+  = listDirectory dir >>= mapM_ removeFile . filter ((/= ".als") . takeExtension)
src/Proof/Assistant/Arend.hs view
@@ -3,7 +3,6 @@ module Proof.Assistant.Arend where  import Control.Concurrent.Async (race)-import Data.ByteString (ByteString) import Data.Coerce (coerce) import Data.Text (unpack) import System.Directory (createDirectoryIfMissing, withCurrentDirectory)@@ -13,6 +12,7 @@ import Proof.Assistant.Helpers import Proof.Assistant.RefreshFile import Proof.Assistant.Request+import Proof.Assistant.Response import Proof.Assistant.ResourceLimit import Proof.Assistant.Settings import Proof.Assistant.State@@ -22,7 +22,7 @@  -- | Call Arend typechecker as CLI application. -- It prepares the CLI command, executes it and waits for response.-callArend :: InterpreterState ArendSettings -> InterpreterRequest -> IO ByteString+callArend :: InterpreterState ArendSettings -> InterpreterRequest -> IO BotResponse callArend InterpreterState{..} ir = do   let ArendSettings{..} = coerce settings       ExternalInterpreterSettings{..} = externalArend@@ -37,8 +37,8 @@         asyncTimer = asyncWait time     eresult <- race asyncTimer (handleErrorMaybe asyncExecutable)     case eresult of-      Left ()  -> pure "Time limit exceeded"-      Right bs -> pure bs+      Left ()  -> pure (TextResponse "Time limit exceeded")+      Right bs -> pure (TextResponse bs)  -- | Arend requires a project for every file to typecheck. -- It reads project configuration, finds all files in a project directory
src/Proof/Assistant/Bot.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} module Proof.Assistant.Bot where@@ -15,12 +16,12 @@  import qualified Data.HashMap.Strict as HashMap +import Agda.Interaction.State import Proof.Assistant.Helpers import Proof.Assistant.Interpreter import Proof.Assistant.Request import Proof.Assistant.Response import Proof.Assistant.Settings-import Agda.Interaction.State import Proof.Assistant.Transport import Proof.Assistant.Version @@ -36,7 +37,7 @@   | Debug String  -- ^ Write in STDOUT unknown input.  -- | Supported backends.-data Backend = Agda | Arend | Idris | Coq | Lean | Rzk+data Backend = Agda | Arend | Idris | Coq | Lean | Rzk | Alloy  -- | Initiate bot app based on a 'Model'. proofAssistantBot :: Model -> BotApp Model Action@@ -57,6 +58,7 @@   | isCommand "lean" update = Call <$> Just Lean <*> updateToRequest update   | isCommand "arend" update = Call <$> Just Arend <*> updateToRequest update   | isCommand "rzk" update = Call <$> Just Rzk <*> updateToRequest update+  | isCommand "alloy" update = Call <$> Just Alloy <*> updateToRequest update   -- other   | isCommand "help" update = Help <$> updateToRequest update   | isCommand "version" update = Version <$> updateToRequest update@@ -80,33 +82,41 @@       Idris -> handle idris       Lean -> handle lean       Rzk -> handle rzk+      Alloy -> handle alloy handleAction (SendBack response) model = model <# sendResponseBack True response handleAction (Help req) model = model <# do   let BotState {..} = model       Settings{..} = botSettings   case HashMap.lookup (bsToText $ interpreterRequestMessage req) helpMessages of-    Nothing -> sendResponseBack False $ makeTelegramResponse req (textToBS help) +    Nothing -> sendResponseBack False+      $ makeTelegramResponse req $ TextResponse $ textToBS help     Just helpMessage -> sendResponseBack False-      $ makeTelegramResponse req (textToBS helpMessage)+      $ makeTelegramResponse req $ TextResponse $ textToBS helpMessage handleAction (Version req) model = model <# do   let BotState {..} = model       Settings{..} = botSettings-  sendResponseBack False $ makeTelegramResponse req (textToBS $ makeVersion version)+  sendResponseBack False+    $ makeTelegramResponse req $ TextResponse $ textToBS $ makeVersion version handleAction (Debug str) model = model <# (liftIO $ putStrLn str)  -- | Helper that will try to deliver message even when Telegram failed to send it. sendResponseBack :: Bool -> InterpreterResponse -> BotM () sendResponseBack isMonospace response =-  let req = toSendMessageRequest isMonospace response+  let req = toMessageRequest isMonospace response+      sendIt = \case+        TgMsg msgReq -> sendMessage msgReq+        TgPng imageReq -> sendPhoto imageReq+        TgGif gifReq -> sendAnimation gifReq       waitAndRetry result = if responseOk result         then pure ()         else case responseParameters result >>= responseParametersRetryAfter of                Nothing -> pure ()                Just sec -> do                  liftIO . threadDelay $ coerce sec * 1000000-                 void (sendMessage req)+                 void $ sendIt req+   in liftClientM $ do-    result <- sendMessage req+    result <- sendIt req     waitAndRetry result  -- | Initiate Telegram Env, 'Model', start Bot, start backends concurrently.@@ -127,7 +137,8 @@       Concurrently (runInterpreter state coq) *>       Concurrently (runInterpreter state idris) *>       Concurrently (runInterpreter state lean) *>-      Concurrently (runInterpreter state rzk)+      Concurrently (runInterpreter state rzk) *>+      Concurrently (runInterpreter state alloy)   -- | Main function. run :: IO ()
src/Proof/Assistant/Helpers.hs view
@@ -27,6 +27,10 @@ t2s :: Coercible a Text => a -> String t2s = Text.unpack . coerce +-- | Cast something as 'Text'.+s2t :: Show a => a -> Text+s2t = Text.pack . show+ -- | Wait N seconds. asyncWait :: Time -> IO () asyncWait n = threadDelay (toInt @_ @Natural n * 1000000)
src/Proof/Assistant/Idris.hs view
@@ -9,6 +9,7 @@ import Idris.Interaction.Command import Proof.Assistant.Helpers import Proof.Assistant.Request+import Proof.Assistant.Response import Proof.Assistant.ResourceLimit import Proof.Assistant.Settings import Proof.Assistant.State@@ -17,10 +18,10 @@  -- | Call Idris 2 as CLI application. -- It prepares the CLI command, executes it and waits for response.-callIdris2 :: InterpreterState IdrisSettings -> InterpreterRequest -> IO ByteString+callIdris2 :: InterpreterState IdrisSettings -> InterpreterRequest -> IO BotResponse callIdris2 InterpreterState{..} ir@InterpreterRequest{..}   = case parseRequest interpreterRequestMessage of-      Left err -> pure err+      Left err -> pure (TextResponse err)       Right (ecmd, request) -> do         let s@ExternalInterpreterSettings{..} = coerce settings         action <- chooseCommand s ir ecmd request@@ -32,8 +33,8 @@             asyncTimer = asyncWait time         eresult <- race asyncTimer (handleErrorMaybe asyncExecutable)         case eresult of-          Left ()  -> pure "Time limit exceeded"-          Right bs -> pure bs+          Left ()  -> pure (TextResponse "Time limit exceeded")+          Right bs -> pure (TextResponse bs)  -- | Parse command. It could be unknown command or 'IdrisCommand' sub-command with its arguments -- or even expression to evaluate.
src/Proof/Assistant/Interpreter.hs view
@@ -15,7 +15,6 @@  import Control.Concurrent.Async import Control.Monad (forever)-import Data.ByteString (ByteString) import Data.Coerce (coerce) import Data.Text (unpack) import System.Directory@@ -24,6 +23,7 @@ import Agda.Interaction.State  import Proof.Assistant.Agda+import Proof.Assistant.Alloy import Proof.Assistant.Arend import Proof.Assistant.Idris import Proof.Assistant.Lean@@ -51,7 +51,7 @@ -- Could be CLI, Haskell function, network, whatever. -- It should have the @state@ and associated @settings@ with the @state@. class Interpreter state settings | state -> settings where-  interpretSafe :: state -> InterpreterRequest -> IO ByteString+  interpretSafe :: state -> InterpreterRequest -> IO BotResponse   getSettings :: state -> InterpreterState settings  instance Interpreter InternalState InternalInterpreterSettings  where@@ -81,11 +81,15 @@   interpretSafe state request = callArend state request   getSettings = id +instance Interpreter (InterpreterState AlloySettings) AlloySettings where+  interpretSafe state request = callAlloy state request+  getSettings = id+ -- ** External Interpreter  -- | Call some external CLI application, probably Coq. callExternalInterpreter-  :: ExternalInterpreterSettings -> (FilePath, FilePath) -> IO ByteString+  :: ExternalInterpreterSettings -> (FilePath, FilePath) -> IO BotResponse callExternalInterpreter ExternalInterpreterSettings{..} (dir, path)   = withCurrentDirectory dir $ do       contents <- readFile path@@ -96,5 +100,5 @@           asyncTimer = asyncWait time       eresult <- race asyncTimer (handleErrorMaybe asyncExecutable)       case eresult of-        Left ()  -> pure "Time limit exceeded"-        Right bs -> pure bs+        Left ()  -> pure (TextResponse "Time limit exceeded")+        Right bs -> pure (TextResponse bs)
src/Proof/Assistant/Lean.hs view
@@ -3,30 +3,27 @@ module Proof.Assistant.Lean where  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.Exit (ExitCode) import System.Process (readProcessWithExitCode)  import Proof.Assistant.Helpers import Proof.Assistant.RefreshFile import Proof.Assistant.Request+import Proof.Assistant.Response import Proof.Assistant.ResourceLimit import Proof.Assistant.Settings import Proof.Assistant.State -import qualified Data.Text as Text--callLean :: InterpreterState LeanSettings -> InterpreterRequest -> IO ByteString+callLean :: InterpreterState LeanSettings -> InterpreterRequest -> IO BotResponse callLean InterpreterState{..} ir = do-  let ls@LeanSettings{..} = coerce settings+  let LeanSettings{..} = coerce settings       s@ExternalInterpreterSettings{..} = externalLean-  (dir, path) <- refreshTmpFile s (validateLean ls ir) (Just projectDir)+  (dir, path) <- refreshTmpFile s ir (Just projectDir)   withCurrentDirectory dir $ do-    let fullArgs = (unpack <$> coerce args) <> [path]-        runProcess = readProcessWithExitCode (t2s executable) fullArgs ""+    let runProcess = runWithSandboxMaybe sandbox executable args path         asyncExecutable = do           setPriority priority           (_exitCode, stdout, stderr) <- runProcess@@ -34,15 +31,16 @@         asyncTimer = asyncWait time     eresult <- race asyncTimer (handleErrorMaybe asyncExecutable)     case eresult of-      Left ()  -> pure "Time limit exceeded"-      Right bs -> pure bs+      Left ()  -> pure (TextResponse "Time limit exceeded")+      Right bs -> pure (TextResponse bs) -validateLean :: LeanSettings -> InterpreterRequest -> InterpreterRequest-validateLean LeanSettings{..} ir@InterpreterRequest{..}-  = ir { interpreterRequestMessage = validatedMsg }+runWithSandboxMaybe+  :: Maybe SandboxSettings -> Executable -> CmdArgs -> FilePath -> IO (ExitCode, String, String)+runWithSandboxMaybe Nothing exec arguments path+  = readProcessWithExitCode (t2s exec) ((unpack <$> coerce arguments) <> [path]) ""+runWithSandboxMaybe (Just SandboxSettings{..}) exec arguments path+  = readProcessWithExitCode (t2s sandboxExecutable) fullArgsList ""   where-    remove txt blockedPrefix = Text.replace blockedPrefix "" txt-    removeAllFromLine x = foldl' remove x leanBlockList-    removeUnsafeImports = textToBS . removeAllFromLine . bsToText--    validatedMsg = removeUnsafeImports interpreterRequestMessage+    sandboxArgsList = unpack <$> coerce sandboxArgs+    appArgsList = t2s exec : (unpack <$> coerce arguments)+    fullArgsList = concat [sandboxArgsList, ["--"], appArgsList, [path]]
src/Proof/Assistant/Response.hs view
@@ -5,42 +5,84 @@ import Data.ByteString (ByteString) import Data.Text.Encoding (decodeUtf8) import Telegram.Bot.API-  (ChatId, MessageId, ParseMode (..), SendMessageRequest (..), SomeChatId (..))+  (ChatId, ContentType, MessageId+  , InputFile (..), ParseMode (..), PhotoFile (..)+  , SendAnimationRequest (..), SendMessageRequest (..), SendPhotoRequest (..), SomeChatId (..)+  , defSendAnimation, defSendMessage, defSendPhoto+  )  import Proof.Assistant.Request +-- | Bot response: either text message or picture (filepath and its content type).+data BotResponse+  = TextResponse !ByteString+  | ImageResponse+      { imgResponseCType :: !ContentType+      , imgResponsePath :: !FilePath+      , imgResponeWidth :: !(Maybe Int)+      , imgResponseHeight :: !(Maybe Int)+      }+ -- | Response for Telegram. data InterpreterResponse = InterpreterResponse   { interpreterResponseTelegramChatId :: !ChatId -- ^ Telegram ChatId (for reply).   , interpreterResponseTelegramMessageId :: !MessageId -- ^ Telegram MessageId (for reply).-  , interpreterResponseResponse :: !ByteString -- ^ output data.+  , interpreterResponseResponse :: !BotResponse -- ^ output data.   } --- | Cast 'InterpreterResponse' to 'SendMessageRequest'.--- If first argument is 'True'+data TelegramMessage+  = TgMsg SendMessageRequest+  | TgPng SendPhotoRequest+  | TgGif SendAnimationRequest++-- | Cast 'InterpreterResponse' to either 'SendMessageRequest' or 'SendPhotoRequest'.+-- For text messages:+-- - If first argument is 'True' -- 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 'True' should be specified.-toSendMessageRequest :: Bool -> InterpreterResponse -> SendMessageRequest-toSendMessageRequest isMonospace InterpreterResponse{..} = SendMessageRequest-  { sendMessageChatId                   = SomeChatId interpreterResponseTelegramChatId-  , sendMessageMessageThreadId          = Nothing-  , sendMessageText-      = if isMonospace-        then "```\n" <> decodeUtf8 interpreterResponseResponse <> "\n```\n"-        else decodeUtf8 interpreterResponseResponse <> "\n"-  , sendMessageParseMode                = if isMonospace then Just MarkdownV2 else Nothing-  , sendMessageEntities                 = Nothing-  , sendMessageDisableWebPagePreview    = Nothing-  , sendMessageDisableNotification      = Nothing-  , sendMessageProtectContent           = Nothing-  , sendMessageReplyToMessageId         = Just interpreterResponseTelegramMessageId-  , sendMessageAllowSendingWithoutReply = Nothing-  , sendMessageReplyMarkup              = Nothing-  }+-- - Otherwise, text message will be sent.+-- - For all responses from Backends 'True' should be specified.+-- +-- For images content type should be specified.+toMessageRequest+  :: Bool -> InterpreterResponse -> TelegramMessage+toMessageRequest isMonospace InterpreterResponse{..} = case interpreterResponseResponse of+  TextResponse bytes -> TgMsg $ SendMessageRequest+    { sendMessageChatId                   = SomeChatId interpreterResponseTelegramChatId+    , sendMessageMessageThreadId          = Nothing+    , sendMessageText+        = if isMonospace+          then "```\n" <> decodeUtf8 bytes <> "\n```\n"+          else decodeUtf8 bytes <> "\n"+    , sendMessageParseMode                = if isMonospace then Just MarkdownV2 else Nothing+    , sendMessageEntities                 = Nothing+    , sendMessageReplyParameters          = Nothing+    , sendMessageLinkPreviewOptions       = Nothing+    , sendMessageDisableNotification      = Nothing+    , sendMessageProtectContent           = Nothing+    , sendMessageReplyToMessageId         = Just interpreterResponseTelegramMessageId+    , sendMessageReplyMarkup              = Nothing+    }+  ImageResponse ctype imgPath mwidth mheight -> case ctype of+    "image/png" ->+      let reply = defSendPhoto (SomeChatId interpreterResponseTelegramChatId)+            $ MakePhotoFile $ InputFile imgPath ctype+      in TgPng (reply { sendPhotoReplyToMessageId = Just interpreterResponseTelegramMessageId })+    "image/gif" ->+      let reply = defSendAnimation (SomeChatId interpreterResponseTelegramChatId)+            $ InputFile imgPath "image/gif"+      in TgGif+        (reply { sendAnimationReplyToMessageId = Just interpreterResponseTelegramMessageId+               , sendAnimationWidth = mwidth+               , sendAnimationHeight = mheight+               }) +    _ ->+      let reply =+            defSendMessage (SomeChatId interpreterResponseTelegramChatId) "Unsupported request"+      in TgMsg (reply { sendMessageReplyToMessageId = Just interpreterResponseTelegramMessageId })+ -- | Cast 'InterpreterRequest' and output data to 'InterpreterResponse'.-makeTelegramResponse :: InterpreterRequest -> ByteString -> InterpreterResponse+makeTelegramResponse :: InterpreterRequest -> BotResponse -> InterpreterResponse makeTelegramResponse InterpreterRequest{..} response =   InterpreterResponse     { interpreterResponseTelegramChatId    = interpreterRequestTelegramChatId
src/Proof/Assistant/Rzk.hs view
@@ -3,30 +3,30 @@ module Proof.Assistant.Rzk where  import Control.Concurrent.Async (race)-import Data.ByteString (ByteString) import Data.Coerce (coerce) import System.Mem -import Rzk.Polylingual+import Rzk.Main  import Proof.Assistant.Helpers import Proof.Assistant.Request+import Proof.Assistant.Response import Proof.Assistant.Settings import Proof.Assistant.State  -- | Call Polilyngual API. Rzk will do all the job and return response or an error as result.-callRzk :: InterpreterState InternalInterpreterSettings -> InterpreterRequest -> IO ByteString+callRzk :: InterpreterState InternalInterpreterSettings -> InterpreterRequest -> IO BotResponse callRzk InterpreterState{..} ir = do   let InternalInterpreterSettings{..} = settings       asyncApi = do         enableAllocationLimit         setAllocationCounter (fromIntegral allocations)         let makeResult = pure-              . either toBS (toBS . compileSomeModule)-              . safeParseSomeModule . fromBS . dropCommand+              . either toBS toBS+              . typecheckString . fromBS . dropCommand         makeResult (interpreterRequestMessage ir)       asyncTimer = asyncWait (coerce timeout)   eresult <- race asyncTimer (handleErrorMaybe asyncApi)   case eresult of-    Left () -> pure "Time limit exceeded"-    Right result -> pure result+    Left () -> pure (TextResponse "Time limit exceeded")+    Right result -> pure (TextResponse result)
src/Proof/Assistant/Settings.hs view
@@ -3,6 +3,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE OverloadedStrings #-} module Proof.Assistant.Settings where @@ -17,6 +18,7 @@   , helpMessages :: HashMap Text Text -- ^ Help messages for sub-commands.   , version :: Text -- ^ Version message.   , interpretersSettings :: !InterpretersSettings -- ^ Settings for backend interpreters.+  , sharedDir :: !FilePath   } deriving (Generic, FromDhall)  data ExternalInterpreterSettings = ExternalInterpreterSettings@@ -28,6 +30,7 @@   , tempFilePrefix :: !FilePath -- ^ Prefix to filepath to avoid confusion between different interpreters.   , fileExtension :: !FilePath -- ^ File extension used by interpreter.   , inputSize :: !Natural -- ^ input size in bytes.+  , sandbox :: !(Maybe SandboxSettings)   } deriving (Generic, FromDhall)  data InternalInterpreterSettings = InternalInterpreterSettings@@ -44,7 +47,6 @@  data LeanSettings = LeanSettings   { projectDir :: !FilePath -- ^ Lean requires project where to store source files for typechecking.-  , leanBlockList :: [Text]   , externalLean   :: !ExternalInterpreterSettings   } deriving (Generic, FromDhall) @@ -56,13 +58,25 @@   , externalArend :: !ExternalInterpreterSettings   } deriving (Generic, FromDhall) +data AlloySettings = AlloySettings+  { alloyProjectDir :: !FilePath+  , dotGraphExecutable :: !Executable+  , dotGraphArgs :: !CmdArgs+  , imageHelperExecutable :: !Executable+  , imageHelperArgs :: !CmdArgs+  , gifConverterExecutable :: !Executable+  , gifConverterArgs :: !CmdArgs+  , alloySharedDir :: !FilePath+  , externalAlloy :: !ExternalInterpreterSettings+  } deriving (Generic, FromDhall)+ newtype IdrisSettings = IdrisSettings ExternalInterpreterSettings   deriving newtype (FromDhall, ToInterpreterState)   deriving stock Generic  newtype CmdArgs = CmdArgs [Text]   deriving stock Generic-  deriving newtype FromDhall+  deriving newtype (FromDhall, Semigroup)  newtype Executable = Executable Text   deriving stock Generic@@ -91,6 +105,11 @@   , hard :: !Natural   } deriving (Generic, FromDhall) +data SandboxSettings = SandboxSettings+  { sandboxExecutable :: !Executable+  , sandboxArgs :: !CmdArgs+  } deriving (Generic, FromDhall)+ -- | Combination of all supported interpreters settings. data InterpretersSettings = InterpretersSettings   { agda  :: !AgdaSettings@@ -99,6 +118,7 @@   , coq   :: !ExternalInterpreterSettings   , lean  :: !LeanSettings   , rzk   :: !InternalInterpreterSettings+  , alloy :: !AlloySettings   } deriving (Generic, FromDhall)  -- | Load settings from file.@@ -114,10 +134,10 @@   getQueueSize :: settings -> Natural  instance ToInterpreterState InternalInterpreterSettings where-  getQueueSize = inputSize+  getQueueSize InternalInterpreterSettings{inputSize} = inputSize  instance ToInterpreterState ExternalInterpreterSettings where-  getQueueSize = inputSize+  getQueueSize ExternalInterpreterSettings{inputSize} = inputSize  instance ToInterpreterState AgdaSettings where   getQueueSize = getQueueSize . internal@@ -127,3 +147,6 @@  instance ToInterpreterState ArendSettings where   getQueueSize = getQueueSize . externalArend++instance ToInterpreterState AlloySettings where+  getQueueSize = getQueueSize . externalAlloy
src/Proof/Assistant/Transport.hs view
@@ -22,6 +22,7 @@   , coq   :: !ExternalState   , lean  :: !(InterpreterState LeanSettings)   , rzk   :: !InternalState+  , alloy :: !(InterpreterState AlloySettings)   }  -- | Initiate new interpreters from settings.@@ -33,6 +34,7 @@   coq <- newInterpreterState $ Settings.coq settings   lean <- newInterpreterState $ Settings.lean settings   rzk <- newInterpreterState $ Settings.rzk settings+  alloy <- newInterpreterState $ Settings.alloy settings   pure Interpreters{..}  type ExternalState = InterpreterState ExternalInterpreterSettings
src/Proof/Assistant/Version.hs view
@@ -8,6 +8,10 @@  import qualified Data.Text as Text +-- | Version of Agda.+agdaVersion :: String+agdaVersion = VERSION_Agda+ -- | Version of Rzk. rzkVersion :: String rzkVersion = VERSION_rzk@@ -19,6 +23,7 @@ -- | Helper to build version from template message. makeVersion :: Text -> Text makeVersion txt = Text.unlines-  [ Text.replace "<bot_version>" (Text.pack proofAssistantBotVersion) txt+  [ Text.replace "<bot_version>" (Text.pack proofAssistantBotVersion)+    $ Text.replace "<agda_version>" (Text.pack agdaVersion) txt   , "rzk v." <> Text.pack rzkVersion   ]