summaryrefslogtreecommitdiff
path: root/Agda.cabal
diff options
context:
space:
mode:
Diffstat (limited to 'Agda.cabal')
-rw-r--r--Agda.cabal259
1 files changed, 149 insertions, 110 deletions
diff --git a/Agda.cabal b/Agda.cabal
index 3adcfac..749224a 100644
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -1,6 +1,6 @@
name: Agda
-version: 2.5.1.2
-cabal-version: >= 1.8
+version: 2.5.2
+cabal-version: >= 1.10
build-type: Custom
license: OtherLicense
license-file: LICENSE
@@ -36,18 +36,22 @@ tested-with: GHC == 7.6.3
GHC == 7.8.4
GHC == 7.10.3
GHC == 8.0.1
-extra-source-files: src/full/undefined.h
+
+extra-source-files: CHANGELOG.md
README.md
- CHANGELOG
+ src/full/undefined.h
+ stack-7.8.4.yaml
+ stack-8.0.1.yaml
+
data-dir: src/data
data-files: Agda.css
+ agda.sty
emacs-mode/*.el
-- EpicInclude/AgdaPrelude.e
-- EpicInclude/stdagda.c
-- EpicInclude/stdagda.h
- agda.sty
- postprocess-latex.pl
- lib/prim/Agda/Primitive.agda
+ 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
@@ -66,10 +70,14 @@ data-files: Agda.css
lib/prim/Agda/Builtin/String.agda
lib/prim/Agda/Builtin/TrustMe.agda
lib/prim/Agda/Builtin/Unit.agda
+ lib/prim/Agda/Primitive.agda
+ MAlonzo/src/MAlonzo/*.hs
+ postprocess-latex.pl
uhc-agda-base/LICENSE
- uhc-agda-base/uhc-agda-base.cabal
uhc-agda-base/src/UHC/Agda/*.hs
- MAlonzo/src/MAlonzo/*.hs
+ uhc-agda-base/src/UHC/Agda/double.c
+ uhc-agda-base/src/UHC/Agda/double.h
+ uhc-agda-base/uhc-agda-base.cabal
source-repository head
type: git
@@ -77,8 +85,8 @@ source-repository head
source-repository this
type: git
- location: https://github.com/agda/agda/tree/v2.5.1.2
- tag: v2.5.1.2
+ location: https://github.com/agda/agda/tree/v2.5.2.
+ tag: v2.5.2
flag cpphs
default: True
@@ -91,12 +99,23 @@ flag uhc
description:
Enable the UHC backend. For details, consult the Agda User Manual.
+flag debug
+ default: False
+ manual: True
+ description:
+ Enable debugging features that may slow Agda down.
+
library
hs-source-dirs: src/full
include-dirs: src/full
if flag(cpphs)
- build-tools: cpphs >= 1.19
+ -- 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.2
ghc-options: -pgmP cpphs -optP --cpp
if flag(uhc)
@@ -109,59 +128,60 @@ library
-- definitions, see module Agda.Compiler.UHC.Bridge.
cpp-options: -DUHC_BACKEND
+ if flag(debug)
+ cpp-options: -DDEBUG
+
if os(windows)
build-depends: Win32 >= 2.2 && < 2.4
- build-depends:
- array >= 0.4.0.1 && < 0.6
- , base >= 4.6.0.1 && < 4.10
- , binary >= 0.7.2.1 && < 0.9
- , boxes >= 0.1.3 && < 0.2
- , bytestring >= 0.10.0.2 && < 0.11
- , containers >= 0.5.0.0 && < 0.6
- , data-hash >= 0.2.0.0 && < 0.3
- , deepseq >= 1.3.0.1 && < 1.5
- , directory >= 1.2.0.1 && < 1.3
- -- Edison versioning scheme: http://rwd.rdockins.name/edison/home/.
- -- EdisonAPI isn't used by Agda, but EdisonCore 1.3.1 doesn't
- -- declare what version of EdisonAPI it depends on.
- , EdisonAPI == 1.3
- , EdisonCore >= 1.3.1.1 && < 1.3.2
- , edit-distance >= 0.2.1.2 && < 0.3
- , equivalence >= 0.2.5 && < 0.4
- , filepath >= 1.3.0.1 && < 1.5
- , geniplate-mirror >= 0.6.0.6 && < 0.8
- -- 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.0.1.8 && < 1.2 || >= 1.2.0.2 && < 1.3
- , haskeline >= 0.7.1.3 && < 0.8
- , haskell-src-exts >= 1.16.0.1 && < 1.18
- , monadplus >= 1.4 && < 1.5
- -- mtl-2.1 contains a severe bug.
- --
- -- mtl >= 2.2 && < 2.2.1 doesn't export Control.Monad.Except.
- , mtl >= 2.1.1 && <= 2.1.3.1 || >= 2.2.1 && < 2.3
- , QuickCheck >= 2.8.2 && < 2.9
- , parallel >= 3.2.0.4 && < 3.3
- -- pretty 1.1.1.2 and 1.1.1.3 do not follow the package versioning
- -- policy.
- , pretty >= 1.1.1.0 && < 1.1.1.2 || >= 1.1.2 && < 1.2
- , process >= 1.1.0.2 && < 1.5
- , strict >= 0.3.2 && < 0.4
- , template-haskell >= 2.8.0.0 && < 2.12
- , text >= 0.11.3.1 && < 1.3
- , time >= 1.4.0.1 && < 1.7
- -- transformers 0.4.0.0 was deprecated.
- , transformers >= 0.3 && < 0.4 || >= 0.4.1.0 && < 0.6
- , transformers-compat >= 0.3.3.3 && < 0.6
- , unordered-containers >= 0.2.5.0 && < 0.3
- , xhtml >= 3000.2.1 && < 3000.3
+ build-depends: array >= 0.4.0.1 && < 0.6
+ , base >= 4.6.0.1 && < 4.10
+ , binary >= 0.7.2.1 && < 0.9
+ , boxes >= 0.1.3 && < 0.2
+ , bytestring >= 0.10.0.2 && < 0.11
+ , containers >= 0.5.0.0 && < 0.6
+ , data-hash >= 0.2.0.0 && < 0.3
+ , deepseq >= 1.3.0.1 && < 1.5
+ , directory >= 1.2.0.1 && < 1.4
+ , EdisonCore >= 1.3.1.1 && < 1.3.2
+ , edit-distance >= 0.2.1.2 && < 0.3
+ , equivalence >= 0.2.5 && < 0.4
+ , filepath >= 1.3.0.1 && < 1.5
+ , geniplate-mirror >= 0.6.0.6 && < 0.8
+ , gitrev >= 1.2 && < 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.0.1.8 && < 1.2 || >= 1.2.0.2 && < 1.3
+ , haskeline >= 0.7.1.3 && < 0.8
+ , ieee754 >= 0.7.8 && < 0.8
+ , monadplus >= 1.4 && < 1.5
+ -- mtl-2.1 contains a severe bug.
+ --
+ -- mtl >= 2.2 && < 2.2.1 doesn't export Control.Monad.Except.
+ , mtl >= 2.1.1 && <= 2.1.3.1 || >= 2.2.1 && < 2.3
+ , murmur-hash >= 0.1 && < 0.2
+ , parallel >= 3.2.0.4 && < 3.3
+ -- pretty 1.1.1.2 and 1.1.1.3 do not follow the
+ -- package versioning policy.
+ , pretty >= 1.1.1.0 && < 1.1.1.2 || >= 1.1.2 && < 1.2
+ , process >= 1.1.0.2 && < 1.5
+ , regex-tdfa >= 1.2.2 && < 1.3
+ , strict >= 0.3.2 && < 0.4
+ , template-haskell >= 2.8.0.0 && < 2.12
+ , text >= 0.11.3.1 && < 1.3
+ , time >= 1.4.0.1 && < 1.7
+ -- transformers 0.4.0.0 was deprecated.
+ , transformers >= 0.3 && < 0.4 || >= 0.4.1.0 && < 0.6
+ , transformers-compat >= 0.3.3.3 && < 0.6
+ , unordered-containers >= 0.2.5.0 && < 0.3
+ , xhtml >= 3000.2.1 && < 3000.3
if impl(ghc < 7.8)
build-depends: base-orphans >= 0.3.1 && < 0.5
@@ -175,6 +195,12 @@ library
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.*
+
-- Agda doesn't build with Alex 3.2.0.
build-tools: alex >= 3.1.0 && < 3.2.0 || >= 3.2.1 && < 3.3
, happy >= 1.19.4 && < 2
@@ -205,11 +231,9 @@ library
Agda.Compiler.Epic.Smashing
Agda.Compiler.Epic.Static
Agda.Compiler.HaskellTypes
- Agda.Compiler.JS.Case
Agda.Compiler.JS.Compiler
Agda.Compiler.JS.Syntax
Agda.Compiler.JS.Substitution
- Agda.Compiler.JS.Parser
Agda.Compiler.JS.Pretty
Agda.Compiler.MAlonzo.Compiler
Agda.Compiler.MAlonzo.Encode
@@ -217,10 +241,14 @@ library
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.DelayCoinduction
+ 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
@@ -235,14 +263,12 @@ library
Agda.Compiler.UHC.Pragmas.Base
Agda.Compiler.UHC.Pragmas.Parse
Agda.Compiler.UHC.Primitives
- Agda.Compiler.UHC.Smashing
Agda.ImpossibleTest
Agda.Interaction.BasicOps
Agda.Interaction.SearchAbout
Agda.Interaction.CommandLine
Agda.Interaction.EmacsCommand
Agda.Interaction.EmacsTop
- Agda.Interaction.Exceptions
Agda.Interaction.FindFile
Agda.Interaction.Highlighting.Dot
Agda.Interaction.Highlighting.Emacs
@@ -273,16 +299,19 @@ library
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.Pretty
Agda.Syntax.Concrete
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
@@ -290,6 +319,7 @@ library
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
@@ -316,7 +346,6 @@ library
Agda.Termination.Semiring
Agda.Termination.TermCheck
Agda.Termination.Termination
- Agda.Tests
Agda.TheTypeChecker
Agda.TypeChecking.Abstract
Agda.TypeChecking.CheckInternal
@@ -338,7 +367,6 @@ library
Agda.TypeChecking.Free
Agda.TypeChecking.Free.Lazy
Agda.TypeChecking.Free.Old
- Agda.TypeChecking.Free.Tests
Agda.TypeChecking.Forcing
Agda.TypeChecking.Implicit
Agda.TypeChecking.Injectivity
@@ -359,6 +387,7 @@ library
Agda.TypeChecking.Monad.Env
Agda.TypeChecking.Monad.Exception
Agda.TypeChecking.Monad.Imports
+ Agda.TypeChecking.Monad.Local
Agda.TypeChecking.Monad.MetaVars
Agda.TypeChecking.Monad.Mutual
Agda.TypeChecking.Monad.Open
@@ -375,7 +404,6 @@ library
Agda.TypeChecking.Polarity
Agda.TypeChecking.Positivity
Agda.TypeChecking.Positivity.Occurrence
- Agda.TypeChecking.Positivity.Tests
Agda.TypeChecking.Pretty
Agda.TypeChecking.Primitive
Agda.TypeChecking.ProjectionLike
@@ -384,6 +412,7 @@ library
Agda.TypeChecking.RecordPatterns
Agda.TypeChecking.Records
Agda.TypeChecking.Reduce
+ Agda.TypeChecking.Reduce.Fast
Agda.TypeChecking.Reduce.Monad
Agda.TypeChecking.Rewriting
Agda.TypeChecking.Rewriting.NonLinMatch
@@ -394,6 +423,7 @@ library
Agda.TypeChecking.Rules.Def
Agda.TypeChecking.Rules.Display
Agda.TypeChecking.Rules.LHS
+ Agda.TypeChecking.Rules.LHS.AsPatterns
Agda.TypeChecking.Rules.LHS.Implicit
Agda.TypeChecking.Rules.LHS.Instantiate
Agda.TypeChecking.Rules.LHS.Problem
@@ -413,15 +443,13 @@ library
Agda.TypeChecking.SizedTypes
Agda.TypeChecking.SizedTypes.Solve
Agda.TypeChecking.SizedTypes.Syntax
- Agda.TypeChecking.SizedTypes.Tests
Agda.TypeChecking.SizedTypes.Utils
Agda.TypeChecking.SizedTypes.WarshallSolver
Agda.TypeChecking.Substitute
- Agda.TypeChecking.Substitute.Pattern
+ Agda.TypeChecking.Substitute.Class
+ Agda.TypeChecking.Substitute.DeBruijn
Agda.TypeChecking.SyntacticEquality
Agda.TypeChecking.Telescope
- Agda.TypeChecking.Test.Generators
- Agda.TypeChecking.Tests
Agda.TypeChecking.Unquote
Agda.TypeChecking.With
Agda.Utils.AssocList
@@ -440,9 +468,9 @@ library
Agda.Utils.Function
Agda.Utils.Geniplate
Agda.Utils.Graph.AdjacencyMap.Unidirectional
- Agda.Utils.Graph.AdjacencyMap.Unidirectional.Tests
Agda.Utils.Hash
Agda.Utils.HashMap
+ Agda.Utils.Haskell.Syntax
Agda.Utils.Impossible
Agda.Utils.IO.Binary
Agda.Utils.IO.Directory
@@ -452,7 +480,6 @@ library
Agda.Utils.Lens.Examples
Agda.Utils.List
Agda.Utils.ListT
- Agda.Utils.ListT.Tests
Agda.Utils.Map
Agda.Utils.Maybe
Agda.Utils.Maybe.Strict
@@ -463,16 +490,13 @@ library
Agda.Utils.Parser.ReadP
Agda.Utils.PartialOrd
Agda.Utils.Permutation
- Agda.Utils.Permutation.Tests
Agda.Utils.Pointer
Agda.Utils.Pretty
- Agda.Utils.QuickCheck
Agda.Utils.SemiRing
Agda.Utils.Singleton
Agda.Utils.Size
Agda.Utils.String
Agda.Utils.Suffix
- Agda.Utils.TestHelpers
Agda.Utils.Time
Agda.Utils.Trie
Agda.Utils.Tuple
@@ -480,12 +504,20 @@ library
Agda.Utils.VarSet
Agda.Utils.Warshall
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.6.3)
- ghc-options: -w
- -fwarn-deprecated-flags
+ ghc-options: -fwarn-deprecated-flags
-fwarn-dodgy-exports
-fwarn-dodgy-foreign-imports
-fwarn-dodgy-imports
@@ -496,7 +528,6 @@ library
-fwarn-missing-fields
-fwarn-missing-methods
-fwarn-missing-signatures
- -fwarn-orphans
-fwarn-tabs
-fwarn-overlapping-patterns
-fwarn-unrecognised-pragmas
@@ -512,6 +543,8 @@ library
if impl(ghc >= 7.10)
ghc-options: -fwarn-unticked-promoted-constructors
+ -- Enable after removing the support for GHC 7.8.
+ -- -fwarn-deriving-typeable
-- This option is deprected in GHC 7.10.1.
if impl(ghc >= 7.8) && impl(ghc < 7.10)
@@ -530,16 +563,40 @@ library
ghc-options: -fwarn-context-quantification
if impl(ghc >= 8.0)
- ghc-options: -Wnoncanonical-monad-instances
+ ghc-options: -Wmissing-pattern-synonym-signatures
+ -Wnoncanonical-monad-instances
+ -Wnoncanonical-monoid-instances
+ -Wsemigroup
+ -Wunused-foralls
+
+ default-language: Haskell2010
+ default-extensions: ConstraintKinds
+ , DataKinds
+ , DefaultSignatures
+ , DeriveFunctor
+ , DeriveFoldable
+ , DeriveTraversable
+ , ExistentialQuantification
+ , FlexibleContexts
+ , FlexibleInstances
+ , FunctionalDependencies
+ , LambdaCase
+ , MultiParamTypeClasses
+ , NamedFieldPuns
+ , RankNTypes
+ , RecordWildCards
+ , StandaloneDeriving
+ , TupleSections
+ , TypeSynonymInstances
executable agda
hs-source-dirs: src/main
main-is: Main.hs
- build-depends:
- Agda == 2.5.1.2
- -- Nothing is used from the following package, except for the
- -- prelude.
- , base >= 4.6.0.1 && < 6
+ build-depends: Agda == 2.5.2
+ -- Nothing is used from the following package,
+ -- except for the prelude.
+ , base >= 4.6.0.1 && < 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).
@@ -552,26 +609,8 @@ executable agda-mode
hs-source-dirs: src/agda-mode
main-is: Main.hs
other-modules: Paths_Agda
- build-depends:
- base >= 4.6.0.1 && < 4.10
- , directory >= 1.2.0.1 && < 1.3
- , filepath >= 1.3.0.1 && < 1.5
- , process >= 1.1.0.2 && < 1.5
-
-executable agda-ghc-names
- hs-source-dirs: src/agda-ghc-names
- main-is: agda-ghc-names.hs
- other-modules: ExtractNames
- , Find
- , FixProf
- , ResolveHsNames
- build-depends:
- base >= 4.6.0.1 && < 4.10
- , binary >= 0.7.2.1 && < 0.9
- , containers >= 0.5.0.0 && < 0.6
- , filemanip >= 0.3.6.3 && < 0.4
- , haskell-src-exts >= 1.16.0.1 && < 1.18
- , mtl >= 2.1.1 && <= 2.1.3.1 || >= 2.2.1 && < 2.3
- , filepath >= 1.3.0.1 && < 1.5
- ghc-options: -rtsopts
-
+ build-depends: base >= 4.6.0.1 && < 4.10
+ , directory >= 1.2.0.1 && < 1.4
+ , filepath >= 1.3.0.1 && < 1.5
+ , process >= 1.1.0.2 && < 1.5
+ default-language: Haskell2010