name: Agda version: 2.5.4.2 cabal-version: >= 1.10 build-type: Custom license: OtherLicense license-file: LICENSE author: Agda 2 was originally written by Ulf Norell, partially based on code from Agda 1 by Catarina Coquand and Makoto Takeyama, and from Agdalight by Ulf Norell and Andreas Abel. Agda 2 is currently actively developed mainly by Andreas Abel, Guillaume Allais, Jesper Cockx, Nils Anders Danielsson, Philipp Hausmann, Fredrik Nordvall Forsberg, Ulf Norell, Víctor López Juan, Andrés Sicard-Ramírez, and Andrea Vezzosi. Further, Agda 2 has received contributions by, amongst others, Stevan Andjelkovic, Marcin Benke, Jean-Philippe Bernardy, Guillaume Brunerie, James Chapman, Dominique Devriese, Péter Diviánszki, Olle Fredriksson, Adam Gundry, Daniel Gustafsson, Kuen-Bang Hou (favonia), Patrik Jansson, Alan Jeffrey, Wolfram Kahl, Wen Kokke, Fredrik Lindblad, Francesco Mazzoli, Stefan Monnier, Darin Morrison, Guilhem Moulin, Nicolas Pouillard, Nobuo Yamashita, Christian Sattler, and Makoto Takeyama and many more. maintainer: Ulf Norell 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 == 7.10.3 GHC == 8.0.2 GHC == 8.2.2 GHC == 8.4.4 extra-source-files: CHANGELOG.md README.md doc/user-manual.pdf src/full/undefined.h stack-7.10.3.yaml stack-8.0.2.yaml stack-8.2.2.yaml stack-8.4.4.yaml data-dir: src/data data-files: Agda.css agda.sty emacs-mode/*.el JS/agda-rts.js JS/biginteger.js lib/prim/Agda/Builtin/Bool.agda lib/prim/Agda/Builtin/Char.agda lib/prim/Agda/Builtin/Coinduction.agda lib/prim/Agda/Builtin/Equality.agda lib/prim/Agda/Builtin/Float.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/Nat.agda lib/prim/Agda/Builtin/Reflection.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/TrustMe.agda lib/prim/Agda/Builtin/Unit.agda lib/prim/Agda/Builtin/Word.agda lib/prim/Agda/Primitive.agda MAlonzo/src/MAlonzo/*.hs postprocess-latex.pl 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.5.4.2 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.) -- ASR (2018-09-14). Every new setup dependency should also be added -- as a library dependency. See Issue #3225. custom-setup setup-depends: base >= 4.8.0.0 && < 4.12 , Cabal >= 1.22.5.0 && < 2.3 , filepath >= 1.4.0.0 && < 1.5 , filemanip >= 0.3.6.2 && < 0.4 , process >= 1.2.3.0 && < 1.7 library hs-source-dirs: src/full include-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. -- If your change the lower bound of cpphs also change it in the -- `.travis.yml` file [Issue #2315]. build-tools: cpphs >= 1.20.8 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.* if os(windows) build-depends: Win32 >= 2.3.1.0 && < 2.7 build-depends: array >= 0.5.1.0 && < 0.6 , async >= 2.2 && < 2.3 , base >= 4.8.0.0 && < 4.12 , binary >= 0.7.3.0 && < 0.9 , blaze-html >= 0.8 && < 0.10 , boxes >= 0.1.3 && < 0.2 , bytestring >= 0.10.6.0 && < 0.11 , containers >= 0.5.6.2 && < 0.6 , data-hash >= 0.2.0.0 && < 0.3 , deepseq >= 1.4.1.1 && < 1.5 , directory >= 1.2.2.0 && < 1.4 -- EdisonCore 1.3.2 doesn't compile with GHC 7.10.*. , EdisonCore == 1.3.1.1 || >= 1.3.2.1 && < 1.4 , edit-distance >= 0.2.1.2 && < 0.3 , equivalence >= 0.3.2 && < 0.4 , filepath >= 1.4.0.0 && < 1.5 , geniplate-mirror >= 0.6.0.6 && < 0.8 , 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.3 -- 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.3 , haskeline >= 0.7.2.1 && < 0.8 , ieee754 >= 0.7.8 && < 0.9 -- mtl-2.1 contains a severe bug. -- -- mtl >= 2.2 && < 2.2.1 doesn't export Control.Monad.Except. , mtl >= 2.2.1 && < 2.3 , murmur-hash >= 0.1 && < 0.2 , pretty >= 1.1.2.0 && < 1.2 , process >= 1.2.3.0 && < 1.7 , regex-tdfa >= 1.2.2 && < 1.3 , stm >= 2.4.4 && < 2.5 , strict >= 0.3.2 && < 0.4 , template-haskell >= 2.10.0.0 && < 2.14 , time >= 1.5.0.1 && < 1.9 , unordered-containers >= 0.2.5.0 && < 0.3 , uri-encode >= 1.5.0.4 && < 1.6 -- In hTags the mtl library must be compiled with the version of -- transformers shipped with GHC, so we use that version in Agda (see, -- for example, Issue 2983). if impl(ghc >= 8.4) build-depends: transformers == 0.5.5.0 -- ASR (2018-10-16). Required for supporting GHC 8.4.1, 8.4.2 and -- 8.4.3. See Issue #3277. if impl(ghc >= 8.4.1) && impl(ghc <= 8.4.3) build-depends: text >= 1.2.3.0 && < 1.3 else build-depends: text >= 1.2.3.1 && < 1.3 if impl(ghc >= 8.0) && impl(ghc < 8.4) build-depends: transformers == 0.5.2.0 -- ASR (2018-09-14). We add the dependency on the filemanip library -- due to Issue #3225. if impl(ghc >= 7.10) && impl(ghc < 8.0) build-depends: transformers == 0.4.2.0 , filemanip >= 0.3.6.2 && < 0.4 -- zlib >= 0.6.1 is broken with GHC < 7.10.3. See Issue 1518. if impl(ghc < 7.10.3) build-depends: zlib >= 0.4.0.1 && < 0.6.1 else build-depends: zlib >= 0.4.0.1 && < 0.7 if impl(ghc < 8.0) -- provide/emulate `Control.Monad.Fail` and `Data.Semigroups` API -- for pre-GHC8 build-depends: fail == 4.9.* , semigroups == 0.18.* -- 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.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.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.BasicOps Agda.Interaction.SearchAbout Agda.Interaction.CommandLine Agda.Interaction.EmacsCommand Agda.Interaction.EmacsTop Agda.Interaction.FindFile Agda.Interaction.Highlighting.Dot Agda.Interaction.Highlighting.Emacs Agda.Interaction.Highlighting.Generate Agda.Interaction.Highlighting.HTML 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.IORefs Agda.Interaction.Options.Lenses Agda.Interaction.Options.Warnings Agda.Main Agda.Syntax.Abstract.Copatterns 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.Common Agda.Syntax.Concrete.Definitions Agda.Syntax.Concrete.Generic 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.Defs Agda.Syntax.Internal.Generic 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.Inlining 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.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.Errors Agda.TypeChecking.Free Agda.TypeChecking.Free.Lazy Agda.TypeChecking.Free.Old Agda.TypeChecking.Free.Precompute Agda.TypeChecking.Free.Reduce Agda.TypeChecking.Forcing Agda.TypeChecking.Functions Agda.TypeChecking.Implicit Agda.TypeChecking.Injectivity Agda.TypeChecking.Inlining Agda.TypeChecking.InstanceArguments Agda.TypeChecking.Irrelevance Agda.TypeChecking.Level Agda.TypeChecking.LevelConstraints 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.Signature Agda.TypeChecking.Monad.SizedTypes Agda.TypeChecking.Monad.State Agda.TypeChecking.Monad.Statistics Agda.TypeChecking.Monad.Trace Agda.TypeChecking.Monad 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.Primitive 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.NonLinMatch 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.Unquote Agda.TypeChecking.Warnings Agda.TypeChecking.With Agda.Utils.AffineHole Agda.Utils.AssocList Agda.Utils.Bag Agda.Utils.Benchmark Agda.Utils.BiMap Agda.Utils.Char Agda.Utils.Cluster Agda.Utils.Empty Agda.Utils.Environment Agda.Utils.Except Agda.Utils.Either Agda.Utils.Favorites Agda.Utils.FileName Agda.Utils.Float Agda.Utils.Functor Agda.Utils.Function Agda.Utils.Geniplate Agda.Utils.Graph.AdjacencyMap.Unidirectional Agda.Utils.Hash Agda.Utils.HashMap 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.UTF8 Agda.Utils.IORef Agda.Utils.Lens Agda.Utils.Lens.Examples Agda.Utils.List Agda.Utils.ListT Agda.Utils.Map Agda.Utils.Maybe Agda.Utils.Maybe.Strict Agda.Utils.Memo Agda.Utils.Monad Agda.Utils.Monoid Agda.Utils.NonemptyList Agda.Utils.Null Agda.Utils.Parser.MemoisedCPS Agda.Utils.Parser.ReadP Agda.Utils.PartialOrd Agda.Utils.Permutation Agda.Utils.Pointer Agda.Utils.POMonoid Agda.Utils.Pretty Agda.Utils.SemiRing Agda.Utils.Singleton Agda.Utils.Size Agda.Utils.String Agda.Utils.Suffix Agda.Utils.Three Agda.Utils.Time Agda.Utils.Trie Agda.Utils.Tuple Agda.Utils.TypeLevel Agda.Utils.Update Agda.Utils.VarSet Agda.Utils.Warshall Agda.Utils.Zipper Agda.Version Agda.VersionCommit other-modules: Paths_Agda -- Initially, we disable all the warnings. ghc-options: -w -- This option must be the first one after disabling the warnings. See -- Issue #2094. if impl(ghc >= 8.0) ghc-options: -Wunrecognised-warning-flags if impl(ghc >= 7.10) ghc-options: -fwarn-deprecated-flags -fwarn-deriving-typeable -fwarn-dodgy-exports -fwarn-dodgy-foreign-imports -fwarn-dodgy-imports -fwarn-duplicate-exports -fwarn-empty-enumerations -fwarn-hi-shadowing -fwarn-identities -fwarn-incomplete-patterns -fwarn-inline-rule-shadowing -fwarn-missing-fields -fwarn-missing-methods -fwarn-missing-signatures -fwarn-tabs -fwarn-typed-holes -fwarn-overflowed-literals -fwarn-overlapping-patterns -fwarn-unrecognised-pragmas -fwarn-unticked-promoted-constructors -fwarn-unused-do-bind -fwarn-warnings-deprecations -fwarn-wrong-do-bind -- These options will be removed in GHC 8.0.1. if impl(ghc >= 7.10) && impl(ghc < 8.0) ghc-options: -fwarn-context-quantification -fwarn-duplicate-constraints -fwarn-pointless-pragmas if impl(ghc >= 8.0) ghc-options: -Wmissing-pattern-synonym-signatures -Wnoncanonical-monad-instances -Wnoncanonical-monoid-instances -Wsemigroup -Wunused-foralls 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 -Wsimplifiable-class-constraints -Wunbanged-strict-patterns default-language: Haskell2010 default-extensions: ConstraintKinds , DataKinds , DefaultSignatures , DeriveFoldable , DeriveFunctor , DeriveTraversable , ExistentialQuantification , FlexibleContexts , FlexibleInstances , FunctionalDependencies , LambdaCase , MultiParamTypeClasses , MultiWayIf , NamedFieldPuns , RankNTypes , RecordWildCards , ScopedTypeVariables , StandaloneDeriving , TypeSynonymInstances , TupleSections 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.8.0.0 && < 6 default-language: Haskell2010 if impl(ghc >= 7) -- 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. ghc-options: -rtsopts executable agda-mode hs-source-dirs: src/agda-mode main-is: Main.hs other-modules: Paths_Agda build-depends: base >= 4.8.0.0 && < 4.12 , directory >= 1.2.2.0 && < 1.4 , filepath >= 1.4.0.0 && < 1.5 , process >= 1.2.3.0 && < 1.7 default-language: Haskell2010