summaryrefslogtreecommitdiff
path: root/Agda.cabal
blob: 6d207af845507e4b28d2c883179ab479a65adc4b (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
name:            Agda
version:         2.4.2.3
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, Philipp Hausmann, 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&#xf6;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.4.2
                    GHC == 7.6.3
                    GHC == 7.8.4
                    GHC == 7.10.1
extra-source-files: src/full/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.3

flag cpphs
  default:     True
  manual:      True
  description: Use cpphs instead of cpp.

library
  hs-source-dirs:   src/full
  include-dirs:     src/full

  if flag(cpphs)
    build-tools: cpphs >= 1.19 && < 1.20
    ghc-options: -pgmP cpphs -optP --cpp

  if os(windows)
    build-depends:  Win32 >= 2.2 && < 2.4

  build-depends:
    array >= 0.4.0.0 && < 0.6
    , base >= 4.5.0.0 && < 4.9
    , binary >= 0.6 && < 0.8
    , boxes >= 0.1.3 && < 0.2
    -- NFData ByteString is only available from bytestring >= 0.10
    -- but bytestring-0.10 is not accepted by travis build for GHC <= 7.4
    -- as it breaks the accompanying haskell-platform
    -- even though it builds with older GHCs.
    , bytestring >= 0.9.2.1 && < 0.11
    , containers >= 0.4.2.1 && < 0.6
    , data-hash == 0.2.0.0
    , deepseq >= 1.3.0.0 && < 1.5
    , edit-distance >= 0.2.1.2 && < 0.3
    , equivalence >= 0.2.5  && < 0.4
    , filepath >= 1.3.0.0 && < 1.5
    , geniplate-mirror >= 0.6.0.6 && < 0.7
    -- 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
    -- 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.2 || >= 1.2.0.2 && < 1.3
    , haskeline >= 0.7 && < 0.8
    , haskell-src-exts >= 1.16.0.1 && < 1.17
    -- 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.9
    , parallel >= 3.2.0.4 && < 3.3
    -- , parsec >= 3.1 && < 3.2,  -- only for Agda.TypeChecking.SizedTypes.Parser, which is not included

    -- 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.1 && < 1.3
    , strict >= 0.3.2 && < 0.4
    , template-haskell >= 2.7.0.0 && < 2.11
    , text >= 0.11 && < 1.3
    -- transformers 0.4.0.0 was deprecated.
    , transformers >= 0.3 && < 0.4 || >= 0.4.1.0 && < 0.5
    , transformers-compat >= 0.3.3.2 && < 0.5
    , unordered-containers == 0.2.*
    , xhtml == 3000.2.*
    , zlib >= 0.4.0.1 && < 0.7

  if impl(ghc < 7.8)
    build-depends: base-orphans >= 0.3.1 && < 0.4

  if impl(ghc < 7.6)
    build-depends:
      directory >= 1.1.0.2 && < 1.2
      -- The package ghc-prim is included in order to get access to
      -- GHC.Generics, which later moved to base.
      , ghc-prim == 0.2.*
      , old-time >= 1.1.0.0 && < 1.2
  else
      build-depends:
        directory >= 1.2.0.0 && < 1.3
        , time >= 1.4 && < 1.6

  build-tools:
    alex >= 3.1.0 && < 3.2
    , happy >= 1.19.4 && < 2

  exposed-modules:  Agda.Auto.Auto
                    Agda.Auto.CaseSplit
                    Agda.Auto.Convert
                    Agda.Auto.NarrowingSearch
                    Agda.Auto.SearchControl
                    Agda.Auto.Syntax
                    Agda.Auto.Typecheck
                    Agda.Compiler.CallCompiler
                    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.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
                    Agda.Compiler.MAlonzo.Misc
                    Agda.Compiler.MAlonzo.Pretty
                    Agda.Compiler.MAlonzo.Primitives
                    Agda.ImpossibleTest
                    Agda.Interaction.BasicOps
                    Agda.Interaction.CommandLine
                    Agda.Interaction.EmacsCommand
                    Agda.Interaction.EmacsTop
                    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.InteractionTop
                    Agda.Interaction.Response
                    Agda.Interaction.MakeCase
                    Agda.Interaction.Monad
                    Agda.Interaction.Options
                    Agda.Interaction.Options.Lenses
                    Agda.Main
                    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.Rewriting.NonLinMatch
                    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.Unquote
                    Agda.TypeChecking.With
                    Agda.Utils.AssocList
                    Agda.Utils.Bag
                    Agda.Utils.BiMap
                    Agda.Utils.Char
                    Agda.Utils.Cluster
                    Agda.Utils.Empty
                    Agda.Utils.Except
                    Agda.Utils.Either
                    Agda.Utils.Favorites
                    Agda.Utils.FileName
                    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.IORef
                    Agda.Utils.Lens
                    Agda.Utils.Lens.Examples
                    Agda.Utils.List
                    Agda.Utils.ListT
                    Agda.Utils.ListT.Tests
                    Agda.Utils.Map
                    Agda.Utils.Map.Compat
                    Agda.Utils.Maybe
                    Agda.Utils.Maybe.Strict
                    Agda.Utils.Monad
                    Agda.Utils.Null
                    Agda.Utils.PartialOrd
                    Agda.Utils.Permutation
                    Agda.Utils.Permutation.Tests
                    Agda.Utils.Pointer
                    Agda.Utils.Pretty
                    Agda.Utils.QuickCheck
                    Agda.Utils.ReadP
                    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
                    Agda.Utils.Update
                    Agda.Utils.VarSet
                    Agda.Utils.Warshall
                    Agda.Version

  other-modules:    Paths_Agda

  if impl(ghc >= 7.4.2)
    ghc-options: -w
                 -fwarn-deprecated-flags
                 -fwarn-dodgy-exports
                 -fwarn-dodgy-foreign-imports
                 -fwarn-dodgy-imports
                 -fwarn-duplicate-exports
                 -fwarn-hi-shadowing
                 -fwarn-identities
                 -fwarn-incomplete-patterns
                 -fwarn-missing-fields
                 -fwarn-missing-methods
                 -fwarn-missing-signatures
                 -fwarn-monomorphism-restriction
                 -fwarn-tabs
                 -fwarn-overlapping-patterns
                 -fwarn-unrecognised-pragmas
                 -fwarn-unused-do-bind
                 -fwarn-warnings-deprecations
                 -fwarn-wrong-do-bind

  if impl(ghc >= 7.6.3)
    ghc-options: -fwarn-pointless-pragmas

  if impl(ghc >= 7.8)
    ghc-options: -fwarn-duplicate-constraints
                 -fwarn-empty-enumerations
                 -fwarn-overflowed-literals
                 -fwarn-typed-holes
                 -fwarn-inline-rule-shadowing

  if impl(ghc >= 7.10)
     ghc-options: -fwarn-context-quantification
                  -fwarn-unticked-promoted-constructors

  -- The -fwarn-amp flag is deprected in GHC 7.10.1.
  if impl(ghc >= 7.8) && impl(ghc < 7.10)
    ghc-options: -fwarn-amp

executable agda
  hs-source-dirs: src/main
  main-is:        Main.hs
  build-depends:
    Agda == 2.4.2.3
    -- 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.5.0.0 && < 4.9
    , directory >= 1.1.0.2 && < 1.3
    , filepath >= 1.3.0.0 && < 1.5
    , process >= 1.0.1.0 && < 1.3