Safe Haskell	None
Language	Haskell2010

Proof.Assistant.Settings

Synopsis

data Settings = Settings {
- botName :: !Text
- botToken :: !Text
- outputSize :: !Natural
- help :: Text
- helpMessages :: HashMap Text Text
- version :: Text
- interpretersSettings :: !InterpretersSettings
}
data ExternalInterpreterSettings = ExternalInterpreterSettings {
- args :: !CmdArgs
- executable :: !Executable
- time :: !Time
- priority :: !Priority
- resources :: !ResourceSettings
- tempFilePrefix :: !FilePath
- fileExtension :: !FilePath
- inputSize :: !Natural
}
data InternalInterpreterSettings = InternalInterpreterSettings {
- timeout :: !Natural
- allocations :: !Natural
- inputSize :: !Natural
- sourceFilePrefix :: !FilePath
- sourceFileExtension :: !FilePath
}
data AgdaSettings = AgdaSettings {
- internal :: !InternalInterpreterSettings
}
data LeanSettings = LeanSettings {
- projectDir :: !FilePath
- leanBlockList :: [Text]
- externalLean :: !ExternalInterpreterSettings
}
data ArendSettings = ArendSettings {
- arendRootProjectDir :: !FilePath
- arendYamlFilename :: !FilePath
- arendYamlContent :: !Text
- arendModuleName :: !FilePath
- externalArend :: !ExternalInterpreterSettings
}
newtype IdrisSettings = IdrisSettings ExternalInterpreterSettings
newtype CmdArgs = CmdArgs [Text]
newtype Executable = Executable Text
newtype Time = Time Natural
newtype Priority = Priority Natural
data ResourceSettings = ResourceSettings {
- totalMemory :: !Limit
- dataSize :: !Limit
- openFiles :: !Limit
- fileSize :: !Limit
- cpuTime :: !Limit
}
data Limit = Limit {
- soft :: !Natural
- hard :: !Natural
}
data InterpretersSettings = InterpretersSettings {
- agda :: !AgdaSettings
- arend :: !ArendSettings
- idris :: !IdrisSettings
- coq :: !ExternalInterpreterSettings
- lean :: !LeanSettings
- rzk :: !InternalInterpreterSettings
}
loadSettings :: Text -> IO Settings
loadDefaultSettings :: IO Settings
class ToInterpreterState settings where
- getQueueSize :: settings -> Natural

Documentation

data Settings Source #

Constructors

Settings
Fields botName :: !Text Telegram bot name. Used to parse `/command@botname`. botToken :: !Text Bot token. outputSize :: !Natural output size in bytes. help :: Text Help message. helpMessages :: HashMap Text Text Help messages for sub-commands. version :: Text Version message. interpretersSettings :: !InterpretersSettings Settings for backend interpreters.

Instances

Instances details

