diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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)). diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/proof-assistant-bot.cabal b/proof-assistant-bot.cabal --- a/proof-assistant-bot.cabal +++ b/proof-assistant-bot.cabal @@ -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 diff --git a/src/Agda/Interaction/Command/EvalIn.hs b/src/Agda/Interaction/Command/EvalIn.hs --- a/src/Agda/Interaction/Command/EvalIn.hs +++ b/src/Agda/Interaction/Command/EvalIn.hs @@ -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 diff --git a/src/Agda/Interaction/Command/EvalTerm.hs b/src/Agda/Interaction/Command/EvalTerm.hs --- a/src/Agda/Interaction/Command/EvalTerm.hs +++ b/src/Agda/Interaction/Command/EvalTerm.hs @@ -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) diff --git a/src/Agda/Interaction/Command/GiveMeta.hs b/src/Agda/Interaction/Command/GiveMeta.hs --- a/src/Agda/Interaction/Command/GiveMeta.hs +++ b/src/Agda/Interaction/Command/GiveMeta.hs @@ -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 (..)) diff --git a/src/Agda/Interaction/Command/Internal/Parser.hs b/src/Agda/Interaction/Command/Internal/Parser.hs --- a/src/Agda/Interaction/Command/Internal/Parser.hs +++ b/src/Agda/Interaction/Command/Internal/Parser.hs @@ -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 diff --git a/src/Agda/Interaction/Command/RefineMeta.hs b/src/Agda/Interaction/Command/RefineMeta.hs --- a/src/Agda/Interaction/Command/RefineMeta.hs +++ b/src/Agda/Interaction/Command/RefineMeta.hs @@ -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 (..)) diff --git a/src/Agda/Interaction/Command/Reload.hs b/src/Agda/Interaction/Command/Reload.hs --- a/src/Agda/Interaction/Command/Reload.hs +++ b/src/Agda/Interaction/Command/Reload.hs @@ -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 diff --git a/src/Agda/Interaction/Command/ShowConstraints.hs b/src/Agda/Interaction/Command/ShowConstraints.hs --- a/src/Agda/Interaction/Command/ShowConstraints.hs +++ b/src/Agda/Interaction/Command/ShowConstraints.hs @@ -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 diff --git a/src/Agda/Interaction/Command/ShowContext.hs b/src/Agda/Interaction/Command/ShowContext.hs --- a/src/Agda/Interaction/Command/ShowContext.hs +++ b/src/Agda/Interaction/Command/ShowContext.hs @@ -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 diff --git a/src/Agda/Interaction/Command/ShowMetas.hs b/src/Agda/Interaction/Command/ShowMetas.hs --- a/src/Agda/Interaction/Command/ShowMetas.hs +++ b/src/Agda/Interaction/Command/ShowMetas.hs @@ -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 diff --git a/src/Agda/Interaction/Command/ShowScope.hs b/src/Agda/Interaction/Command/ShowScope.hs --- a/src/Agda/Interaction/Command/ShowScope.hs +++ b/src/Agda/Interaction/Command/ShowScope.hs @@ -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) diff --git a/src/Agda/Interaction/Command/TypeIn.hs b/src/Agda/Interaction/Command/TypeIn.hs --- a/src/Agda/Interaction/Command/TypeIn.hs +++ b/src/Agda/Interaction/Command/TypeIn.hs @@ -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 diff --git a/src/Agda/Interaction/Command/TypeOf.hs b/src/Agda/Interaction/Command/TypeOf.hs --- a/src/Agda/Interaction/Command/TypeOf.hs +++ b/src/Agda/Interaction/Command/TypeOf.hs @@ -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 diff --git a/src/Agda/Interaction/State.hs b/src/Agda/Interaction/State.hs --- a/src/Agda/Interaction/State.hs +++ b/src/Agda/Interaction/State.hs @@ -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'. diff --git a/src/Proof/Assistant/Agda.hs b/src/Proof/Assistant/Agda.hs --- a/src/Proof/Assistant/Agda.hs +++ b/src/Proof/Assistant/Agda.hs @@ -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. diff --git a/src/Proof/Assistant/Alloy.hs b/src/Proof/Assistant/Alloy.hs new file mode 100644 --- /dev/null +++ b/src/Proof/Assistant/Alloy.hs @@ -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) diff --git a/src/Proof/Assistant/Arend.hs b/src/Proof/Assistant/Arend.hs --- a/src/Proof/Assistant/Arend.hs +++ b/src/Proof/Assistant/Arend.hs @@ -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 diff --git a/src/Proof/Assistant/Bot.hs b/src/Proof/Assistant/Bot.hs --- a/src/Proof/Assistant/Bot.hs +++ b/src/Proof/Assistant/Bot.hs @@ -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 () diff --git a/src/Proof/Assistant/Helpers.hs b/src/Proof/Assistant/Helpers.hs --- a/src/Proof/Assistant/Helpers.hs +++ b/src/Proof/Assistant/Helpers.hs @@ -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) diff --git a/src/Proof/Assistant/Idris.hs b/src/Proof/Assistant/Idris.hs --- a/src/Proof/Assistant/Idris.hs +++ b/src/Proof/Assistant/Idris.hs @@ -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. diff --git a/src/Proof/Assistant/Interpreter.hs b/src/Proof/Assistant/Interpreter.hs --- a/src/Proof/Assistant/Interpreter.hs +++ b/src/Proof/Assistant/Interpreter.hs @@ -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) diff --git a/src/Proof/Assistant/Lean.hs b/src/Proof/Assistant/Lean.hs --- a/src/Proof/Assistant/Lean.hs +++ b/src/Proof/Assistant/Lean.hs @@ -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]] diff --git a/src/Proof/Assistant/Response.hs b/src/Proof/Assistant/Response.hs --- a/src/Proof/Assistant/Response.hs +++ b/src/Proof/Assistant/Response.hs @@ -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 diff --git a/src/Proof/Assistant/Rzk.hs b/src/Proof/Assistant/Rzk.hs --- a/src/Proof/Assistant/Rzk.hs +++ b/src/Proof/Assistant/Rzk.hs @@ -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) diff --git a/src/Proof/Assistant/Settings.hs b/src/Proof/Assistant/Settings.hs --- a/src/Proof/Assistant/Settings.hs +++ b/src/Proof/Assistant/Settings.hs @@ -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 diff --git a/src/Proof/Assistant/Transport.hs b/src/Proof/Assistant/Transport.hs --- a/src/Proof/Assistant/Transport.hs +++ b/src/Proof/Assistant/Transport.hs @@ -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 diff --git a/src/Proof/Assistant/Version.hs b/src/Proof/Assistant/Version.hs --- a/src/Proof/Assistant/Version.hs +++ b/src/Proof/Assistant/Version.hs @@ -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 "" (Text.pack proofAssistantBotVersion) txt + [ Text.replace "" (Text.pack proofAssistantBotVersion) + $ Text.replace "" (Text.pack agdaVersion) txt , "rzk v." <> Text.pack rzkVersion ]