cabal-version: 2.4 name: Agda version: 2.7.20250510 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 Coq, Idris, Lean and NuPRL. . This package includes both a command-line program (agda) and an Emacs mode. If you want to use the Emacs mode you can set it up by running @agda-mode setup@ (see the README). 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! 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 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.7.20250510 -- 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: False manual: True description: Enable some expensive optimisations when compiling Agda. -- Common stanzas --------------------------------------------------------------------------- common language if flag(optimise-heavily) cpp-options: -DOPTIMISE_HEAVILY ghc-options: -fexpose-all-unfoldings -fspecialise-aggressively 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.Emacs Agda.Interaction.Highlighting.FromAbstract Agda.Interaction.Highlighting.Generate Agda.Interaction.Highlighting.HTML Agda.Interaction.Highlighting.JSON Agda.Interaction.Highlighting.Precise Agda.Interaction.Highlighting.Range Agda.Interaction.Highlighting.Vim Agda.Interaction.Highlighting.LaTeX 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.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.Highlighting.Dot.Backend Agda.Interaction.Highlighting.Dot.Base Agda.Interaction.Highlighting.HTML.Backend Agda.Interaction.Highlighting.HTML.Base Agda.Interaction.Highlighting.LaTeX.Backend Agda.Interaction.Highlighting.LaTeX.Base 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