Agda-2.8.0: Agda.cabal
cabal-version: 2.4
name: Agda
version: 2.8.0
build-type: Simple
license: MIT
license-file: LICENSE
copyright: (c) 2005-2025 The Agda Team.
author: The Agda Team, see https://agda.readthedocs.io/en/latest/team.html
maintainer: The Agda Team
homepage: https://wiki.portal.chalmers.se/agda/
bug-reports: https://github.com/agda/agda/issues
category: Dependent types
synopsis: A dependently typed functional programming language and proof assistant
description:
Agda is a dependently typed functional programming language: It has
inductive families, which are similar to Haskell's GADTs, but they
can be indexed by values and not just types. It also has
parameterised modules, mixfix operators, Unicode characters, and an
interactive Emacs interface (the type checker can assist in the
development of your code).
.
Agda is also a proof assistant: It is an interactive system for
writing and checking proofs. Agda is based on intuitionistic type
theory, a foundational system for constructive mathematics developed
by the Swedish logician Per Martin-Löf. It has many
similarities with other proof assistants based on dependent types,
such as Rocq (formerly known as Coq), Idris, Lean and NuPRL.
.
This package includes both a command-line program (agda) and an
Emacs mode.
tested-with:
GHC == 9.12.2
GHC == 9.10.2
GHC == 9.8.4
GHC == 9.6.7
GHC == 9.4.8
GHC == 9.2.8
GHC == 9.0.2
GHC == 8.10.7
GHC == 8.8.4
extra-doc-files:
CHANGELOG.md
README.md
doc/user-manual/agda.svg
doc/release-notes/2.7.0.1.md
doc/release-notes/2.7.0.md
doc/release-notes/2.6.4.3.md
doc/release-notes/2.6.4.2.md
doc/release-notes/2.6.4.1.md
doc/release-notes/2.6.4.md
doc/release-notes/2.6.3.md
doc/release-notes/2.6.2.2.md
doc/release-notes/2.6.2.1.md
doc/release-notes/2.6.2.md
doc/release-notes/2.6.1.3.md
doc/release-notes/2.6.1.2.md
doc/release-notes/2.6.1.1.md
doc/release-notes/2.6.1.md
doc/release-notes/2.6.0.1.md
doc/release-notes/2.6.0.md
doc/release-notes/2.5.4.2.md
doc/release-notes/2.5.4.1.md
doc/release-notes/2.5.4.md
doc/release-notes/2.5.3.md
doc/release-notes/2.5.2.md
doc/release-notes/2.5.1.2.md
doc/release-notes/2.5.1.1.md
doc/release-notes/2.5.1.md
doc/release-notes/2.4.2.5.md
doc/release-notes/2.4.2.4.md
doc/release-notes/2.4.2.3.md
doc/release-notes/2.4.2.2.md
doc/release-notes/2.4.2.1.md
doc/release-notes/2.4.2.md
doc/release-notes/2.4.0.2.md
doc/release-notes/2.4.0.1.md
doc/release-notes/2.4.0.md
doc/release-notes/2.3.2.2.md
doc/release-notes/2.3.2.1.md
doc/release-notes/2.3.2.md
doc/release-notes/2.3.0.md
doc/release-notes/2.2.10.md
doc/release-notes/2.2.8.md
doc/release-notes/2.2.6.md
doc/release-notes/2.2.2.md
doc/release-notes/2.2.4.md
doc/release-notes/2.2.0.md
extra-source-files:
stack-9.12.2.yaml
stack-9.10.2.yaml
stack-9.8.4.yaml
stack-9.6.7.yaml
stack-9.4.8.yaml
stack-9.2.8.yaml
stack-9.0.2.yaml
stack-8.10.7.yaml
stack-8.8.4.yaml
-- Agda's data files, embedded by module Agda.Setup.
-- Keep in sync with the list in Agda.Setup.DataFiles and below.
src/data/emacs-mode/agda-input.el
src/data/emacs-mode/agda2-abbrevs.el
src/data/emacs-mode/agda2-highlight.el
src/data/emacs-mode/agda2-mode-pkg.el
src/data/emacs-mode/agda2-mode.el
src/data/emacs-mode/agda2-queue.el
src/data/emacs-mode/agda2.el
src/data/emacs-mode/annotation.el
src/data/emacs-mode/eri.el
src/data/html/Agda.css
src/data/html/highlight-hover.js
src/data/JS/agda-rts.mjs
src/data/JS/agda-rts.js
src/data/JS/agda-rts.amd.js
src/data/latex/agda.sty
src/data/latex/postprocess-latex.pl
src/data/lib/prim/agda-builtins.agda-lib
src/data/lib/prim/Agda/Builtin/Bool.agda
src/data/lib/prim/Agda/Builtin/Char.agda
src/data/lib/prim/Agda/Builtin/Char/Properties.agda
src/data/lib/prim/Agda/Builtin/Coinduction.agda
src/data/lib/prim/Agda/Builtin/Cubical/Path.agda
src/data/lib/prim/Agda/Builtin/Cubical/Sub.agda
src/data/lib/prim/Agda/Builtin/Cubical/Glue.agda
src/data/lib/prim/Agda/Builtin/Cubical/Equiv.agda
src/data/lib/prim/Agda/Builtin/Cubical/HCompU.agda
src/data/lib/prim/Agda/Builtin/Equality.agda
src/data/lib/prim/Agda/Builtin/Equality/Erase.agda
src/data/lib/prim/Agda/Builtin/Equality/Rewrite.agda
src/data/lib/prim/Agda/Builtin/Float.agda
src/data/lib/prim/Agda/Builtin/Float/Properties.agda
src/data/lib/prim/Agda/Builtin/FromNat.agda
src/data/lib/prim/Agda/Builtin/FromNeg.agda
src/data/lib/prim/Agda/Builtin/FromString.agda
src/data/lib/prim/Agda/Builtin/IO.agda
src/data/lib/prim/Agda/Builtin/Int.agda
src/data/lib/prim/Agda/Builtin/List.agda
src/data/lib/prim/Agda/Builtin/Maybe.agda
src/data/lib/prim/Agda/Builtin/Nat.agda
src/data/lib/prim/Agda/Builtin/Reflection.agda
src/data/lib/prim/Agda/Builtin/Reflection/External.agda
src/data/lib/prim/Agda/Builtin/Reflection/Properties.agda
src/data/lib/prim/Agda/Builtin/Sigma.agda
src/data/lib/prim/Agda/Builtin/Size.agda
src/data/lib/prim/Agda/Builtin/Strict.agda
src/data/lib/prim/Agda/Builtin/String.agda
src/data/lib/prim/Agda/Builtin/String/Properties.agda
src/data/lib/prim/Agda/Builtin/TrustMe.agda
src/data/lib/prim/Agda/Builtin/Unit.agda
src/data/lib/prim/Agda/Builtin/Word.agda
src/data/lib/prim/Agda/Builtin/Word/Properties.agda
src/data/lib/prim/Agda/Primitive.agda
src/data/lib/prim/Agda/Primitive/Cubical.agda
src/data/MAlonzo/src/MAlonzo/RTE.hs
src/data/MAlonzo/src/MAlonzo/RTE/Float.hs
data-dir: src/data
data-files:
emacs-mode/agda-input.el
emacs-mode/agda2-abbrevs.el
emacs-mode/agda2-highlight.el
emacs-mode/agda2-mode-pkg.el
emacs-mode/agda2-mode.el
emacs-mode/agda2-queue.el
emacs-mode/agda2.el
emacs-mode/annotation.el
emacs-mode/eri.el
html/Agda.css
html/highlight-hover.js
JS/agda-rts.mjs
JS/agda-rts.js
JS/agda-rts.amd.js
latex/agda.sty
latex/postprocess-latex.pl
lib/prim/agda-builtins.agda-lib
lib/prim/Agda/Builtin/Bool.agda
lib/prim/Agda/Builtin/Char.agda
lib/prim/Agda/Builtin/Char/Properties.agda
lib/prim/Agda/Builtin/Coinduction.agda
lib/prim/Agda/Builtin/Cubical/Path.agda
lib/prim/Agda/Builtin/Cubical/Sub.agda
lib/prim/Agda/Builtin/Cubical/Glue.agda
lib/prim/Agda/Builtin/Cubical/Equiv.agda
lib/prim/Agda/Builtin/Cubical/HCompU.agda
lib/prim/Agda/Builtin/Equality.agda
lib/prim/Agda/Builtin/Equality/Erase.agda
lib/prim/Agda/Builtin/Equality/Rewrite.agda
lib/prim/Agda/Builtin/Float.agda
lib/prim/Agda/Builtin/Float/Properties.agda
lib/prim/Agda/Builtin/FromNat.agda
lib/prim/Agda/Builtin/FromNeg.agda
lib/prim/Agda/Builtin/FromString.agda
lib/prim/Agda/Builtin/IO.agda
lib/prim/Agda/Builtin/Int.agda
lib/prim/Agda/Builtin/List.agda
lib/prim/Agda/Builtin/Maybe.agda
lib/prim/Agda/Builtin/Nat.agda
lib/prim/Agda/Builtin/Reflection.agda
lib/prim/Agda/Builtin/Reflection/External.agda
lib/prim/Agda/Builtin/Reflection/Properties.agda
lib/prim/Agda/Builtin/Sigma.agda
lib/prim/Agda/Builtin/Size.agda
lib/prim/Agda/Builtin/Strict.agda
lib/prim/Agda/Builtin/String.agda
lib/prim/Agda/Builtin/String/Properties.agda
lib/prim/Agda/Builtin/TrustMe.agda
lib/prim/Agda/Builtin/Unit.agda
lib/prim/Agda/Builtin/Word.agda
lib/prim/Agda/Builtin/Word/Properties.agda
lib/prim/Agda/Primitive.agda
lib/prim/Agda/Primitive/Cubical.agda
MAlonzo/src/MAlonzo/RTE.hs
MAlonzo/src/MAlonzo/RTE/Float.hs
source-repository head
type: git
location: https://github.com/agda/agda.git
source-repository this
type: git
location: https://github.com/agda/agda.git
tag: v2.8.0
-- Build flags
---------------------------------------------------------------------------
flag dump-core
default: False
manual: True
description: Write GHC core output.
flag debug
default: False
manual: True
description:
Enable debug printing. This makes Agda slightly slower, and
building Agda slower as well. The --verbose=N option only
has an effect when Agda was built with this flag.
flag debug-serialisation
default: False
manual: True
description:
Enable debug mode in serialisation. This makes serialisation slower.
flag debug-parsing
default: False
manual: True
description:
Enable debug mode in parsing. This makes parsing slower.
flag enable-cluster-counting
default: False
manual: True
description:
Enable the --count-clusters flag. (If enable-cluster-counting is
False, then the --count-clusters flag triggers an error message.)
flag optimise-heavily
default: True
manual: True
description:
Enable some expensive optimisations when compiling Agda.
flag use-xdg-data-home
default: False
manual: True
description:
Install data files under $XDG_DATA_HOME\/agda\/$AGDA_VERSION by default
instead of the installation location defined by Cabal.
This should not be enabled in declarative build environments like Nix or Guix.
-- Common stanzas
---------------------------------------------------------------------------
common language
if flag(optimise-heavily)
cpp-options:
-DOPTIMISE_HEAVILY
ghc-options:
-fexpose-all-unfoldings
-fspecialise-aggressively
if flag(use-xdg-data-home)
cpp-options:
-DUSE_XDG_DATA_HOME
if flag(dump-core)
ghc-options:
-dsuppress-coercions -ddump-simpl -dsuppress-idinfo
-dsuppress-type-applications -dsuppress-uniques
-dsuppress-module-prefixes -ddump-to-file
ghc-options:
-- ASR (2022-05-31). Workaround to Issue #5932.
-Wwarn
-Wwarn=cpp-undef
-Wwarn=deprecated-flags
-Wwarn=deriving-typeable
-Wwarn=dodgy-exports
-Wwarn=dodgy-foreign-imports
-Wwarn=dodgy-imports
-Wwarn=duplicate-exports
-Wwarn=empty-enumerations
-Wwarn=identities
-Wwarn=inaccessible-code
-Wwarn=inline-rule-shadowing
-Wwarn=missed-extra-shared-lib
-Wwarn=missing-fields
-Wwarn=missing-home-modules
-Wwarn=missing-methods
-Wwarn=missing-pattern-synonym-signatures
-Wwarn=missing-signatures
-Wwarn=noncanonical-monad-instances
-Wwarn=noncanonical-monoid-instances
-Wwarn=overflowed-literals
-Wwarn=overlapping-patterns
-- -Wwarn=redundant-constraints
-Wwarn=simplifiable-class-constraints
-Wwarn=star-binder
-Wwarn=star-is-type
-Wwarn=tabs
-Wwarn=typed-holes
-Wwarn=unbanged-strict-patterns
-Wwarn=unrecognised-pragmas
-Wwarn=unrecognised-warning-flags
-Wwarn=unticked-promoted-constructors
-Wwarn=unused-do-bind
-Wwarn=unused-foralls
-Wwarn=warnings-deprecations
-Wwarn=wrong-do-bind
-- The following warning is an error in GHC >= 8.10.
if impl(ghc < 8.10)
ghc-options:
-Wwarn=implicit-kind-vars
-- #6623: Turn off this (nameless) warning:
-- "Pattern match checker exceeded (2000000) iterations in a case alternative."
-- See: https://gitlab.haskell.org/ghc/ghc/-/issues/13464
-Wno-incomplete-patterns
-Wno-overlapping-patterns
if impl(ghc < 9.10)
ghc-options:
-Wwarn=semigroup
-- The semigroup warning is deprecated in GHC 9.10
if impl(ghc >= 8.10)
ghc-options:
-Wwarn=deriving-defaults
-Wwarn=redundant-record-wildcards
-Wwarn=unused-packages
-Wwarn=unused-record-wildcards
if impl(ghc >= 9.0)
ghc-options:
-Wwarn=invalid-haddock
-- #6137: coverage checker works only sufficiently well from GHC 9.0
-Wwarn=incomplete-patterns
-Wwarn=incomplete-record-updates
-Wwarn=overlapping-patterns
-- ASR (2022-04-27). This warning was added in GHC 9.0.2, removed
-- from 9.2.1 and added back in 9.2.2.
if impl(ghc == 9.0.2 || >= 9.2.2)
ghc-options:
-Wwarn=unicode-bidirectional-format-characters
if impl(ghc >= 9.2)
ghc-options:
-Wwarn=operator-whitespace
-Wwarn=redundant-bang-patterns
if impl(ghc >= 9.4)
ghc-options:
-Wwarn=type-equality-out-of-scope
if impl(ghc >= 9.4 && < 9.10)
ghc-options:
-Wwarn=forall-identifier
-- The forall-identifier warning is deprecated in GHC 9.10
default-language: Haskell2010
-- NOTE: If adding or removing default extensions, also change:
-- .hlint.yaml
default-extensions:
BangPatterns
BlockArguments
ConstraintKinds
--L-T Chen (2019-07-15):
-- Enabling DataKinds only locally makes the compile time
-- slightly shorter, see PR #3920.
-- DataKinds
DefaultSignatures
DeriveFoldable
DeriveFunctor
DeriveGeneric
DeriveTraversable
DerivingStrategies
DerivingVia
ExistentialQuantification
FlexibleContexts
FlexibleInstances
FunctionalDependencies
GADTs
GeneralizedNewtypeDeriving
InstanceSigs
LambdaCase
MultiParamTypeClasses
MultiWayIf
NamedFieldPuns
OverloadedStrings
PatternSynonyms
RankNTypes
RecordWildCards
ScopedTypeVariables
StandaloneDeriving
TupleSections
TypeFamilies
TypeOperators
TypeSynonymInstances
ViewPatterns
TypeApplications
other-extensions:
AllowAmbiguousTypes
ApplicativeDo
CPP
DataKinds
DeriveAnyClass
ImplicitParams
KindSignatures
MagicHash
NondecreasingIndentation
OverloadedLists
PartialTypeSignatures
PatternGuards
PolyKinds
RebindableSyntax
TemplateHaskell
UnboxedTuples
UndecidableInstances
-- Agda library
---------------------------------------------------------------------------
library
import: language
hs-source-dirs: src/full src/setup
-- Andreas, 2021-03-10:
-- All packages we depend upon should be mentioned in an unconditional
-- build-depends field, but additional restrictions on their
-- version for specific GHCs may be placed in conditionals.
--
-- The goal is to be able to make (e.g. when a new GHC comes out)
-- revisions on hackage, e.g. relaxing upper bounds. This process
-- currently does not support revising conditionals.
--
-- An exceptions are packages that are only needed for certain configurations,
-- like for flags, Windows, etc.
if flag(debug)
cpp-options: -DDEBUG
if flag(debug-serialisation)
cpp-options: -DDEBUG_SERIALISATION
if flag(debug-parsing)
cpp-options: -DDEBUG_PARSING
if flag(enable-cluster-counting)
cpp-options: -DCOUNT_CLUSTERS
build-depends:
text-icu >= 0.7.1.0 && < 0.9
if os(windows)
build-depends:
Win32 >= 2.6.1.0 && < 2.15
-- We need instance TH.Lift ByteString in Agda.Setup.
-- bytestring-0.11.2.0 adds "Lift instances for all flavors of ByteString"
-- GHC 9.2 comes with bytestring-0.11.4.0
-- Older GHCs can get the instance from th-lift-instances.
if impl(ghc < 9.2)
build-depends:
th-lift-instances >= 0.1.18 && < 0.1.21
-- For libraries that come with GHC, we take the shipped version as default lower bound.
-- For the other libraries, we take the lower bound from the oldest LTS we support.
-- This is currently LTS 16.31 (last for GHC 8.8.4).
build-depends:
-- Please keep in alphabetical order!
, aeson >= 1.4.7.1 && < 2.3
, ansi-terminal >= 0.10.3 && < 1.2
, array >= 0.5.4.0 && < 0.6
, async >= 2.2.2 && < 2.3
, base >= 4.13.0.0 && < 4.22
, binary >= 0.8.7.0 && < 0.9
, blaze-html >= 0.9.1.2 && < 0.10
, boxes >= 0.1.5 && < 0.2
, bytestring >= 0.10.10.1 && < 0.13
, case-insensitive >= 1.2.1.0 && < 1.3
, containers >= 0.6.2.1 && < 0.8
-- containers-0.6.3.1 adds IntSet.mapMonotonic, but its too young for GHC 8.8
, data-hash >= 0.2.0.1 && < 0.3
, deepseq >= 1.4.4.0 && < 1.6
, directory >= 1.3.6.0 && < 1.4
, dlist >= 0.8.0.8 && < 1.1
, edit-distance >= 0.2.2.1 && < 0.3
, enummapset >= 0.6.0.3 && < 0.8
, equivalence >= 0.3.5 && < 0.5
, exceptions >= 0.10.4 && < 0.11
, filelock >= 0.1.1.5 && < 0.2
, filepath >= 1.4.2.1 && < 1.6
, filemanip >= 0.3.6.3 && < 0.4
, generic-data >= 0.9.2.0 && < 1.2
-- generic-data-0.9.2.0 adds instance of Bounded for FiniteEnumeration
, ghc-compact == 0.1.*
, gitrev >= 1.3.1 && < 2
, hashable >= 1.3.0.0 && < 1.6
, haskeline >= 0.7.5.0 && < 0.9
, monad-control >= 1.0.2.3 && < 1.1
, mtl >= 2.2.2 && < 2.4
, murmur-hash >= 0.1.0.9 && < 0.2
, nonempty-containers >= 0.3.4.1 && < 0.4
, parallel >= 3.2.2.0 && < 3.3
, peano >= 0.1.0.1 && < 0.2
, pqueue >= 1.4.1.3 && < 1.6
, pretty >= 1.1.3.6 && < 1.2
, process >= 1.6.9.0 && < 1.7
, process-extras >= 0.7.4 && < 0.8
, regex-tdfa >= 1.3.1.0 && < 1.4
, split >= 0.2.3.4 && < 0.3
, stm >= 2.5.0.0 && < 2.6
, STMonadTrans >= 0.4.5 && < 0.5
, strict >= 0.4.0.1 && < 0.6
-- module Data.Strict.Classes entered in strict-0.4
, template-haskell >= 2.15.0.0 && < 2.24
, text >= 1.2.4.0 && < 2.2
, time >= 1.9.3 && < 1.15
, transformers >= 0.5.6.2 && < 0.7
, unordered-containers >= 0.2.10.0 && < 0.3
, uri-encode >= 1.5.0.7 && < 1.6
, vector >= 0.12.1.2 && < 0.14
, vector-hashtables >= 0.1.1.1 && < 0.2
, zlib >= 0.6.2.2 && < 0.8
-- We don't write upper bounds for Alex nor Happy because the
-- `build-tool-depends` field can not be modified in Hackage.
build-tool-depends:
, alex:alex >= 3.2.5
-- alex-3.2.5 contains fixes for building with GHC 8.8
, happy:happy >= 1.19.12
-- happy-1.19.12 contains fixes for building with GHC 8.8
exposed-modules:
Agda.Benchmarking
Agda.Compiler.Backend
Agda.Compiler.Backend.Base
Agda.Compiler.Builtin
Agda.Compiler.CallCompiler
Agda.Compiler.Common
Agda.Compiler.JS.Compiler
Agda.Compiler.JS.Syntax
Agda.Compiler.JS.Substitution
Agda.Compiler.JS.Pretty
Agda.Compiler.MAlonzo.Coerce
Agda.Compiler.MAlonzo.Compiler
Agda.Compiler.MAlonzo.Encode
Agda.Compiler.MAlonzo.HaskellTypes
Agda.Compiler.MAlonzo.Misc
Agda.Compiler.MAlonzo.Pragmas
Agda.Compiler.MAlonzo.Pretty
Agda.Compiler.MAlonzo.Primitives
Agda.Compiler.MAlonzo.Strict
Agda.Compiler.ToTreeless
Agda.Compiler.Treeless.AsPatterns
Agda.Compiler.Treeless.Builtin
Agda.Compiler.Treeless.Compare
Agda.Compiler.Treeless.EliminateDefaults
Agda.Compiler.Treeless.EliminateLiteralPatterns
Agda.Compiler.Treeless.Erase
Agda.Compiler.Treeless.GuardsToPrims
Agda.Compiler.Treeless.Identity
Agda.Compiler.Treeless.NormalizeNames
Agda.Compiler.Treeless.Pretty
Agda.Compiler.Treeless.Simplify
Agda.Compiler.Treeless.Subst
Agda.Compiler.Treeless.Uncase
Agda.Compiler.Treeless.Unused
Agda.ImpossibleTest
Agda.Interaction.AgdaTop
Agda.Interaction.Base
Agda.Interaction.BasicOps
Agda.Interaction.BuildLibrary
Agda.Interaction.Command
Agda.Interaction.SearchAbout
Agda.Interaction.CommandLine
Agda.Interaction.EmacsCommand
Agda.Interaction.EmacsTop
Agda.Interaction.ExitCode
Agda.Interaction.JSONTop
Agda.Interaction.JSON
Agda.Interaction.FindFile
Agda.Interaction.Highlighting.Common
Agda.Interaction.Highlighting.Dot
Agda.Interaction.Highlighting.Dot.Backend
Agda.Interaction.Highlighting.Dot.Base
Agda.Interaction.Highlighting.Emacs
Agda.Interaction.Highlighting.FromAbstract
Agda.Interaction.Highlighting.Generate
Agda.Interaction.Highlighting.HTML
Agda.Interaction.Highlighting.HTML.Backend
Agda.Interaction.Highlighting.HTML.Base
Agda.Interaction.Highlighting.JSON
Agda.Interaction.Highlighting.Precise
Agda.Interaction.Highlighting.Range
Agda.Interaction.Highlighting.Vim
Agda.Interaction.Highlighting.LaTeX
Agda.Interaction.Highlighting.LaTeX.Backend
Agda.Interaction.Highlighting.LaTeX.Base
Agda.Interaction.Imports
Agda.Interaction.InteractionTop
Agda.Interaction.Output
Agda.Interaction.Response
Agda.Interaction.Response.Base
Agda.Interaction.MakeCase
Agda.Interaction.Monad
Agda.Interaction.Library
Agda.Interaction.Library.Base
Agda.Interaction.Library.Parse
Agda.Interaction.Options
Agda.Interaction.Options.Errors
Agda.Interaction.Options.Help
Agda.Interaction.Options.Lenses
Agda.Interaction.Options.Warnings
Agda.Main
Agda.Mimer.Mimer
Agda.Mimer.Options
Agda.Setup
Agda.Setup.DataFiles
Agda.Setup.EmacsMode
Agda.Syntax.Abstract.Name
Agda.Syntax.Abstract.Pattern
Agda.Syntax.Abstract.PatternSynonyms
Agda.Syntax.Abstract.Pretty
Agda.Syntax.Abstract.UsedNames
Agda.Syntax.Abstract.Views
Agda.Syntax.Abstract
Agda.Syntax.Builtin
Agda.Syntax.Common
Agda.Syntax.Common.Aspect
Agda.Syntax.Common.KeywordRange
Agda.Syntax.Common.Pretty
Agda.Syntax.Common.Pretty.ANSI
Agda.Syntax.Concrete.Attribute
Agda.Syntax.Concrete.Definitions
Agda.Syntax.Concrete.Definitions.Errors
Agda.Syntax.Concrete.Definitions.Monad
Agda.Syntax.Concrete.Definitions.Types
Agda.Syntax.Concrete.Fixity
Agda.Syntax.Concrete.Generic
Agda.Syntax.Concrete.Glyph
Agda.Syntax.Concrete.Name
Agda.Syntax.Concrete.Operators.Parser
Agda.Syntax.Concrete.Operators.Parser.Monad
Agda.Syntax.Concrete.Operators
Agda.Syntax.Concrete.Pattern
Agda.Syntax.Concrete.Pretty
Agda.Syntax.Concrete
Agda.Syntax.DoNotation
Agda.Syntax.Fixity
Agda.Syntax.IdiomBrackets
Agda.Syntax.Info
Agda.Syntax.Internal
Agda.Syntax.Internal.Blockers
Agda.Syntax.Internal.Defs
Agda.Syntax.Internal.Elim
Agda.Syntax.Internal.Generic
Agda.Syntax.Internal.MetaVars
Agda.Syntax.Internal.Names
Agda.Syntax.Internal.Pattern
Agda.Syntax.Internal.SanityCheck
Agda.Syntax.Internal.Univ
Agda.Syntax.Literal
Agda.Syntax.Notation
Agda.Syntax.Parser.Alex
Agda.Syntax.Parser.Comments
Agda.Syntax.Parser.Helpers
Agda.Syntax.Parser.Layout
Agda.Syntax.Parser.LexActions
Agda.Syntax.Parser.Lexer
Agda.Syntax.Parser.Literate
Agda.Syntax.Parser.LookAhead
Agda.Syntax.Parser.Monad
Agda.Syntax.Parser.Parser
Agda.Syntax.Parser.StringLiterals
Agda.Syntax.Parser.Tokens
Agda.Syntax.Parser
Agda.Syntax.Position
Agda.Syntax.Reflected
Agda.Syntax.Scope.Base
Agda.Syntax.Scope.Flat
Agda.Syntax.Scope.Monad
Agda.Syntax.TopLevelModuleName
Agda.Syntax.TopLevelModuleName.Boot
Agda.Syntax.Translation.AbstractToConcrete
Agda.Syntax.Translation.ConcreteToAbstract
Agda.Syntax.Translation.InternalToAbstract
Agda.Syntax.Translation.ReflectedToAbstract
Agda.Syntax.Treeless
Agda.Termination.CallGraph
Agda.Termination.CallMatrix
Agda.Termination.CutOff
Agda.Termination.Monad
Agda.Termination.Order
Agda.Termination.RecCheck
Agda.Termination.SparseMatrix
Agda.Termination.Semiring
Agda.Termination.TermCheck
Agda.Termination.Termination
Agda.TheTypeChecker
Agda.TypeChecking.Abstract
Agda.TypeChecking.CheckInternal
Agda.TypeChecking.CompiledClause
Agda.TypeChecking.CompiledClause.Compile
Agda.TypeChecking.CompiledClause.Match
Agda.TypeChecking.Constraints
Agda.TypeChecking.Conversion
Agda.TypeChecking.Conversion.Pure
Agda.TypeChecking.Coverage
Agda.TypeChecking.Coverage.Match
Agda.TypeChecking.Coverage.SplitTree
Agda.TypeChecking.Coverage.SplitClause
Agda.TypeChecking.Coverage.Cubical
Agda.TypeChecking.Datatypes
Agda.TypeChecking.DeadCode
Agda.TypeChecking.DisplayForm
Agda.TypeChecking.DropArgs
Agda.TypeChecking.DiscrimTree
Agda.TypeChecking.DiscrimTree.Types
Agda.TypeChecking.Empty
Agda.TypeChecking.EtaContract
Agda.TypeChecking.Errors
Agda.TypeChecking.Errors.Names
Agda.TypeChecking.Free
Agda.TypeChecking.Free.Lazy
Agda.TypeChecking.Free.Precompute
Agda.TypeChecking.Free.Reduce
Agda.TypeChecking.Forcing
Agda.TypeChecking.Functions
Agda.TypeChecking.Generalize
Agda.TypeChecking.IApplyConfluence
Agda.TypeChecking.Implicit
Agda.TypeChecking.Injectivity
Agda.TypeChecking.Inlining
Agda.TypeChecking.InstanceArguments
Agda.TypeChecking.Irrelevance
Agda.TypeChecking.Level
Agda.TypeChecking.LevelConstraints
Agda.TypeChecking.Lock
Agda.TypeChecking.Level.Solve
Agda.TypeChecking.MetaVars
Agda.TypeChecking.MetaVars.Mention
Agda.TypeChecking.MetaVars.Occurs
Agda.TypeChecking.Modalities
Agda.TypeChecking.Monad.Base
Agda.TypeChecking.Monad.Base.Types
Agda.TypeChecking.Monad.Base.Warning
Agda.TypeChecking.Monad.Benchmark
Agda.TypeChecking.Monad.Builtin
Agda.TypeChecking.Monad.Caching
Agda.TypeChecking.Monad.Closure
Agda.TypeChecking.Monad.Constraints
Agda.TypeChecking.Monad.Context
Agda.TypeChecking.Monad.Debug
Agda.TypeChecking.Monad.Env
Agda.TypeChecking.Monad.Imports
Agda.TypeChecking.Monad.MetaVars
Agda.TypeChecking.Monad.Modality
Agda.TypeChecking.Monad.Mutual
Agda.TypeChecking.Monad.Open
Agda.TypeChecking.Monad.Options
Agda.TypeChecking.Monad.Pure
Agda.TypeChecking.Monad.Signature
Agda.TypeChecking.Monad.SizedTypes
Agda.TypeChecking.Monad.State
Agda.TypeChecking.Monad.Statistics
Agda.TypeChecking.Monad.Trace
Agda.TypeChecking.Monad
Agda.TypeChecking.Names
Agda.TypeChecking.Opacity
Agda.TypeChecking.Patterns.Abstract
Agda.TypeChecking.Patterns.Internal
Agda.TypeChecking.Patterns.Match
Agda.TypeChecking.Polarity
Agda.TypeChecking.Positivity
Agda.TypeChecking.Positivity.Occurrence
Agda.TypeChecking.Pretty
Agda.TypeChecking.Pretty.Call
Agda.TypeChecking.Pretty.Constraint
Agda.TypeChecking.Pretty.Warning
Agda.TypeChecking.Primitive
Agda.TypeChecking.Primitive.Base
Agda.TypeChecking.Primitive.Cubical
Agda.TypeChecking.Primitive.Cubical.Glue
Agda.TypeChecking.Primitive.Cubical.Base
Agda.TypeChecking.Primitive.Cubical.HCompU
Agda.TypeChecking.ProjectionLike
Agda.TypeChecking.Quote
Agda.TypeChecking.ReconstructParameters
Agda.TypeChecking.RecordPatterns
Agda.TypeChecking.Records
Agda.TypeChecking.Reduce
Agda.TypeChecking.Reduce.Fast
Agda.TypeChecking.Reduce.Monad
Agda.TypeChecking.Rewriting
Agda.TypeChecking.Rewriting.Clause
Agda.TypeChecking.Rewriting.Confluence
Agda.TypeChecking.Rewriting.NonLinMatch
Agda.TypeChecking.Rewriting.NonLinPattern
Agda.TypeChecking.Rules.Application
Agda.TypeChecking.Rules.Builtin
Agda.TypeChecking.Rules.Builtin.Coinduction
Agda.TypeChecking.Rules.Data
Agda.TypeChecking.Rules.Decl
Agda.TypeChecking.Rules.Def
Agda.TypeChecking.Rules.Display
Agda.TypeChecking.Rules.LHS
Agda.TypeChecking.Rules.LHS.Implicit
Agda.TypeChecking.Rules.LHS.Problem
Agda.TypeChecking.Rules.LHS.ProblemRest
Agda.TypeChecking.Rules.LHS.Unify
Agda.TypeChecking.Rules.LHS.Unify.Types
Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
Agda.TypeChecking.Rules.Record
Agda.TypeChecking.Rules.Term
Agda.TypeChecking.Serialise
Agda.TypeChecking.Serialise.Base
Agda.TypeChecking.Serialise.Instances
Agda.TypeChecking.Serialise.Instances.Abstract
Agda.TypeChecking.Serialise.Instances.Common
Agda.TypeChecking.Serialise.Instances.Compilers
Agda.TypeChecking.Serialise.Instances.Highlighting
Agda.TypeChecking.Serialise.Instances.Internal
Agda.TypeChecking.Serialise.Instances.Errors
Agda.TypeChecking.SizedTypes
Agda.TypeChecking.SizedTypes.Pretty
Agda.TypeChecking.SizedTypes.Solve
Agda.TypeChecking.SizedTypes.Syntax
Agda.TypeChecking.SizedTypes.Utils
Agda.TypeChecking.SizedTypes.WarshallSolver
Agda.TypeChecking.Sort
Agda.TypeChecking.Substitute
Agda.TypeChecking.Substitute.Class
Agda.TypeChecking.Substitute.DeBruijn
Agda.TypeChecking.SyntacticEquality
Agda.TypeChecking.Telescope
Agda.TypeChecking.Telescope.Path
Agda.TypeChecking.Unquote
Agda.TypeChecking.Warnings
Agda.TypeChecking.With
Agda.Utils.AffineHole
Agda.Utils.Applicative
Agda.Utils.AssocList
Agda.Utils.Bag
Agda.Utils.Benchmark
Agda.Utils.BiMap
Agda.Utils.Boolean
Agda.Utils.BoolSet
Agda.Utils.CallStack
Agda.Utils.Char
Agda.Utils.Cluster
Agda.Utils.Empty
Agda.Utils.Environment
Agda.Utils.Either
Agda.Utils.Fail
Agda.Utils.Favorites
Agda.Utils.FileName
Agda.Utils.FileId
Agda.Utils.Float
Agda.Utils.Functor
Agda.Utils.Function
Agda.Utils.GetOpt
Agda.Utils.Graph.AdjacencyMap.Unidirectional
Agda.Utils.Graph.TopSort
Agda.Utils.Hash
Agda.Utils.HashTable
Agda.Utils.Haskell.Syntax
Agda.Utils.IArray
Agda.Utils.Impossible
Agda.Utils.IndexedList
Agda.Utils.IntSet.Infinite
Agda.Utils.IO
Agda.Utils.IO.Binary
Agda.Utils.IO.Directory
Agda.Utils.IO.TempFile
Agda.Utils.IO.UTF8
Agda.Utils.IORef
Agda.Utils.Lens
Agda.Utils.Lens.Examples
Agda.Utils.List
Agda.Utils.List1
Agda.Utils.List2
Agda.Utils.ListT
Agda.Utils.Map
Agda.Utils.Map1
Agda.Utils.Maybe
Agda.Utils.Maybe.Strict
Agda.Utils.Memo
Agda.Utils.Monad
Agda.Utils.Monoid
Agda.Utils.Null
Agda.Utils.Parser.MemoisedCPS
Agda.Utils.PartialOrd
Agda.Utils.Permutation
Agda.Utils.POMonoid
Agda.Utils.ProfileOptions
Agda.Utils.RangeMap
Agda.Utils.SemiRing
Agda.Utils.Semigroup
Agda.Utils.Set1
Agda.Utils.Singleton
Agda.Utils.Size
Agda.Utils.SmallSet
Agda.Utils.String
Agda.Utils.Suffix
Agda.Utils.Three
Agda.Utils.Time
Agda.Utils.Trie
Agda.Utils.Tuple
Agda.Utils.TypeLevel
Agda.Utils.TypeLits
Agda.Utils.Unsafe
Agda.Utils.Update
Agda.Utils.VarSet
Agda.Utils.WithDefault
Agda.Utils.Zipper
Agda.Version
Agda.VersionCommit
autogen-modules:
Paths_Agda
other-modules:
Paths_Agda
-- Need not export submodules if parent module reexports them.
Agda.Interaction.Options.Base
Agda.Interaction.Options.HasOptions
Agda.Interaction.Options.Types
Agda.Utils.CallStack.Base
Agda.Utils.CallStack.Pretty
-- Agda binary
---------------------------------------------------------------------------
executable agda
hs-source-dirs: src/main
main-is: Main.hs
build-depends:
, Agda
-- Nothing is used from the following package,
-- except for the Prelude.
, base
default-language: Haskell2010
-- If someone installs Agda with the setuid bit set, then the
-- presence of +RTS may be a security problem (see GHC bug #3910).
-- However, we sometimes recommend people to use +RTS to control
-- Agda's memory usage, so we want this functionality enabled by
-- default.
-- The threaded RTS by default starts a major GC after a program has
-- been idle for 0.3 s. This feature turned out to be annoying, so
-- the idle GC is now by default turned off (-I0).
ghc-options:
-threaded
-rtsopts
-with-rtsopts=-I0
-- agda-mode executable
---------------------------------------------------------------------------
executable agda-mode
import: language
hs-source-dirs: src/agda-mode src/setup
main-is: Main.hs
autogen-modules:
Paths_Agda
other-modules:
Paths_Agda
Agda.Setup
Agda.Setup.DataFiles
Agda.Setup.EmacsMode
Agda.Version
Agda.VersionCommit
-- We need instance TH.Lift ByteString in Agda.Setup.
-- bytestring-0.11.2.0 adds "Lift instances for all flavors of ByteString"
-- GHC 9.2 comes with bytestring-0.11.4.0
-- Older GHCs can get the instance from th-lift-instances.
if impl(ghc < 9.2)
build-depends:
th-lift-instances >= 0.1.18 && < 0.1.21
build-depends:
, base >= 4.13.0.0 && < 4.22
, bytestring >= 0.10.10.1 && < 0.13
, directory >= 1.3.6.0 && < 1.4
, filelock >= 0.1.1.5 && < 0.2
, filepath >= 1.4.2.1 && < 1.6
, gitrev >= 1.3.1 && < 2
, process >= 1.6.9.0 && < 1.7
, template-haskell >= 2.15.0.0 && < 2.24