Cabal revisions of Agda-2.7.0.1
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.7.0.1-build-type: Custom-license: MIT-license-file: LICENSE-copyright: (c) 2005-2024 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.10.1- GHC == 9.8.2- GHC == 9.6.6- GHC == 9.4.8- GHC == 9.2.8- GHC == 9.0.2- GHC == 8.10.7- GHC == 8.8.4- GHC == 8.6.5--extra-doc-files:- CHANGELOG.md- README.md- doc/user-manual/agda.svg- 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.10.1.yaml- stack-9.8.2.yaml- stack-9.6.6.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--data-dir:- src/data--data-files:- emacs-mode/*.el- html/Agda.css- html/highlight-hover.js- 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/Id.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/*.hs- MAlonzo/src/MAlonzo/RTE/*.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.0.1---- Build flags------------------------------------------------------------------------------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.---- Setup------------------------------------------------------------------------------custom-setup- setup-depends:- , base >= 4.12.0.0 && < 4.21- , Cabal >= 2.4.0.1 && < 3.13- , directory >= 1.3.3.0 && < 1.4- , filepath >= 1.4.2.1 && < 1.6- , process >= 1.6.3.0 && < 1.7---- Common stanzas------------------------------------------------------------------------------common language-- if flag(optimise-heavily)- cpp-options:- -DOPTIMISE_HEAVILY- ghc-options:- -fexpose-all-unfoldings- -fspecialise-aggressively-- 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=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.8)- ghc-options:- -Wwarn=missed-extra-shared-lib-- if impl(ghc >= 8.10)- ghc-options:- -Wwarn=compat-unqualified-imports- -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- ExistentialQuantification- FlexibleContexts- FlexibleInstances- FunctionalDependencies- GADTs- GeneralizedNewtypeDeriving- InstanceSigs- LambdaCase- MultiParamTypeClasses- MultiWayIf- NamedFieldPuns- OverloadedStrings- PatternSynonyms- RankNTypes- RecordWildCards- ScopedTypeVariables- StandaloneDeriving- TupleSections- TypeFamilies- TypeOperators- TypeSynonymInstances- ViewPatterns-- other-extensions:- CPP- DeriveAnyClass- PartialTypeSignatures----- Agda library------------------------------------------------------------------------------library- import: language-- hs-source-dirs: src/full-- -- 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-- if os(windows)- build-depends: Win32 >= 2.6.1.0 && < 2.15-- -- Agda cannot be built with GHC 8.6.1 due to a compiler bug, see- -- Agda Issue #3344.- if impl(ghc == 8.6.1)- buildable: False-- -- Agda cannot be built with Windows and GHC 8.6.3 due to a compiler- -- bug, see Agda Issue #3657.- if os(windows) && impl(ghc == 8.6.3)- buildable: False-- -- For libraries that come with GHC, we take the shipped version as default lower bound.- build-depends:- -- Please keep in alphabetical order!- , aeson >= 1.1.2.0 && < 2.3- , ansi-terminal >= 0.9 && < 1.2- , array >= 0.5.2.0 && < 0.6- , async >= 2.2 && < 2.3- , base >= 4.12.0.0 && < 4.21- , binary >= 0.8.6.0 && < 0.9- , blaze-html >= 0.8 && < 0.10- , boxes >= 0.1.3 && < 0.2- , bytestring >= 0.10.8.2 && < 0.13- , case-insensitive >= 1.2.0.4 && < 1.3- , containers >= 0.6.0.1 && < 0.8- , data-hash >= 0.2.0.0 && < 0.3- , deepseq >= 1.4.4.0 && < 1.6- , directory >= 1.3.3.0 && < 1.4- , dlist >= 0.8 && < 1.1- , edit-distance >= 0.2.1.2 && < 0.3- , equivalence >= 0.3.2 && < 0.5- -- exceptions-0.8 instead of 0.10 because of stack- , exceptions >= 0.8 && < 0.11- , filepath >= 1.4.2.1 && < 1.6- , ghc-compact == 0.1.*- , gitrev >= 1.3.1 && < 2- -- hashable 1.2.0.10 makes library-test 10x- -- slower. The issue was fixed in hashable 1.2.1.0.- -- https://github.com/tibbe/hashable/issues/57.- , hashable >= 1.2.1.0 && < 1.6- , haskeline >= 0.7.4.3 && < 0.9- -- monad-control-1.0.1.0 is the first to contain liftThrough- , monad-control >= 1.0.1.0 && < 1.1- , mtl >= 2.2.2 && < 2.4- , murmur-hash >= 0.1 && < 0.2- , parallel >= 3.2.2.0 && < 3.3- , peano >= 0.1.0.1 && < 0.2- , pqueue >= 1.4.1.2 && < 1.6- , pretty >= 1.1.3.3 && < 1.2- , process >= 1.6.3.0 && < 1.7- , regex-tdfa >= 1.3.1.0 && < 1.4- , split >= 0.2.0.0 && < 0.3- , stm >= 2.4.4 && < 2.6- , STMonadTrans >= 0.4.3 && < 0.5- , strict >= 0.4.0.1 && < 0.6- , text >= 1.2.3.1 && < 2.2- , time >= 1.9.2 && < 1.15- , transformers >= 0.5.5.0 && < 0.7- , unordered-containers >= 0.2.9.0 && < 0.3- -- unordered-containers < 0.2.9 need base < 4.11- , uri-encode >= 1.5.0.4 && < 1.6- , vector >= 0.12 && < 0.14- , vector-hashtables >= 0.1.1.1 && < 0.2- , zlib >= 0.6 && < 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.3- -- alex-3.2.3 is packaged with Ubuntu 18.04- , happy:happy >= 1.19.8- -- happy-1.19.8 is packaged with Ubuntu 18.04-- 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.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.Help- Agda.Interaction.Options.Lenses- Agda.Interaction.Options.Warnings- Agda.Main- Agda.Mimer.Mimer- Agda.Mimer.Options- 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.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.Id- 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.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.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.Pointer- Agda.Utils.POMonoid- Agda.Utils.ProfileOptions- Agda.Utils.RangeMap- Agda.Utils.SemiRing- Agda.Utils.Semigroup- 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.Warshall- 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.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- hs-source-dirs: src/agda-mode- main-is: Main.hs- autogen-modules: Paths_Agda- other-modules: Paths_Agda- build-depends:- , base >= 4.12.0.0 && < 4.21- , directory >= 1.3.3.0 && < 1.4- , filepath >= 1.4.2.1 && < 1.6- , process >= 1.6.3.0 && < 1.7- default-language: Haskell2010+cabal-version: 2.4 +name: Agda +version: 2.7.0.1 +x-revision: 1 +build-type: Custom +license: MIT +license-file: LICENSE +copyright: (c) 2005-2024 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.10.1 + GHC == 9.8.2 + GHC == 9.6.6 + GHC == 9.4.8 + GHC == 9.2.8 + GHC == 9.0.2 + GHC == 8.10.7 + GHC == 8.8.4 + GHC == 8.6.5 + +extra-doc-files: + CHANGELOG.md + README.md + doc/user-manual/agda.svg + 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.10.1.yaml + stack-9.8.2.yaml + stack-9.6.6.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 + +data-dir: + src/data + +data-files: + emacs-mode/*.el + html/Agda.css + html/highlight-hover.js + 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/Id.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/*.hs + MAlonzo/src/MAlonzo/RTE/*.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.0.1 + +-- Build flags +--------------------------------------------------------------------------- + +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. + +-- Setup +--------------------------------------------------------------------------- + +custom-setup + setup-depends: + , base >= 4.12.0.0 && < 4.21 + , Cabal >= 2.4.0.1 && < 3.13 + , directory >= 1.3.3.0 && < 1.4 + , filepath >= 1.4.2.1 && < 1.6 + , process >= 1.6.3.0 && < 1.7 + +-- Common stanzas +--------------------------------------------------------------------------- + +common language + + if flag(optimise-heavily) + cpp-options: + -DOPTIMISE_HEAVILY + ghc-options: + -fexpose-all-unfoldings + -fspecialise-aggressively + + 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=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.8) + ghc-options: + -Wwarn=missed-extra-shared-lib + + if impl(ghc >= 8.10) + ghc-options: + -Wwarn=compat-unqualified-imports + -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 + ExistentialQuantification + FlexibleContexts + FlexibleInstances + FunctionalDependencies + GADTs + GeneralizedNewtypeDeriving + InstanceSigs + LambdaCase + MultiParamTypeClasses + MultiWayIf + NamedFieldPuns + OverloadedStrings + PatternSynonyms + RankNTypes + RecordWildCards + ScopedTypeVariables + StandaloneDeriving + TupleSections + TypeFamilies + TypeOperators + TypeSynonymInstances + ViewPatterns + + other-extensions: + CPP + DeriveAnyClass + PartialTypeSignatures + + +-- Agda library +--------------------------------------------------------------------------- + +library + import: language + + hs-source-dirs: src/full + + -- 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 + + if os(windows) + build-depends: Win32 >= 2.6.1.0 && < 2.15 + + -- Agda cannot be built with GHC 8.6.1 due to a compiler bug, see + -- Agda Issue #3344. + if impl(ghc == 8.6.1) + buildable: False + + -- Agda cannot be built with Windows and GHC 8.6.3 due to a compiler + -- bug, see Agda Issue #3657. + if os(windows) && impl(ghc == 8.6.3) + buildable: False + + -- For libraries that come with GHC, we take the shipped version as default lower bound. + build-depends: + -- Please keep in alphabetical order! + , aeson >= 1.1.2.0 && < 2.3 + , ansi-terminal >= 0.9 && < 1.2 + , array >= 0.5.2.0 && < 0.6 + , async >= 2.2 && < 2.3 + , base >= 4.12.0.0 && < 4.21 + , binary >= 0.8.6.0 && < 0.9 + , blaze-html >= 0.8 && < 0.10 + , boxes >= 0.1.3 && < 0.2 + , bytestring >= 0.10.8.2 && < 0.13 + , case-insensitive >= 1.2.0.4 && < 1.3 + , containers >= 0.6.0.1 && < 0.8 + , data-hash >= 0.2.0.0 && < 0.3 + , deepseq >= 1.4.4.0 && < 1.6 + , directory >= 1.3.3.0 && < 1.4 + , dlist >= 0.8 && < 1.1 + , edit-distance >= 0.2.1.2 && < 0.3 + , equivalence >= 0.3.2 && < 0.5 + -- exceptions-0.8 instead of 0.10 because of stack + , exceptions >= 0.8 && < 0.11 + , filepath >= 1.4.2.1 && < 1.6 + , ghc-compact == 0.1.* + , gitrev >= 1.3.1 && < 2 + -- hashable 1.2.0.10 makes library-test 10x + -- slower. The issue was fixed in hashable 1.2.1.0. + -- https://github.com/tibbe/hashable/issues/57. + , hashable >= 1.2.1.0 && < 1.6 + , haskeline >= 0.7.4.3 && < 0.9 + -- monad-control-1.0.1.0 is the first to contain liftThrough + , monad-control >= 1.0.1.0 && < 1.1 + , mtl >= 2.2.2 && < 2.4 + , murmur-hash >= 0.1 && < 0.2 + , parallel >= 3.2.2.0 && < 3.3 + , peano >= 0.1.0.1 && < 0.2 + , pqueue >= 1.4.1.2 && < 1.6 + , pretty >= 1.1.3.3 && < 1.2 + , process >= 1.6.3.0 && < 1.7 + , regex-tdfa >= 1.3.1.0 && < 1.4 + , split >= 0.2.0.0 && < 0.3 + , stm >= 2.4.4 && < 2.6 + , STMonadTrans >= 0.4.3 && < 0.5 + , strict >= 0.4.0.1 && < 0.6 + , text >= 1.2.3.1 && < 2.2 + , time >= 1.9.2 && < 1.15 + , transformers >= 0.5.5.0 && < 0.7 + , unordered-containers >= 0.2.9.0 && < 0.3 + -- unordered-containers < 0.2.9 need base < 4.11 + , uri-encode >= 1.5.0.4 && < 1.6 + , vector >= 0.12 && < 0.14 + , vector-hashtables >= 0.1.1.1 && < 0.2 + , zlib >= 0.6 && < 0.8 + + build-tool-depends: + , alex:alex >= 3.2.3 && < 4 + -- alex-3.2.3 is packaged with Ubuntu 18.04 + , happy:happy >= 1.19.8 && < 2.1.1 + -- happy-1.19.8 is packaged with Ubuntu 18.04 + -- Build failure with happy-2.1.1, issue #7585 + + 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.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.Help + Agda.Interaction.Options.Lenses + Agda.Interaction.Options.Warnings + Agda.Main + Agda.Mimer.Mimer + Agda.Mimer.Options + 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.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.Id + 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.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.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.Pointer + Agda.Utils.POMonoid + Agda.Utils.ProfileOptions + Agda.Utils.RangeMap + Agda.Utils.SemiRing + Agda.Utils.Semigroup + 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.Warshall + 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.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 + hs-source-dirs: src/agda-mode + main-is: Main.hs + autogen-modules: Paths_Agda + other-modules: Paths_Agda + build-depends: + , base >= 4.12.0.0 && < 4.21 + , directory >= 1.3.3.0 && < 1.4 + , filepath >= 1.4.2.1 && < 1.6 + , process >= 1.6.3.0 && < 1.7 + default-language: Haskell2010
revision 2
cabal-version: 2.4 name: Agda version: 2.7.0.1 -x-revision: 1 +x-revision: 2 build-type: Custom license: MIT license-file: LICENSE build-tool-depends: , alex:alex >= 3.2.3 && < 4 -- alex-3.2.3 is packaged with Ubuntu 18.04 - , happy:happy >= 1.19.8 && < 2.1.1 + , happy:happy >= 1.19.8 && < 2.1.1 || >= 2.1.2 && < 3 -- happy-1.19.8 is packaged with Ubuntu 18.04 -- Build failure with happy-2.1.1, issue #7585
revision 3
cabal-version: 2.4 name: Agda version: 2.7.0.1 -x-revision: 2 +x-revision: 3 build-type: Custom license: MIT license-file: LICENSE custom-setup setup-depends: - , base >= 4.12.0.0 && < 4.21 + , base >= 4.12.0.0 && < 4.22 , Cabal >= 2.4.0.1 && < 3.13 , directory >= 1.3.3.0 && < 1.4 , filepath >= 1.4.2.1 && < 1.6 , ansi-terminal >= 0.9 && < 1.2 , array >= 0.5.2.0 && < 0.6 , async >= 2.2 && < 2.3 - , base >= 4.12.0.0 && < 4.21 + , base >= 4.12.0.0 && < 4.22 , binary >= 0.8.6.0 && < 0.9 , blaze-html >= 0.8 && < 0.10 , boxes >= 0.1.3 && < 0.2 autogen-modules: Paths_Agda other-modules: Paths_Agda build-depends: - , base >= 4.12.0.0 && < 4.21 + , base >= 4.12.0.0 && < 4.22 , directory >= 1.3.3.0 && < 1.4 , filepath >= 1.4.2.1 && < 1.6 , process >= 1.6.3.0 && < 1.7