Agda-2.4.2: Agda.cabal
name: Agda
version: 2.4.2
cabal-version: >= 1.8
build-type: Custom
license: OtherLicense
license-file: LICENSE
author: Ulf Norell, Andreas Abel, Nils Anders Danielsson, Makoto Takeyama, Catarina Coquand, with contributions by Stevan Andjelkovic, Marcin Benke, Jean-Philippe Bernardy, James Chapman, Jesper Cockx, Dominique Devriese, Peter Divanski, Fredrik Nordvall Forsberg, Olle Fredriksson, Daniel Gustafsson, Patrik Jansson, Alan Jeffrey, Wolfram Kahl, Fredrik Lindblad, Francesco Mazzoli, Stefan Monnier, Darin Morrison, Guilhem Moulin, Nicolas Pouillard, Andrés Sicard-Ramírez, Andrea Vezzosi and many more.
maintainer: Ulf Norell <ulfn@chalmers.se>
homepage: http://wiki.portal.chalmers.se/agda/
bug-reports: http://code.google.com/p/agda/issues/list
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 library does not follow the package versioning
policy, because it is not intended to be used by third-party
packages.
tested-with: GHC == 7.2.2
GHC == 7.4.2
GHC == 7.6.3
GHC == 7.8.3
extra-source-files: src/full/Agda/undefined.h
README.md
CHANGELOG
data-dir: src/data
data-files: Agda.css
emacs-mode/*.el
EpicInclude/AgdaPrelude.e
EpicInclude/stdagda.c
EpicInclude/stdagda.h
agda.sty
postprocess-latex.pl
lib/prim/Agda/Primitive.agda
source-repository head
type: git
location: https://github.com/agda/agda.git
source-repository this
type: git
location: https://github.com/agda/agda
tag: 2.4.2
flag epic
default: False
manual: True
description:
Install the Epic compiler.
library
hs-source-dirs: src/full
if flag(epic)
build-depends: epic >= 0.1.13 && < 0.10
if os(windows)
build-depends: Win32 >= 2.2 && < 2.4
build-depends: base >= 4.2 && < 4.8,
transformers == 0.3.*,
-- mtl-2.1 contains a severe bug
mtl >= 2.1.1 && < 2.2,
QuickCheck >= 2.7.5 && < 2.8,
haskell-src-exts >= 1.9.6 && < 1.16,
containers >= 0.1 && < 0.6,
unordered-containers == 0.2.*,
pretty >= 1.0 && < 1.2,
bytestring >= 0.9.0.1 && < 0.11,
array >= 0.1 && < 0.6,
binary >= 0.6 && < 0.8,
zlib >= 0.4.0.1 && < 0.6,
filepath >= 1.1 && < 1.4,
process >= 1.0.1.0 && < 1.3,
haskeline >= 0.7 && < 0.8,
data-hash == 0.2.0.0,
xhtml == 3000.2.*,
-- hashable 1.2.0.10 makes library-test 10x
-- slower. The issue was fixed in hashable 1.2.1.0.
-- https://github.com/tibbe/hashable/issues/57.
hashable >= 1.1.2.3 && < 1.2 || >= 1.2.1.0 && < 1.3,
hashtables >= 1.0 && < 1.2,
geniplate >= 0.6.0.3 && < 0.7,
-- parsec >= 3.1 && < 3.2, -- only for Agda.TypeChecking.SizedTypes.Parser, which is not included
parallel < 3.3,
deepseq == 1.3.*,
strict >= 0.3.2 && < 0.4,
STMonadTrans >= 0.3.2 && < 0.4,
equivalence >= 0.2.4 && < 0.3,
boxes >= 0.1.3 && < 0.2,
text >= 0.11 && < 1.2
if impl(ghc < 7.6)
build-depends: old-time >= 1.0 && < 1.2,
directory >= 1.0 && < 1.2
else
build-depends: time == 1.4.*,
directory == 1.2.*
build-tools: happy >= 1.19.3 && < 2,
alex >= 3.1.0 && < 3.2,
cpphs >= 1.18.5 && < 1.19
exposed-modules: Agda.Main
Agda.ImpossibleTest
Agda.Interaction.BasicOps
Agda.Interaction.EmacsTop
Agda.Interaction.InteractionTop
Agda.Compiler.CallCompiler
Agda.Compiler.HaskellTypes
Agda.Compiler.Epic.AuxAST
Agda.Compiler.Epic.CaseOpts
Agda.Compiler.Epic.Compiler
Agda.Compiler.Epic.CompileState
Agda.Compiler.Epic.Epic
Agda.Compiler.Epic.Erasure
Agda.Compiler.Epic.ForceConstrs
Agda.Compiler.Epic.Forcing
Agda.Compiler.Epic.FromAgda
Agda.Compiler.Epic.Injection
Agda.Compiler.Epic.Interface
Agda.Compiler.Epic.NatDetection
Agda.Compiler.Epic.Primitive
Agda.Compiler.Epic.Smashing
Agda.Compiler.Epic.Static
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
Agda.Compiler.MAlonzo.Misc
Agda.Compiler.MAlonzo.Pretty
Agda.Compiler.MAlonzo.Primitives
Agda.Interaction.CommandLine.CommandLine
Agda.Interaction.EmacsCommand
Agda.Interaction.Exceptions
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.Response
Agda.Interaction.MakeCase
Agda.Interaction.Monad
Agda.Interaction.Options
Agda.Interaction.Options.Lenses
Agda.Syntax.Abstract.Copatterns
Agda.Syntax.Abstract.Name
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
Agda.Syntax.Concrete.Pretty
Agda.Syntax.Concrete
Agda.Syntax.Fixity
Agda.Syntax.Info
Agda.Syntax.Internal
Agda.Syntax.Internal.Defs
Agda.Syntax.Internal.Generic
Agda.Syntax.Internal.Pattern
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.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.Scope.Base
Agda.Syntax.Scope.Monad
Agda.Syntax.Translation.AbstractToConcrete
Agda.Syntax.Translation.ConcreteToAbstract
Agda.Syntax.Translation.InternalToAbstract
Agda.Termination.CallGraph
Agda.Termination.CallMatrix
Agda.Termination.CutOff
Agda.Termination.Inlining
-- Agda.Termination.Lexicographic -- RETIRED
-- Agda.Termination.Matrix -- RETIRED
Agda.Termination.Monad
Agda.Termination.Order
Agda.Termination.RecCheck
Agda.Termination.SparseMatrix
Agda.Termination.Semiring
Agda.Termination.TermCheck
Agda.Termination.Termination
Agda.Tests
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.DisplayForm
Agda.TypeChecking.DropArgs
-- Agda.TypeChecking.Eliminators -- RETIRED
Agda.TypeChecking.Empty
Agda.TypeChecking.EtaContract
Agda.TypeChecking.Errors
Agda.TypeChecking.Free
Agda.TypeChecking.Forcing
Agda.TypeChecking.Implicit
Agda.TypeChecking.Injectivity
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.Base.Benchmark
Agda.TypeChecking.Monad.Base.KillRange
Agda.TypeChecking.Monad.Benchmark
Agda.TypeChecking.Monad.Builtin
Agda.TypeChecking.Monad.Closure
Agda.TypeChecking.Monad.Constraints
Agda.TypeChecking.Monad.Context
Agda.TypeChecking.Monad.Debug
Agda.TypeChecking.Monad.Env
Agda.TypeChecking.Monad.Exception
Agda.TypeChecking.Monad.Imports
Agda.TypeChecking.Monad.MetaVars
Agda.TypeChecking.Monad.Mutual
Agda.TypeChecking.Monad.Open
Agda.TypeChecking.Monad.Options
Agda.TypeChecking.Monad.Sharing
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 -- RETIRED
Agda.TypeChecking.Patterns.Abstract
Agda.TypeChecking.Patterns.Match
Agda.TypeChecking.Polarity
Agda.TypeChecking.Positivity
Agda.TypeChecking.Pretty
Agda.TypeChecking.Primitive
Agda.TypeChecking.ProjectionLike
Agda.TypeChecking.Quote
-- Agda.TypeChecking.Rebind -- DEAD
Agda.TypeChecking.RecordPatterns
Agda.TypeChecking.Records
Agda.TypeChecking.Reduce
Agda.TypeChecking.Reduce.Monad
Agda.TypeChecking.Rewriting
Agda.TypeChecking.Rules.Builtin
Agda.TypeChecking.Rules.Builtin.Coinduction
Agda.TypeChecking.Rules.Data
Agda.TypeChecking.Rules.Decl
Agda.TypeChecking.Rules.Def
Agda.TypeChecking.Rules.LHS
Agda.TypeChecking.Rules.LHS.Implicit
Agda.TypeChecking.Rules.LHS.Instantiate
Agda.TypeChecking.Rules.LHS.Problem
Agda.TypeChecking.Rules.LHS.ProblemRest
Agda.TypeChecking.Rules.LHS.Split
Agda.TypeChecking.Rules.LHS.Unify
Agda.TypeChecking.Rules.Record
Agda.TypeChecking.Rules.Term
Agda.TypeChecking.Serialise
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.SyntacticEquality
Agda.TypeChecking.Telescope
Agda.TypeChecking.Test.Generators
Agda.TypeChecking.Tests
-- Agda.TypeChecking.UniversePolymorphism -- RETIRED
Agda.TypeChecking.With
Agda.Utils.BiMap
Agda.Utils.Char
Agda.Utils.Cluster
Agda.Utils.Either
Agda.Utils.Favorites
Agda.Utils.FileName
Agda.Utils.Fresh
Agda.Utils.Functor
Agda.Utils.Function
Agda.Utils.Geniplate
Agda.Utils.Graph.AdjacencyMap
Agda.Utils.Graph.AdjacencyMap.Unidirectional
Agda.Utils.Hash
Agda.Utils.HashMap
Agda.Utils.Impossible
Agda.Utils.IO.Binary
Agda.Utils.IO.UTF8
Agda.Utils.List
Agda.Utils.Map
Agda.Utils.Maybe
Agda.Utils.Maybe.Strict
Agda.Utils.Monad
Agda.Utils.Null
Agda.Utils.PartialOrd
Agda.Utils.Permutation
Agda.Utils.Pointer
Agda.Utils.Pointed
Agda.Utils.Pretty
Agda.Utils.QuickCheck
Agda.Utils.ReadP
Agda.Utils.SemiRing
Agda.Utils.Size
Agda.Utils.String
Agda.Utils.Suffix
Agda.Utils.TestHelpers
Agda.Utils.Time
Agda.Utils.Trie
Agda.Utils.Tuple
Agda.Utils.Unicode
Agda.Utils.Update
Agda.Utils.VarSet
Agda.Utils.Warshall
Agda.Version
Agda.Auto.Auto
Agda.Auto.Convert
Agda.Auto.Typecheck
Agda.Auto.NarrowingSearch
Agda.Auto.Syntax
Agda.Auto.SearchControl
Agda.Auto.CaseSplit
other-modules: Paths_Agda
-- This conditional is required by GHC <= 7.4.2.
if true
ghc-options: -w
-fwarn-deprecated-flags
-fwarn-dodgy-foreign-imports
-fwarn-dodgy-imports
-fwarn-duplicate-exports
-fwarn-hi-shadowing
-fwarn-incomplete-patterns
-fwarn-missing-fields
-fwarn-missing-methods
-fwarn-monomorphism-restriction
-fwarn-overlapping-patterns
-fwarn-unrecognised-pragmas
-fwarn-warnings-deprecations
-- Using cpphs as the C preprocessor.
-pgmPcpphs -optP--cpp
-- The Cabal-generated module Paths_Agda triggers a warning under
-- GHC 7.2.1/7.2.2 (at least when certain versions of Cabal are
-- used).
-- Issue 1103: Termination.SparseMatrix triggers a warning under GHC 7.0.4.
-- -Werror is for developers only, who are assumed to use a recent GHC.
-- if impl(ghc > 7.2.2)
-- ghc-options: -Werror
if impl(ghc >= 6.12)
ghc-options: -fwarn-dodgy-exports
-fwarn-wrong-do-bind
if impl(ghc >= 7.2)
ghc-options: -fwarn-identities
if impl(ghc >= 7.6.3)
ghc-options: -fwarn-pointless-pragmas
if impl(ghc >= 7.8)
ghc-options: -fwarn-amp
-fwarn-duplicate-constraints
-fwarn-empty-enumerations
-fwarn-overflowed-literals
-fwarn-typed-holes
-fwarn-inline-rule-shadowing
ghc-prof-options: -auto-all
executable agda
hs-source-dirs: src/main
main-is: Main.hs
build-depends: Agda == 2.4.2,
-- Nothing is used from the following package, except
-- for the prelude.
base >= 3 && < 6
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.2 && < 4.8,
filepath >= 1.1 && < 1.4,
process >= 1.0.1.0 && < 1.3,
directory >= 1.0 && < 1.3