Generic Settings Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep Settings :: Type -> Type # Methods from :: Settings -> Rep Settings x # to :: Rep Settings x -> Settings #
FromDhall Settings Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder Settings
type Rep Settings Source #
Instance details Defined in Proof.Assistant.Settings type Rep Settings = D1 ('MetaData "Settings" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'False) (C1 ('MetaCons "Settings" 'PrefixI 'True) ((S1 ('MetaSel ('Just "botName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text) :: (S1 ('MetaSel ('Just "botToken") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text) :: S1 ('MetaSel ('Just "outputSize") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Natural))) :: ((S1 ('MetaSel ('Just "help") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :: S1 ('MetaSel ('Just "helpMessages") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap Text Text))) :: (S1 ('MetaSel ('Just "version") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :: S1 ('MetaSel ('Just "interpretersSettings") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 InterpretersSettings)))))

data ExternalInterpreterSettings Source #

Constructors

ExternalInterpreterSettings

Fields

args :: !CmdArgs
CLI arguments.
executable :: !Executable
Path to executable.
time :: !Time
Time, in seconds.
priority :: !Priority
Priority for the thread.
resources :: !ResourceSettings
Different resources.
tempFilePrefix :: !FilePath
Prefix to filepath to avoid confusion between different interpreters.
fileExtension :: !FilePath
File extension used by interpreter.
inputSize :: !Natural
input size in bytes.

Instances

Instances details

Generic ExternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep ExternalInterpreterSettings :: Type -> Type # Methods from :: ExternalInterpreterSettings -> Rep ExternalInterpreterSettings x # to :: Rep ExternalInterpreterSettings x -> ExternalInterpreterSettings #
FromDhall ExternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder ExternalInterpreterSettings
ToInterpreterState ExternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods getQueueSize :: ExternalInterpreterSettings -> Natural Source #
Interpreter ExternalState ExternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Interpreter Methods interpretSafe :: ExternalState -> InterpreterRequest -> IO ByteString Source # getSettings :: ExternalState -> InterpreterState ExternalInterpreterSettings Source #
type Rep ExternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Settings type Rep ExternalInterpreterSettings = D1 ('MetaData "ExternalInterpreterSettings" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'False) (C1 ('MetaCons "ExternalInterpreterSettings" 'PrefixI 'True) (((S1 ('MetaSel ('Just "args") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 CmdArgs) :: S1 ('MetaSel ('Just "executable") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Executable)) :: (S1 ('MetaSel ('Just "time") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Time) :: S1 ('MetaSel ('Just "priority") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Priority))) :: ((S1 ('MetaSel ('Just "resources") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ResourceSettings) :: S1 ('MetaSel ('Just "tempFilePrefix") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FilePath)) :: (S1 ('MetaSel ('Just "fileExtension") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "inputSize") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Natural)))))

data InternalInterpreterSettings Source #

Constructors

InternalInterpreterSettings
Fields timeout :: !Natural Timeout in seconds. allocations :: !Natural Max number of GHC allocations for the interpreter thread. inputSize :: !Natural input size in bytes. sourceFilePrefix :: !FilePath Prefix to filepath to avoid confusion between different interpreters. sourceFileExtension :: !FilePath File extension used by interpreter.

Instances

Instances details

Generic InternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep InternalInterpreterSettings :: Type -> Type # Methods from :: InternalInterpreterSettings -> Rep InternalInterpreterSettings x # to :: Rep InternalInterpreterSettings x -> InternalInterpreterSettings #
FromDhall InternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder InternalInterpreterSettings
ToInterpreterState InternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods getQueueSize :: InternalInterpreterSettings -> Natural Source #
Interpreter InternalState InternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Interpreter Methods interpretSafe :: InternalState -> InterpreterRequest -> IO ByteString Source # getSettings :: InternalState -> InterpreterState InternalInterpreterSettings Source #
type Rep InternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Settings type Rep InternalInterpreterSettings = D1 ('MetaData "InternalInterpreterSettings" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'False) (C1 ('MetaCons "InternalInterpreterSettings" 'PrefixI 'True) ((S1 ('MetaSel ('Just "timeout") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Natural) :: S1 ('MetaSel ('Just "allocations") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Natural)) :: (S1 ('MetaSel ('Just "inputSize") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Natural) :: (S1 ('MetaSel ('Just "sourceFilePrefix") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FilePath) :: S1 ('MetaSel ('Just "sourceFileExtension") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FilePath)))))

data AgdaSettings Source #

Constructors

AgdaSettings
Fields internal :: !InternalInterpreterSettings

Instances

Instances details

Generic AgdaSettings Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep AgdaSettings :: Type -> Type # Methods from :: AgdaSettings -> Rep AgdaSettings x # to :: Rep AgdaSettings x -> AgdaSettings #
FromDhall AgdaSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder AgdaSettings
ToInterpreterState AgdaSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods getQueueSize :: AgdaSettings -> Natural Source #
Interpreter AgdaState AgdaSettings Source #
Instance details Defined in Proof.Assistant.Interpreter Methods interpretSafe :: AgdaState -> InterpreterRequest -> IO ByteString Source # getSettings :: AgdaState -> InterpreterState AgdaSettings Source #
type Rep AgdaSettings Source #
Instance details Defined in Proof.Assistant.Settings type Rep AgdaSettings = D1 ('MetaData "AgdaSettings" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'False) (C1 ('MetaCons "AgdaSettings" 'PrefixI 'True) (S1 ('MetaSel ('Just "internal") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 InternalInterpreterSettings)))

data LeanSettings Source #

Constructors

LeanSettings
Fields projectDir :: !FilePath Lean requires project where to store source files for typechecking. leanBlockList :: [Text] externalLean :: !ExternalInterpreterSettings

Instances

Instances details

Generic LeanSettings Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep LeanSettings :: Type -> Type # Methods from :: LeanSettings -> Rep LeanSettings x # to :: Rep LeanSettings x -> LeanSettings #
FromDhall LeanSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder LeanSettings
ToInterpreterState LeanSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods getQueueSize :: LeanSettings -> Natural Source #
Interpreter (InterpreterState LeanSettings) LeanSettings Source #
Instance details Defined in Proof.Assistant.Interpreter Methods interpretSafe :: InterpreterState LeanSettings -> InterpreterRequest -> IO ByteString Source # getSettings :: InterpreterState LeanSettings -> InterpreterState LeanSettings Source #
type Rep LeanSettings Source #
Instance details Defined in Proof.Assistant.Settings type Rep LeanSettings = D1 ('MetaData "LeanSettings" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'False) (C1 ('MetaCons "LeanSettings" 'PrefixI 'True) (S1 ('MetaSel ('Just "projectDir") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FilePath) :: (S1 ('MetaSel ('Just "leanBlockList") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Text]) :: S1 ('MetaSel ('Just "externalLean") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ExternalInterpreterSettings))))

data ArendSettings Source #

Constructors

ArendSettings

Fields

arendRootProjectDir :: !FilePath
Arend requires different directories to work correctly. One of them used to store libraries, settings, user projects. We call it "root directory".
arendYamlFilename :: !FilePath
For each project Arend requires yaml file with a specific name.
arendYamlContent :: !Text
For each project Arend requires yaml file to store specific settings inside.
arendModuleName :: !FilePath
Since Arend requires project per chat, it will have a single module inside and we want to give it a common specific configurable name.
externalArend :: !ExternalInterpreterSettings

Instances

Instances details

Generic ArendSettings Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep ArendSettings :: Type -> Type # Methods from :: ArendSettings -> Rep ArendSettings x # to :: Rep ArendSettings x -> ArendSettings #
FromDhall ArendSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder ArendSettings
ToInterpreterState ArendSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods getQueueSize :: ArendSettings -> Natural Source #
Interpreter (InterpreterState ArendSettings) ArendSettings Source #
Instance details Defined in Proof.Assistant.Interpreter Methods interpretSafe :: InterpreterState ArendSettings -> InterpreterRequest -> IO ByteString Source # getSettings :: InterpreterState ArendSettings -> InterpreterState ArendSettings Source #
type Rep ArendSettings Source #
Instance details Defined in Proof.Assistant.Settings type Rep ArendSettings = D1 ('MetaData "ArendSettings" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'False) (C1 ('MetaCons "ArendSettings" 'PrefixI 'True) ((S1 ('MetaSel ('Just "arendRootProjectDir") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FilePath) :: S1 ('MetaSel ('Just "arendYamlFilename") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FilePath)) :: (S1 ('MetaSel ('Just "arendYamlContent") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text) :: (S1 ('MetaSel ('Just "arendModuleName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FilePath) :: S1 ('MetaSel ('Just "externalArend") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ExternalInterpreterSettings)))))

newtype IdrisSettings Source #

Constructors

IdrisSettings ExternalInterpreterSettings

Instances

Instances details

Generic IdrisSettings Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep IdrisSettings :: Type -> Type # Methods from :: IdrisSettings -> Rep IdrisSettings x # to :: Rep IdrisSettings x -> IdrisSettings #
FromDhall IdrisSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder IdrisSettings
ToInterpreterState IdrisSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods getQueueSize :: IdrisSettings -> Natural Source #
Interpreter (InterpreterState IdrisSettings) IdrisSettings Source #
Instance details Defined in Proof.Assistant.Interpreter Methods interpretSafe :: InterpreterState IdrisSettings -> InterpreterRequest -> IO ByteString Source # getSettings :: InterpreterState IdrisSettings -> InterpreterState IdrisSettings Source #
type Rep IdrisSettings Source #
Instance details Defined in Proof.Assistant.Settings type Rep IdrisSettings = D1 ('MetaData "IdrisSettings" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'True) (C1 ('MetaCons "IdrisSettings" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExternalInterpreterSettings)))

newtype CmdArgs Source #

Constructors

CmdArgs [Text]

Instances

Instances details

Generic CmdArgs Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep CmdArgs :: Type -> Type # Methods from :: CmdArgs -> Rep CmdArgs x # to :: Rep CmdArgs x -> CmdArgs #
FromDhall CmdArgs Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder CmdArgs
type Rep CmdArgs Source #
Instance details Defined in Proof.Assistant.Settings type Rep CmdArgs = D1 ('MetaData "CmdArgs" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'True) (C1 ('MetaCons "CmdArgs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Text])))

newtype Executable Source #

Constructors

Executable Text

Instances

Instances details

Generic Executable Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep Executable :: Type -> Type # Methods from :: Executable -> Rep Executable x # to :: Rep Executable x -> Executable #
FromDhall Executable Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder Executable
type Rep Executable Source #
Instance details Defined in Proof.Assistant.Settings type Rep Executable = D1 ('MetaData "Executable" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'True) (C1 ('MetaCons "Executable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))

newtype Time Source #

Constructors

Time Natural

Instances

Instances details

Generic Time Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep Time :: Type -> Type # Methods from :: Time -> Rep Time x # to :: Rep Time x -> Time #
FromDhall Time Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder Time
type Rep Time Source #
Instance details Defined in Proof.Assistant.Settings type Rep Time = D1 ('MetaData "Time" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'True) (C1 ('MetaCons "Time" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Natural)))

newtype Priority Source #

Constructors

Priority Natural

Instances

Instances details

Generic Priority Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep Priority :: Type -> Type # Methods from :: Priority -> Rep Priority x # to :: Rep Priority x -> Priority #
FromDhall Priority Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder Priority
type Rep Priority Source #
Instance details Defined in Proof.Assistant.Settings type Rep Priority = D1 ('MetaData "Priority" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'True) (C1 ('MetaCons "Priority" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Natural)))

data ResourceSettings Source #

Resource settings.

Constructors

ResourceSettings
Fields totalMemory :: !Limit dataSize :: !Limit openFiles :: !Limit fileSize :: !Limit cpuTime :: !Limit

Instances

Instances details

Generic ResourceSettings Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep ResourceSettings :: Type -> Type # Methods from :: ResourceSettings -> Rep ResourceSettings x # to :: Rep ResourceSettings x -> ResourceSettings #
FromDhall ResourceSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder ResourceSettings
type Rep ResourceSettings Source #
Instance details Defined in Proof.Assistant.Settings type Rep ResourceSettings = D1 ('MetaData "ResourceSettings" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'False) (C1 ('MetaCons "ResourceSettings" 'PrefixI 'True) ((S1 ('MetaSel ('Just "totalMemory") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Limit) :: S1 ('MetaSel ('Just "dataSize") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Limit)) :: (S1 ('MetaSel ('Just "openFiles") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Limit) :: (S1 ('MetaSel ('Just "fileSize") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Limit) :: S1 ('MetaSel ('Just "cpuTime") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Limit)))))

data Limit Source #

Limits.

Constructors

Limit
Fields soft :: !Natural hard :: !Natural

Instances

Instances details

Generic Limit Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep Limit :: Type -> Type # Methods from :: Limit -> Rep Limit x # to :: Rep Limit x -> Limit #
FromDhall Limit Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder Limit
type Rep Limit Source #
Instance details Defined in Proof.Assistant.Settings type Rep Limit = D1 ('MetaData "Limit" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'False) (C1 ('MetaCons "Limit" 'PrefixI 'True) (S1 ('MetaSel ('Just "soft") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Natural) :*: S1 ('MetaSel ('Just "hard") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Natural)))

data InterpretersSettings Source #

Combination of all supported interpreters settings.

Constructors

InterpretersSettings
Fields agda :: !AgdaSettings arend :: !ArendSettings idris :: !IdrisSettings coq :: !ExternalInterpreterSettings lean :: !LeanSettings rzk :: !InternalInterpreterSettings

Instances

Instances details

Generic InterpretersSettings Source #
Instance details Defined in Proof.Assistant.Settings Associated Types type Rep InterpretersSettings :: Type -> Type # Methods from :: InterpretersSettings -> Rep InterpretersSettings x # to :: Rep InterpretersSettings x -> InterpretersSettings #
FromDhall InterpretersSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods autoWith :: InputNormalizer -> Decoder InterpretersSettings
type Rep InterpretersSettings Source #
Instance details Defined in Proof.Assistant.Settings type Rep InterpretersSettings = D1 ('MetaData "InterpretersSettings" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.1-inplace" 'False) (C1 ('MetaCons "InterpretersSettings" 'PrefixI 'True) ((S1 ('MetaSel ('Just "agda") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 AgdaSettings) :: (S1 ('MetaSel ('Just "arend") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ArendSettings) :: S1 ('MetaSel ('Just "idris") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 IdrisSettings))) :: (S1 ('MetaSel ('Just "coq") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ExternalInterpreterSettings) :: (S1 ('MetaSel ('Just "lean") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LeanSettings) :*: S1 ('MetaSel ('Just "rzk") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 InternalInterpreterSettings)))))

loadSettings :: Text -> IO Settings Source #

Load settings from file.

loadDefaultSettings :: IO Settings Source #

Load default settings.

class ToInterpreterState settings where Source #

Helper to get queue size (communication model between bot and backend worker).

Methods

getQueueSize :: settings -> Natural Source #

Instances

Instances details

ToInterpreterState IdrisSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods getQueueSize :: IdrisSettings -> Natural Source #
ToInterpreterState ArendSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods getQueueSize :: ArendSettings -> Natural Source #
ToInterpreterState LeanSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods getQueueSize :: LeanSettings -> Natural Source #
ToInterpreterState AgdaSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods getQueueSize :: AgdaSettings -> Natural Source #
ToInterpreterState InternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods getQueueSize :: InternalInterpreterSettings -> Natural Source #
ToInterpreterState ExternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Settings Methods getQueueSize :: ExternalInterpreterSettings -> Natural Source #