Cabal revisions of Agda-2.8.0
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-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+cabal-version: 2.4 +name: Agda +version: 2.8.0 +x-revision: 1 +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.7 + , 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
revision 2
-cabal-version: 2.4 -name: Agda -version: 2.8.0 -x-revision: 1 -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.7 - , 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 +cabal-version: 2.4+name: Agda+version: 2.8.0+x-revision: 2+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.4+ , peano >= 0.1.0.1 && < 0.2+ , pqueue >= 1.4.1.3 && < 1.7+ , 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
revision 3
cabal-version: 2.4 name: Agda version: 2.8.0-x-revision: 2+x-revision: 3 build-type: Simple license: MIT license-file: LICENSE , nonempty-containers >= 0.3.4.1 && < 0.4 , parallel >= 3.2.2.0 && < 3.4 , peano >= 0.1.0.1 && < 0.2- , pqueue >= 1.4.1.3 && < 1.7+ , pqueue >= 1.4.1.3 && < 1.8 , pretty >= 1.1.3.6 && < 1.2 , process >= 1.6.9.0 && < 1.7 , process-extras >= 0.7.4 && < 0.8
revision 4
cabal-version: 2.4 name: Agda version: 2.8.0-x-revision: 3+x-revision: 4 build-type: Simple license: MIT license-file: LICENSE Emacs mode. tested-with:- GHC == 9.12.2- GHC == 9.10.2+ GHC == 9.12.4+ GHC == 9.10.3 GHC == 9.8.4 GHC == 9.6.7 GHC == 9.4.8 -- 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+ , aeson >= 1.4.7.1 && < 2.4 , ansi-terminal >= 0.10.3 && < 1.2 , array >= 0.5.4.0 && < 0.6 , async >= 2.2.2 && < 2.3