Cabal revisions of Agda-2.6.2.1
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-name: Agda-version: 2.6.2.1-cabal-version: >= 1.10-build-type: Custom-license: OtherLicense-license-file: LICENSE-copyright: (c) 2005-2021 The Agda Team.-author: Ulf Norell and The Agda Team, see https://agda.readthedocs.io/en/latest/team.html-maintainer: The Agda Team-homepage: http://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, Epigram 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).- .- Note that the Agda package does not follow the package versioning- policy, because it is not intended to be used by third-party- packages.--tested-with: GHC == 8.0.2- GHC == 8.2.2- GHC == 8.4.4- GHC == 8.6.5- GHC == 8.8.4- GHC == 8.10.7- GHC == 9.0.1- GHC == 9.2.1--extra-source-files: CHANGELOG.md- README.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--- Liang-Ting (2019-11-26): See Issues #4216--- doc/user-manual.pdf- stack-8.0.2.yaml- stack-8.2.2.yaml- stack-8.4.4.yaml- stack-8.6.5.yaml- stack-8.8.4.yaml- stack-8.10.7.yaml- stack-9.0.1.yaml- stack-9.2.1.yaml--data-dir: src/data-data-files: emacs-mode/*.el- html/Agda.css- html/highlight-hover.js- JS/agda-rts.js- latex/agda.sty- latex/postprocess-latex.pl- 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/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.6.2.1--flag cpphs- default: False- manual: True- description: Use cpphs instead of cpp.--flag debug- default: False- manual: True- description:- Enable debugging features that may slow Agda down.--flag enable-cluster-counting- default: False- 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- description:- Enable some expensive optimisations when compiling Agda.--custom-setup- setup-depends: base >= 4.9.0.0 && < 4.17- , Cabal >= 1.24.0.0 && < 3.7- , directory >= 1.2.6.2 && < 1.4- , filepath >= 1.4.1.0 && < 1.5- , process >= 1.4.2.0 && < 1.7--library- hs-source-dirs: src/full-- if flag(cpphs)- -- We don't write an upper bound for cpphs because the- -- `build-tools` field can not be modified in Hackage.-- build-tools: cpphs >= 1.20.9- ghc-options: -pgmP cpphs -optP --cpp-- if flag(debug)- cpp-options: -DDEBUG-- if flag(enable-cluster-counting)- cpp-options: -DCOUNT_CLUSTERS- build-depends: text-icu >= 0.7.1.0-- if os(windows)- build-depends: Win32 >= 2.3.1.1 && < 2.13-- -- 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-- build-depends: aeson >= 1.1.2.0 && < 2.1- , array >= 0.5.1.1 && < 0.6- , async >= 2.2 && < 2.3- , base >= 4.9.0.0 && < 4.17- , binary >= 0.8.3.0 && < 0.9- , blaze-html >= 0.8 && < 0.10- , boxes >= 0.1.3 && < 0.2- , bytestring >= 0.10.8.1 && < 0.12- , case-insensitive >= 1.2.0.4 && < 1.3- -- containers-0.5.11.0 is the first to contain IntSet.intersection- , containers >= 0.5.11.0 && < 0.7- , data-hash >= 0.2.0.0 && < 0.3- , deepseq >= 1.4.2.0 && < 1.5- , directory >= 1.2.6.2 && < 1.4- , edit-distance >= 0.2.1.2 && < 0.3- , equivalence >= 0.3.2 && < 0.4- -- exceptions-0.8 instead of 0.10 because of stack- , exceptions >= 0.8 && < 0.11- , filepath >= 1.4.1.0 && < 1.5- , gitrev >= 1.3.1 && < 2.0- -- 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.5- -- There is a "serious bug"- -- (https://hackage.haskell.org/package/hashtables-1.2.0.2/changelog)- -- in hashtables 1.2.0.0/1.2.0.1. This bug seems to- -- have made Agda much slower (infinitely slower?) in- -- some cases.- , hashtables >= 1.2.0.2 && < 1.4- , haskeline >= 0.7.2.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.1 contains a severe bug.- --- -- mtl >= 2.2 && < 2.2.1 doesn't export Control.Monad.Except.- -- Need mtl 2.2.2 for export of Control.Monad.IdentityT (ghc 8.2.2+)- , mtl >= 2.2.1 && < 2.3- , murmur-hash >= 0.1 && < 0.2- , parallel >= 3.2.2.0 && < 3.3- , pretty >= 1.1.3.3 && < 1.2- , process >= 1.4.2.0 && < 1.7- , regex-tdfa >= 1.3.1.0 && < 1.4- , split >= 0.2.0.0 && < 0.2.4- , stm >= 2.4.4 && < 2.6- , strict >= 0.3.2 && < 0.5- , template-haskell >= 2.11.0.0 && < 2.19- , text >= 1.2.3.0 && < 1.3- , time >= 1.6.0.1 && < 1.13- , transformers >= 0.5 && < 0.7- , unordered-containers >= 0.2.5.0 && < 0.3- , uri-encode >= 1.5.0.4 && < 1.6- , zlib == 0.6.*-- -- 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.-- -- ASR (2018-10-16).- -- text-1.2.3.0 required for supporting GHC 8.4.1, 8.4.2 and- -- 8.4.3. See Issue #3277.- -- The other GHC versions can be restricted to >= 1.2.3.1.- if impl(ghc < 8.4.1) || impl(ghc > 8.4.3)- build-depends: text >= 1.2.3.1-- if impl(ghc >= 8.4)- build-depends: ghc-compact == 0.1.*-- -- We don't write upper bounds for Alex nor Happy because the- -- `build-tools` field can not be modified in Hackage. Agda doesn't- -- build with Alex 3.2.0 and segfaults with 3.2.2.- build-tools: alex >= 3.1.0 && < 3.2.0 || == 3.2.1 || >= 3.2.3- , happy >= 1.19.4-- exposed-modules: Agda.Auto.Auto- Agda.Auto.Options- Agda.Auto.CaseSplit- Agda.Auto.Convert- Agda.Auto.NarrowingSearch- Agda.Auto.SearchControl- Agda.Auto.Syntax- Agda.Auto.Typecheck- Agda.Benchmarking- Agda.Compiler.Backend- 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.Response- 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.Syntax.Abstract.Name- Agda.Syntax.Abstract.Pattern- Agda.Syntax.Abstract.PatternSynonyms- Agda.Syntax.Abstract.Pretty- Agda.Syntax.Abstract.Views- Agda.Syntax.Abstract- Agda.Syntax.Builtin- Agda.Syntax.Common- 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.Literal- Agda.Syntax.Notation- Agda.Syntax.Parser.Alex- Agda.Syntax.Parser.Comments- 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.Monad- 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.Datatypes- Agda.TypeChecking.DeadCode- Agda.TypeChecking.DisplayForm- Agda.TypeChecking.DropArgs- Agda.TypeChecking.Empty- Agda.TypeChecking.EtaContract- Agda.TypeChecking.EtaExpand- 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.Monad.Base- 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.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.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.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.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.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.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.Haskell.Syntax- 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.Pretty- 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.Update- Agda.Utils.VarSet- Agda.Utils.Warshall- Agda.Utils.WithDefault- Agda.Utils.Zipper- Agda.Version- Agda.VersionCommit-- other-modules: Paths_Agda- 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-- if flag(optimise-heavily)- ghc-options: -fexpose-all-unfoldings- -fspecialise-aggressively-- -- NOTE: If adding flags, also add to `.ghci-8.0`- if impl(ghc <= 8.0.2)- ghc-options: -fprint-potential-instances- -- Initially, we disable all the warnings.- -w- -Wwarn- -- This option must be the first one after disabling the- -- warnings. See Issue #2094.- -Wunrecognised-warning-flags- -Wdeprecated-flags- -Wderiving-typeable- -Wdodgy-exports- -Wdodgy-foreign-imports- -Wdodgy-imports- -Wduplicate-exports- -Wempty-enumerations- -Widentities- -Wincomplete-patterns- -Winline-rule-shadowing- -Wmissing-fields- -Wmissing-methods- -Wmissing-pattern-synonym-signatures- -Wmissing-signatures- -Wnoncanonical-monad-instances- -Wnoncanonical-monoid-instances- -Woverflowed-literals- -Woverlapping-patterns- -Wsemigroup- -Wtabs- -Wtyped-holes- -Wunrecognised-pragmas- -Wunticked-promoted-constructors- -Wunused-do-bind- -Wunused-foralls- -Wwarnings-deprecations- -Wwrong-do-bind- else- ghc-options: -fprint-potential-instances- -Wwarn=unrecognised-warning-flags- -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=incomplete-patterns- -Wwarn=inline-rule-shadowing- -Wwarn=missing-fields- -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=semigroup- -Wwarn=tabs- -Wwarn=typed-holes- -Wwarn=unrecognised-pragmas- -Wwarn=unticked-promoted-constructors- -Wwarn=unused-do-bind- -Wwarn=unused-foralls- -Wwarn=warnings-deprecations- -Wwarn=wrong-do-bind-- -- NOTE: If adding or removing flags, also change `.ghci-8.2`- if impl(ghc >= 8.2)- ghc-options: -Wcpp-undef- -- ASR TODO (2017-07-23): `make haddock` fails when- -- this flag is on.- -- -Wmissing-home-modules- -Wwarn=simplifiable-class-constraints- -Wwarn=unbanged-strict-patterns-- -- NOTE: If adding or removing flags, also change `.ghci-8.6`- if impl(ghc >= 8.6)- ghc-options: -Wwarn=inaccessible-code- -Wwarn=star-binder- -Wwarn=star-is-type-- -- The following warning is an error in GHC >= 8.10.- if impl(ghc >= 8.6) && impl(ghc < 8.10)- ghc-options: -Wwarn=implicit-kind-vars-- -- NOTE: If adding or removing flags, also change `.ghci-8.8`- if impl(ghc >= 8.8)- ghc-options: -Wwarn=missed-extra-shared-lib-- -- NOTE: If adding or removing flags, also change `.ghci-8.10`- if impl(ghc >= 8.10)- ghc-options: -Wwarn=deriving-defaults- -Wwarn=redundant-record-wildcards- -Wwarn=unused-packages- -Wwarn=unused-record-wildcards-- -- NOTE: If adding or removing flags, also change `.ghci-9.0`- if impl(ghc >= 9.0)- ghc-options: -Wwarn=invalid-haddock-- default-language: Haskell2010-- -- NOTE: If adding or removing default extensions, also change:- -- .ghci-8.0- -- .hlint.yaml- -- This should also use the same extensions as the `test-suite` target below.- default-extensions: BangPatterns- , ConstraintKinds- --L-T Chen (2019-07-15):- -- Enabling DataKinds only locally makes the compile time- -- slightly shorter, see PR #3920.- --, DataKinds- , DefaultSignatures- , DeriveDataTypeable- , DeriveFoldable- , DeriveFunctor- , DeriveGeneric- , DeriveTraversable- , ExistentialQuantification- , FlexibleContexts- , FlexibleInstances- , FunctionalDependencies- , GeneralizedNewtypeDeriving- , InstanceSigs- , LambdaCase- , MultiParamTypeClasses- , MultiWayIf- , NamedFieldPuns- , OverloadedStrings- , PatternSynonyms- , RankNTypes- , RecordWildCards- , ScopedTypeVariables- , StandaloneDeriving- , TupleSections- , TypeFamilies- , TypeSynonymInstances--executable agda- hs-source-dirs: src/main- main-is: Main.hs- build-depends: Agda- -- A version range on Agda generates a warning with- -- some versions of Cabal and GHC- -- (e.g. cabal-install version 1.24.0.2 compiled- -- using version 1.24.2.0 of the Cabal library and- -- GHC 8.2.1 RC1).-- -- Nothing is used from the following package,- -- except for the prelude.- , base >= 4.9.0.0 && < 6- 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=-M3.5G -I0"--executable agda-mode- hs-source-dirs: src/agda-mode- main-is: Main.hs- other-modules: Paths_Agda- build-depends: base >= 4.9.0.0 && < 4.17- , directory >= 1.2.6.2 && < 1.4- , filepath >= 1.4.1.0 && < 1.5- , process >= 1.4.2.0 && < 1.7- default-language: Haskell2010+name: Agda +version: 2.6.2.1 +x-revision: 1 +cabal-version: >= 1.10 +build-type: Custom +license: OtherLicense +license-file: LICENSE +copyright: (c) 2005-2021 The Agda Team. +author: Ulf Norell and The Agda Team, see https://agda.readthedocs.io/en/latest/team.html +maintainer: The Agda Team +homepage: http://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, Epigram 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). + . + Note that the Agda package does not follow the package versioning + policy, because it is not intended to be used by third-party + packages. + +tested-with: GHC == 8.0.2 + GHC == 8.2.2 + GHC == 8.4.4 + GHC == 8.6.5 + GHC == 8.8.4 + GHC == 8.10.7 + GHC == 9.0.1 + GHC == 9.2.1 + +extra-source-files: CHANGELOG.md + README.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 +-- Liang-Ting (2019-11-26): See Issues #4216 +-- doc/user-manual.pdf + stack-8.0.2.yaml + stack-8.2.2.yaml + stack-8.4.4.yaml + stack-8.6.5.yaml + stack-8.8.4.yaml + stack-8.10.7.yaml + stack-9.0.1.yaml + stack-9.2.1.yaml + +data-dir: src/data +data-files: emacs-mode/*.el + html/Agda.css + html/highlight-hover.js + JS/agda-rts.js + latex/agda.sty + latex/postprocess-latex.pl + 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/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.6.2.1 + +flag cpphs + default: False + manual: True + description: Use cpphs instead of cpp. + +flag debug + default: False + manual: True + description: + Enable debugging features that may slow Agda down. + +flag enable-cluster-counting + default: False + 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 + description: + Enable some expensive optimisations when compiling Agda. + +custom-setup + setup-depends: base >= 4.9.0.0 && < 4.17 + , Cabal >= 1.24.0.0 && < 3.7 + , directory >= 1.2.6.2 && < 1.4 + , filepath >= 1.4.1.0 && < 1.5 + , process >= 1.4.2.0 && < 1.7 + +library + hs-source-dirs: src/full + + if flag(cpphs) + -- We don't write an upper bound for cpphs because the + -- `build-tools` field can not be modified in Hackage. + + build-tools: cpphs >= 1.20.9 + ghc-options: -pgmP cpphs -optP --cpp + + if flag(debug) + cpp-options: -DDEBUG + + if flag(enable-cluster-counting) + cpp-options: -DCOUNT_CLUSTERS + build-depends: text-icu >= 0.7.1.0 + + if os(windows) + build-depends: Win32 >= 2.3.1.1 && < 2.13 + + -- 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 + + build-depends: aeson >= 1.1.2.0 && < 2.1 + , array >= 0.5.1.1 && < 0.6 + , async >= 2.2 && < 2.3 + , base >= 4.9.0.0 && < 4.17 + , binary >= 0.8.3.0 && < 0.9 + , blaze-html >= 0.8 && < 0.10 + , boxes >= 0.1.3 && < 0.2 + , bytestring >= 0.10.8.1 && < 0.12 + , case-insensitive >= 1.2.0.4 && < 1.3 + -- containers-0.5.11.0 is the first to contain IntSet.intersection + , containers >= 0.5.11.0 && < 0.7 + , data-hash >= 0.2.0.0 && < 0.3 + , deepseq >= 1.4.2.0 && < 1.5 + , directory >= 1.2.6.2 && < 1.4 + , edit-distance >= 0.2.1.2 && < 0.3 + , equivalence >= 0.3.2 && < 0.4 + -- exceptions-0.8 instead of 0.10 because of stack + , exceptions >= 0.8 && < 0.11 + , filepath >= 1.4.1.0 && < 1.5 + , gitrev >= 1.3.1 && < 2.0 + -- 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.5 + -- There is a "serious bug" + -- (https://hackage.haskell.org/package/hashtables-1.2.0.2/changelog) + -- in hashtables 1.2.0.0/1.2.0.1. This bug seems to + -- have made Agda much slower (infinitely slower?) in + -- some cases. + , hashtables >= 1.2.0.2 && < 1.4 + , haskeline >= 0.7.2.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.1 contains a severe bug. + -- + -- mtl >= 2.2 && < 2.2.1 doesn't export Control.Monad.Except. + -- Need mtl 2.2.2 for export of Control.Monad.IdentityT (ghc 8.2.2+) + , mtl >= 2.2.1 && < 2.3 + , murmur-hash >= 0.1 && < 0.2 + , parallel >= 3.2.2.0 && < 3.3 + , pretty >= 1.1.3.3 && < 1.2 + , process >= 1.4.2.0 && < 1.7 + , regex-tdfa >= 1.3.1.0 && < 1.4 + , split >= 0.2.0.0 && < 0.2.4 + , stm >= 2.4.4 && < 2.6 + , strict >= 0.3.2 && < 0.5 + , template-haskell >= 2.11.0.0 && < 2.19 + , text >= 1.2.3.0 && < 2.1 + , time >= 1.6.0.1 && < 1.13 + , transformers >= 0.5 && < 0.7 + , unordered-containers >= 0.2.5.0 && < 0.3 + , uri-encode >= 1.5.0.4 && < 1.6 + , zlib == 0.6.* + + -- 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. + + -- ASR (2018-10-16). + -- text-1.2.3.0 required for supporting GHC 8.4.1, 8.4.2 and + -- 8.4.3. See Issue #3277. + -- The other GHC versions can be restricted to >= 1.2.3.1. + if impl(ghc < 8.4.1) || impl(ghc > 8.4.3) + build-depends: text >= 1.2.3.1 + + if impl(ghc >= 8.4) + build-depends: ghc-compact == 0.1.* + + -- We don't write upper bounds for Alex nor Happy because the + -- `build-tools` field can not be modified in Hackage. Agda doesn't + -- build with Alex 3.2.0 and segfaults with 3.2.2. + build-tools: alex >= 3.1.0 && < 3.2.0 || == 3.2.1 || >= 3.2.3 + , happy >= 1.19.4 + + exposed-modules: Agda.Auto.Auto + Agda.Auto.Options + Agda.Auto.CaseSplit + Agda.Auto.Convert + Agda.Auto.NarrowingSearch + Agda.Auto.SearchControl + Agda.Auto.Syntax + Agda.Auto.Typecheck + Agda.Benchmarking + Agda.Compiler.Backend + 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.Response + 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.Syntax.Abstract.Name + Agda.Syntax.Abstract.Pattern + Agda.Syntax.Abstract.PatternSynonyms + Agda.Syntax.Abstract.Pretty + Agda.Syntax.Abstract.Views + Agda.Syntax.Abstract + Agda.Syntax.Builtin + Agda.Syntax.Common + 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.Literal + Agda.Syntax.Notation + Agda.Syntax.Parser.Alex + Agda.Syntax.Parser.Comments + 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.Monad + 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.Datatypes + Agda.TypeChecking.DeadCode + Agda.TypeChecking.DisplayForm + Agda.TypeChecking.DropArgs + Agda.TypeChecking.Empty + Agda.TypeChecking.EtaContract + Agda.TypeChecking.EtaExpand + 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.Monad.Base + 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.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.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.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.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.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.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.Haskell.Syntax + 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.Pretty + 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.Update + Agda.Utils.VarSet + Agda.Utils.Warshall + Agda.Utils.WithDefault + Agda.Utils.Zipper + Agda.Version + Agda.VersionCommit + + other-modules: Paths_Agda + 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 + + if flag(optimise-heavily) + ghc-options: -fexpose-all-unfoldings + -fspecialise-aggressively + + -- NOTE: If adding flags, also add to `.ghci-8.0` + if impl(ghc <= 8.0.2) + ghc-options: -fprint-potential-instances + -- Initially, we disable all the warnings. + -w + -Wwarn + -- This option must be the first one after disabling the + -- warnings. See Issue #2094. + -Wunrecognised-warning-flags + -Wdeprecated-flags + -Wderiving-typeable + -Wdodgy-exports + -Wdodgy-foreign-imports + -Wdodgy-imports + -Wduplicate-exports + -Wempty-enumerations + -Widentities + -Wincomplete-patterns + -Winline-rule-shadowing + -Wmissing-fields + -Wmissing-methods + -Wmissing-pattern-synonym-signatures + -Wmissing-signatures + -Wnoncanonical-monad-instances + -Wnoncanonical-monoid-instances + -Woverflowed-literals + -Woverlapping-patterns + -Wsemigroup + -Wtabs + -Wtyped-holes + -Wunrecognised-pragmas + -Wunticked-promoted-constructors + -Wunused-do-bind + -Wunused-foralls + -Wwarnings-deprecations + -Wwrong-do-bind + else + ghc-options: -fprint-potential-instances + -Wwarn=unrecognised-warning-flags + -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=incomplete-patterns + -Wwarn=inline-rule-shadowing + -Wwarn=missing-fields + -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=semigroup + -Wwarn=tabs + -Wwarn=typed-holes + -Wwarn=unrecognised-pragmas + -Wwarn=unticked-promoted-constructors + -Wwarn=unused-do-bind + -Wwarn=unused-foralls + -Wwarn=warnings-deprecations + -Wwarn=wrong-do-bind + + -- NOTE: If adding or removing flags, also change `.ghci-8.2` + if impl(ghc >= 8.2) + ghc-options: -Wcpp-undef + -- ASR TODO (2017-07-23): `make haddock` fails when + -- this flag is on. + -- -Wmissing-home-modules + -Wwarn=simplifiable-class-constraints + -Wwarn=unbanged-strict-patterns + + -- NOTE: If adding or removing flags, also change `.ghci-8.6` + if impl(ghc >= 8.6) + ghc-options: -Wwarn=inaccessible-code + -Wwarn=star-binder + -Wwarn=star-is-type + + -- The following warning is an error in GHC >= 8.10. + if impl(ghc >= 8.6) && impl(ghc < 8.10) + ghc-options: -Wwarn=implicit-kind-vars + + -- NOTE: If adding or removing flags, also change `.ghci-8.8` + if impl(ghc >= 8.8) + ghc-options: -Wwarn=missed-extra-shared-lib + + -- NOTE: If adding or removing flags, also change `.ghci-8.10` + if impl(ghc >= 8.10) + ghc-options: -Wwarn=deriving-defaults + -Wwarn=redundant-record-wildcards + -Wwarn=unused-packages + -Wwarn=unused-record-wildcards + + -- NOTE: If adding or removing flags, also change `.ghci-9.0` + if impl(ghc >= 9.0) + ghc-options: -Wwarn=invalid-haddock + + default-language: Haskell2010 + + -- NOTE: If adding or removing default extensions, also change: + -- .ghci-8.0 + -- .hlint.yaml + -- This should also use the same extensions as the `test-suite` target below. + default-extensions: BangPatterns + , ConstraintKinds + --L-T Chen (2019-07-15): + -- Enabling DataKinds only locally makes the compile time + -- slightly shorter, see PR #3920. + --, DataKinds + , DefaultSignatures + , DeriveDataTypeable + , DeriveFoldable + , DeriveFunctor + , DeriveGeneric + , DeriveTraversable + , ExistentialQuantification + , FlexibleContexts + , FlexibleInstances + , FunctionalDependencies + , GeneralizedNewtypeDeriving + , InstanceSigs + , LambdaCase + , MultiParamTypeClasses + , MultiWayIf + , NamedFieldPuns + , OverloadedStrings + , PatternSynonyms + , RankNTypes + , RecordWildCards + , ScopedTypeVariables + , StandaloneDeriving + , TupleSections + , TypeFamilies + , TypeSynonymInstances + +executable agda + hs-source-dirs: src/main + main-is: Main.hs + build-depends: Agda + -- A version range on Agda generates a warning with + -- some versions of Cabal and GHC + -- (e.g. cabal-install version 1.24.0.2 compiled + -- using version 1.24.2.0 of the Cabal library and + -- GHC 8.2.1 RC1). + + -- Nothing is used from the following package, + -- except for the prelude. + , base >= 4.9.0.0 && < 6 + 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=-M3.5G -I0" + +executable agda-mode + hs-source-dirs: src/agda-mode + main-is: Main.hs + other-modules: Paths_Agda + build-depends: base >= 4.9.0.0 && < 4.17 + , directory >= 1.2.6.2 && < 1.4 + , filepath >= 1.4.1.0 && < 1.5 + , process >= 1.4.2.0 && < 1.7 + default-language: Haskell2010
revision 2
name: Agda version: 2.6.2.1 -x-revision: 1 +x-revision: 2 cabal-version: >= 1.10 build-type: Custom license: OtherLicense , binary >= 0.8.3.0 && < 0.9 , blaze-html >= 0.8 && < 0.10 , boxes >= 0.1.3 && < 0.2 - , bytestring >= 0.10.8.1 && < 0.12 + , bytestring >= 0.10.8.1 && < 0.11.2 , case-insensitive >= 1.2.0.4 && < 1.3 -- containers-0.5.11.0 is the first to contain IntSet.intersection , containers >= 0.5.11.0 && < 0.7
revision 3
name: Agda version: 2.6.2.1 -x-revision: 2 +x-revision: 3 cabal-version: >= 1.10 build-type: Custom license: OtherLicense -- -- mtl >= 2.2 && < 2.2.1 doesn't export Control.Monad.Except. -- Need mtl 2.2.2 for export of Control.Monad.IdentityT (ghc 8.2.2+) - , mtl >= 2.2.1 && < 2.3 + , mtl >= 2.2.1 && < 2.4 , murmur-hash >= 0.1 && < 0.2 , parallel >= 3.2.2.0 && < 3.3 , pretty >= 1.1.3.3 && < 1.2 , template-haskell >= 2.11.0.0 && < 2.19 , text >= 1.2.3.0 && < 2.1 , time >= 1.6.0.1 && < 1.13 - , transformers >= 0.5 && < 0.7 + , transformers >= 0.5 && < 0.6 + -- build failure with transformers-0.6 , unordered-containers >= 0.2.5.0 && < 0.3 , uri-encode >= 1.5.0.4 && < 1.6 , zlib == 0.6.*
revision 4
name: Agda version: 2.6.2.1 -x-revision: 3 +x-revision: 4 cabal-version: >= 1.10 build-type: Custom license: OtherLicense , deepseq >= 1.4.2.0 && < 1.5 , directory >= 1.2.6.2 && < 1.4 , edit-distance >= 0.2.1.2 && < 0.3 - , equivalence >= 0.3.2 && < 0.4 + , equivalence >= 0.3.2 && < 0.5 -- exceptions-0.8 instead of 0.10 because of stack , exceptions >= 0.8 && < 0.11 , filepath >= 1.4.1.0 && < 1.5