proof-assistant-bot-0.2.0: Telegram bot for proof assistants
Safe HaskellNone
LanguageHaskell2010

Proof.Assistant.Settings

Synopsis

Documentation

data Settings Source #

Constructors

Settings 

Fields

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

data ExternalInterpreterSettings Source #

Constructors

ExternalInterpreterSettings 

Fields

Instances

Instances details
Generic ExternalInterpreterSettings Source # 
Instance details

Defined in Proof.Assistant.Settings

Associated Types

type Rep ExternalInterpreterSettings :: Type -> Type #

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

Interpreter ExternalState ExternalInterpreterSettings Source # 
Instance details

Defined in Proof.Assistant.Interpreter

type Rep ExternalInterpreterSettings Source # 
Instance details

Defined in Proof.Assistant.Settings

data InternalInterpreterSettings Source #

Constructors

InternalInterpreterSettings 

Fields

Instances

Instances details
Generic InternalInterpreterSettings Source # 
Instance details

Defined in Proof.Assistant.Settings

Associated Types

type Rep InternalInterpreterSettings :: Type -> Type #

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

Interpreter InternalState InternalInterpreterSettings Source # 
Instance details

Defined in Proof.Assistant.Interpreter

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.0-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 #

Instances

Instances details
Generic AgdaSettings Source # 
Instance details

Defined in Proof.Assistant.Settings

Associated Types

type Rep AgdaSettings :: Type -> Type #

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

Interpreter AgdaState AgdaSettings Source # 
Instance details

Defined in Proof.Assistant.Interpreter

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.0-inplace" 'False) (C1 ('MetaCons "AgdaSettings" 'PrefixI 'True) (S1 ('MetaSel ('Just "internal") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 InternalInterpreterSettings)))

data LeanSettings Source #

Constructors

LeanSettings 

Fields

Instances

Instances details
Generic LeanSettings Source # 
Instance details

Defined in Proof.Assistant.Settings

Associated Types

type Rep LeanSettings :: Type -> Type #

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

Interpreter (InterpreterState LeanSettings) LeanSettings Source # 
Instance details

Defined in Proof.Assistant.Interpreter

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.0-inplace" 'False) (C1 ('MetaCons "LeanSettings" 'PrefixI 'True) (S1 ('MetaSel ('Just "projectDir") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "externalLean") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ExternalInterpreterSettings)))

data ArendSettings Source #

Constructors

ArendSettings 

Fields

Instances

Instances details
Generic ArendSettings Source # 
Instance details

Defined in Proof.Assistant.Settings

Associated Types

type Rep ArendSettings :: Type -> Type #

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

Interpreter (InterpreterState ArendSettings) ArendSettings Source # 
Instance details

Defined in Proof.Assistant.Interpreter

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.0-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 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.0-inplace" 'True) (C1 ('MetaCons "CmdArgs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Text])))

newtype Packages Source #

Constructors

Packages Text 

Instances

Instances details
Generic Packages Source # 
Instance details

Defined in Proof.Assistant.Settings

Associated Types

type Rep Packages :: Type -> Type #

Methods

from :: Packages -> Rep Packages x #

to :: Rep Packages x -> Packages #

FromDhall Packages Source # 
Instance details

Defined in Proof.Assistant.Settings

Methods

autoWith :: InputNormalizer -> Decoder Packages

type Rep Packages Source # 
Instance details

Defined in Proof.Assistant.Settings

type Rep Packages = D1 ('MetaData "Packages" "Proof.Assistant.Settings" "proof-assistant-bot-0.2.0-inplace" 'True) (C1 ('MetaCons "Packages" '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 #

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.0-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.0-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.0-inplace" 'True) (C1 ('MetaCons "Priority" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Natural)))

data ResourceSettings Source #

Resource settings.

Instances

Instances details
Generic ResourceSettings Source # 
Instance details

Defined in Proof.Assistant.Settings

Associated Types

type Rep ResourceSettings :: Type -> Type #

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

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

loadSettings :: Text -> IO Settings Source #

Load settings from file.

loadDefaultSettings :: IO Settings Source #

Load default settings.