Agda.Utils.ProfileOptions

Documentation

data ProfileOption

Various things that can be measured when checking an Agda development. Turned on with the `--profile` flag, for instance `--profile=sharing` to turn on the Sharing option. Internal, Modules, and Definitions are mutually exclusive.

NOTE: Changing this data type requires bumping the interface version number in currentInterfaceVersion.

Constructors

Internal

Measure time taken by various parts of the system (type checking, serialization, etc)

Modules

Measure time spent on individual (Agda) modules

Definitions

Measure time spent on individual (Agda) definitions

Sharing

Measure things related to sharing

Serialize

Collect detailed statistics about serialization

Constraints

Collect statistics about constraint solving

Metas

Count number of created metavariables

Interactive

Measure time of interactive commands

Conversion

Collect statistics about conversion checking

Instances

EmbPrj ProfileOption

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ProfileOption -> S Int32

icod_ :: ProfileOption -> S Int32

value :: Int32 -> R ProfileOption

Bounded ProfileOption

Defined in Agda.Utils.ProfileOptions

Methods

minBound :: ProfileOption

maxBound :: ProfileOption

Enum ProfileOption

Defined in Agda.Utils.ProfileOptions

Methods

succ :: ProfileOption -> ProfileOption

pred :: ProfileOption -> ProfileOption

toEnum :: Int -> ProfileOption

fromEnum :: ProfileOption -> Int

enumFrom :: ProfileOption -> [ProfileOption]

enumFromThen :: ProfileOption -> ProfileOption -> [ProfileOption]

enumFromTo :: ProfileOption -> ProfileOption -> [ProfileOption]

enumFromThenTo :: ProfileOption -> ProfileOption -> ProfileOption -> [ProfileOption]

Generic ProfileOption

Defined in Agda.Utils.ProfileOptions

Associated Types

type Rep ProfileOption

Defined in Agda.Utils.ProfileOptions

type Rep ProfileOption = D1 ('MetaData "ProfileOption" "Agda.Utils.ProfileOptions" "Agda-2.6.4.2-inplace" 'False) (((C1 ('MetaCons "Internal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Modules" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Definitions" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Sharing" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Serialize" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Constraints" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Metas" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Interactive" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Conversion" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: ProfileOption -> Rep ProfileOption x

to :: Rep ProfileOption x -> ProfileOption

Show ProfileOption

Defined in Agda.Utils.ProfileOptions

Methods

showsPrec :: Int -> ProfileOption -> ShowS

show :: ProfileOption -> String

showList :: [ProfileOption] -> ShowS

NFData ProfileOption

Defined in Agda.Utils.ProfileOptions

Methods

rnf :: ProfileOption -> ()

Eq ProfileOption

Defined in Agda.Utils.ProfileOptions

Methods

(==) :: ProfileOption -> ProfileOption -> Bool

(/=) :: ProfileOption -> ProfileOption -> Bool

Ord ProfileOption

Defined in Agda.Utils.ProfileOptions

Methods

compare :: ProfileOption -> ProfileOption -> Ordering

(<) :: ProfileOption -> ProfileOption -> Bool

(<=) :: ProfileOption -> ProfileOption -> Bool

(>) :: ProfileOption -> ProfileOption -> Bool

(>=) :: ProfileOption -> ProfileOption -> Bool

max :: ProfileOption -> ProfileOption -> ProfileOption

min :: ProfileOption -> ProfileOption -> ProfileOption

type Rep ProfileOption

Defined in Agda.Utils.ProfileOptions

type Rep ProfileOption = D1 ('MetaData "ProfileOption" "Agda.Utils.ProfileOptions" "Agda-2.6.4.2-inplace" 'False) (((C1 ('MetaCons "Internal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Modules" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Definitions" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Sharing" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Serialize" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Constraints" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Metas" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Interactive" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Conversion" 'PrefixI 'False) (U1 :: Type -> Type)))))

data ProfileOptions

A set of ProfileOptions

Instances

EmbPrj ProfileOptions

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ProfileOptions -> S Int32

icod_ :: ProfileOptions -> S Int32

value :: Int32 -> R ProfileOptions

Null ProfileOptions

Defined in Agda.Utils.ProfileOptions

Methods

empty :: ProfileOptions

null :: ProfileOptions -> Bool

Show ProfileOptions

Defined in Agda.Utils.ProfileOptions

Methods

showsPrec :: Int -> ProfileOptions -> ShowS

show :: ProfileOptions -> String

showList :: [ProfileOptions] -> ShowS

NFData ProfileOptions

Defined in Agda.Utils.ProfileOptions

Methods

rnf :: ProfileOptions -> ()

Eq ProfileOptions

Defined in Agda.Utils.ProfileOptions

Methods

(==) :: ProfileOptions -> ProfileOptions -> Bool

(/=) :: ProfileOptions -> ProfileOptions -> Bool

noProfileOptions :: ProfileOptions

The empty set of profiling options.

addProfileOption :: String -> ProfileOptions -> Either String ProfileOptions

Parse and add a profiling option to a set of profiling options. Returns Left with a helpful error message if the option doesn't parse or if it's incompatible with existing options. The special string "all" adds all options compatible with the given set and prefering the first of incompatible options. So `--profile=all` sets Internal over Modules and Definitions, but `--profile=modules --profile=all` sets Modules and not Internal.

containsProfileOption :: ProfileOption -> ProfileOptions -> Bool

Check if a given profiling option is present in a set of profiling options.

profileOptionsToList :: ProfileOptions -> [ProfileOption]

Use only for serialization.

profileOptionsFromList :: [ProfileOption] -> ProfileOptions

Use only for serialization.

validProfileOptionStrings :: [String]

Strings accepted by addProfileOption