Agda-2.6.0: Agda.cabal
name: Agda
version: 2.6.0
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ánszky, 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 <ulfn@chalmers.se>
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
GHC == 8.6.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
stack-8.6.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/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/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/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/String/Properties.agda
lib/prim/Agda/Builtin/TrustMe.agda
lib/prim/Agda/Builtin/Unit.agda
lib/prim/Agda/Builtin/Word.agda
lib/prim/Agda/Primitive.agda
lib/prim/Agda/Primitive/Cubical.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.6.0
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.13
, Cabal >= 1.22.5.0 && < 2.5
, filepath >= 1.4.0.0 && < 1.5
, process >= 1.2.3.0 && < 1.7
, directory >= 1.2.2.0 && < 1.4
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
-- 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 >= 0.11.3.0 && < 1.5
, array >= 0.5.1.0 && < 0.6
, async >= 2.2 && < 2.3
, base >= 4.8.0.0 && < 4.13
, 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.7
, 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
-- exceptions-0.8 instead of 0.10 because of stack
, exceptions >= 0.8 && < 0.11
, 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
, split >= 0.2.0.0 && < 0.2.3.4
, stm >= 2.4.4 && < 2.6
, strict >= 0.3.2 && < 0.4
, template-haskell >= 2.10.0.0 && < 2.15
, 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.6.4) && impl(ghc < 8.6.6)
build-depends: transformers == 0.5.6.2
if impl(ghc >= 8.4) && impl(ghc < 8.6.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 `Data.Semigroups` API for pre-GHC8
build-depends: 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.AgdaTop
Agda.Interaction.BasicOps
Agda.Interaction.SearchAbout
Agda.Interaction.CommandLine
Agda.Interaction.EmacsCommand
Agda.Interaction.EmacsTop
Agda.Interaction.JSONTop
Agda.Interaction.FindFile
Agda.Interaction.Highlighting.Common
Agda.Interaction.Highlighting.Dot
Agda.Interaction.Highlighting.Emacs
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.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.Builtin
Agda.Syntax.Common
Agda.Syntax.Concrete.Attribute
Agda.Syntax.Concrete.Definitions
Agda.Syntax.Concrete.Fixity
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.EtaExpand
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.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.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.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.Primitive
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.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.Telescope.Path
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.Graph.TopSort
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.TempFile
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.TypeLits
Agda.Utils.Update
Agda.Utils.VarSet
Agda.Utils.Warshall
Agda.Utils.WithDefault
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
if impl(ghc >= 8.6)
ghc-options: -Winaccessible-code
default-language: Haskell2010
default-extensions: ConstraintKinds
, DataKinds
, DefaultSignatures
, DeriveFoldable
, DeriveFunctor
, DeriveTraversable
, ExistentialQuantification
, FlexibleContexts
, FlexibleInstances
, FunctionalDependencies
, LambdaCase
, MultiParamTypeClasses
, MultiWayIf
, NamedFieldPuns
, OverloadedStrings
, 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.13
, directory >= 1.2.2.0 && < 1.4
, filepath >= 1.4.0.0 && < 1.5
, process >= 1.2.3.0 && < 1.7
default-language: Haskell2010