forked from agda/agda
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Agda.cabal
547 lines (521 loc) · 22.6 KB
/
Agda.cabal
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
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
name: Agda
version: 2.4.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 <[email protected]>
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.6.3
GHC == 7.8.4
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
uhc-agda-base/LICENSE
uhc-agda-base/uhc-agda-base.cabal
uhc-agda-base/src/UHC/Agda/*.hs
source-repository head
type: git
location: https://github.com/agda/agda.git
flag cpphs
default: True
manual: True
description: Use cpphs instead of cpp.
flag uhc
default: False
manual: True
description:
Install the UHC backend (requires GHC 7.6 or newer).
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 flag(uhc)
build-depends: uhc-light >= 1.1.9.0 && < 1.2
, uhc-util >= 0.1.5.5
, uulib >= 0.9.20
cpp-options: -DUHC_BACKEND
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.9
, binary >= 0.7.2.1 && < 0.8
, 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
, 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.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
-- 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.3
, strict >= 0.3.2 && < 0.4
, template-haskell >= 2.8.0.0 && < 2.11
, text >= 0.11.3.1 && < 1.3
, time >= 1.4.0.1 && < 1.6
-- transformers 0.4.0.0 was deprecated.
, transformers >= 0.3 && < 0.4 || >= 0.4.1.0 && < 0.5
, transformers-compat >= 0.3.3.3 && < 0.5
, unordered-containers >= 0.2.5.0 && < 0.3
, xhtml >= 3000.2.1 && < 3000.3
-- zlib >= 0.6.1 is broken. See Issue 1518.
, zlib >= 0.4.0.1 && < 0.6.1
if impl(ghc < 7.8)
build-depends: base-orphans >= 0.3.1 && < 0.5
build-tools:
alex >= 3.1.0 && < 3.2
, happy >= 1.19.4 && < 2
-- required to make the code compile, as the EH library is not present when the uhc backend is disabled
if flag(uhc)
cpp-options: -DUHC_BACKEND
exposed-modules: Agda.Auto.Auto
Agda.Auto.CaseSplit
Agda.Auto.Convert
Agda.Auto.NarrowingSearch
Agda.Auto.SearchControl
Agda.Auto.Syntax
Agda.Auto.Typecheck
Agda.Benchmarking
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.Compiler.ToTreeless
Agda.Compiler.Treeless.NPlusK
Agda.Compiler.Treeless.Simplify
Agda.Compiler.Treeless.Subst
Agda.Compiler.UHC.AuxAST
Agda.Compiler.UHC.AuxASTUtil
Agda.Compiler.UHC.Bridge
Agda.Compiler.UHC.Compiler
Agda.Compiler.UHC.CompileState
Agda.Compiler.UHC.Core
Agda.Compiler.UHC.FromAgda
Agda.Compiler.UHC.MagicTypes
Agda.Compiler.UHC.ModuleInfo
Agda.Compiler.UHC.Naming
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
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.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.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.Empty
Agda.TypeChecking.EtaContract
Agda.TypeChecking.Errors
Agda.TypeChecking.Free
Agda.TypeChecking.Free.Lazy
Agda.TypeChecking.Free.Old
Agda.TypeChecking.Free.Tests
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.Benchmark
Agda.TypeChecking.Monad.Builtin
Agda.TypeChecking.Monad.Caching
Agda.TypeChecking.Monad.Closure
Agda.TypeChecking.Monad.Constraints
Agda.TypeChecking.Monad.Context
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.Abstract
Agda.TypeChecking.Patterns.Match
Agda.TypeChecking.Polarity
Agda.TypeChecking.Positivity
Agda.TypeChecking.Positivity.Occurrence
Agda.TypeChecking.Positivity.Tests
Agda.TypeChecking.Pretty
Agda.TypeChecking.Primitive
Agda.TypeChecking.ProjectionLike
Agda.TypeChecking.Quote
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.Display
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.Main
Agda.TypeChecking.SizedTypes.Parser
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.Unquote
Agda.TypeChecking.With
Agda.Utils.AssocList
Agda.Utils.Bag
Agda.Utils.Benchmark
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.Unidirectional
Agda.Utils.Graph.AdjacencyMap.Unidirectional.Tests
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.Maybe
Agda.Utils.Maybe.Strict
Agda.Utils.Monad
Agda.Utils.Null
Agda.Utils.Parser.MemoisedCPS
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
Agda.Utils.Update
Agda.Utils.VarSet
Agda.Utils.Warshall
Agda.Version
other-modules: Paths_Agda
if impl(ghc >= 7.6.3)
ghc-options: -w
-Werror
-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-orphans
-fwarn-pointless-pragmas
-fwarn-tabs
-fwarn-overlapping-patterns
-fwarn-unrecognised-pragmas
-fwarn-unused-do-bind
-fwarn-warnings-deprecations
-fwarn-wrong-do-bind
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
ghc-prof-options: -fprof-auto
executable agda
hs-source-dirs: src/main
main-is: Main.hs
build-depends:
Agda == 2.4.3
-- Nothing is used from the following package, except for the
-- prelude.
, base >= 4.6.0.1 && < 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.6.0.1 && < 4.9
, directory >= 1.2.0.1 && < 1.3
, filepath >= 1.3.0.1 && < 1.5
, process >= 1.1.0.2 && < 1.3
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.9
, binary >= 0.7.2.1 && < 0.8
, containers >= 0.5.0.0 && < 0.6
, filemanip >= 0.3.6.3 && < 0.4
, haskell-src-exts >= 1.16.0.1 && < 1.17
, mtl >= 2.1.1 && <= 2.1.3.1 || >= 2.2.1 && < 2.3
, filepath >= 1.3.0.1 && < 1.5
-- Cabal testsuite integration has some serious bugs, but we
-- can still make it work. See also:
-- https://github.com/haskell/cabal/issues/1938
-- https://github.com/haskell/cabal/issues/2214
-- https://github.com/haskell/cabal/issues/1953
--
-- This test suite should only be run using the Makefile.
-- The Makefile sets up the required environment,
-- executing the tests using cabal directly is almost
-- guarantued to fail. See also Issue 1490.
test-suite agda-tests
type: exitcode-stdio-1.0
hs-source-dirs: test/
main-is: Main.hs
other-modules: Compiler.Tests
, LatexBackend.Tests
, Utils
build-depends: base >= 4.6.0.1 && < 4.9
, bytestring >= 0.10.0.2 && < 0.11
, directory >= 1.2.0.1 && < 1.3
, containers >= 0.5.0.0 && < 0.6
, filepath >= 1.3.0.1 && < 1.5
, process >= 1.1.0.2 && < 1.3
, process-extras >= 0.2.0 && < 0.4
, tasty >= 0.10 && < 0.11
, tasty-silver >= 3.1.7 && < 3.2
, temporary >= 1.2.0.3 && < 1.3
, text >= 0.11.3.1 && < 1.3
if flag(uhc)
cpp-options: -DUHC_BACKEND
ghc-options: -threaded -Wall -Werror