/
Agda.cabal
319 lines (297 loc) · 9.77 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
cabal-version: 2.4
name: Agda
version: 2.6.4
build-type: Simple
data-dir:
src/data
data-files:
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/Cubical/Equiv.agda
lib/prim/Agda/Builtin/Cubical/HCompU.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/Float/Properties.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/Maybe.agda
lib/prim/Agda/Builtin/Nat.agda
lib/prim/Agda/Builtin/Reflection.agda
lib/prim/Agda/Builtin/Reflection/External.agda
lib/prim/Agda/Builtin/Reflection/Properties.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/Builtin/Word/Properties.agda
lib/prim/Agda/Primitive.agda
lib/prim/Agda/Primitive/Cubical.agda
-- Build flags
---------------------------------------------------------------------------
flag debug
default: False
manual: True
description:
Enable debugging features that may slow Agda down.
flag optimise-heavily
default: False
description:
Enable some expensive optimisations when compiling Agda.
-- Common stanzas
---------------------------------------------------------------------------
common language
if flag(optimise-heavily)
cpp-options:
-DOPTIMISE_HEAVILY
ghc-options:
-fexpose-all-unfoldings
-fspecialise-aggressively
default-language: Haskell2010
-- NOTE: If adding or removing default extensions, also change:
-- .hlint.yaml
default-extensions:
BangPatterns
BlockArguments
ConstraintKinds
--L-T Chen (2019-07-15):
-- Enabling DataKinds only locally makes the compile time
-- slightly shorter, see PR #3920.
-- DataKinds
DefaultSignatures
DeriveFoldable
DeriveFunctor
DeriveGeneric
DeriveTraversable
DerivingStrategies
ExistentialQuantification
FlexibleContexts
FlexibleInstances
FunctionalDependencies
GeneralizedNewtypeDeriving
InstanceSigs
LambdaCase
MultiParamTypeClasses
MultiWayIf
NamedFieldPuns
OverloadedStrings
PatternSynonyms
RankNTypes
RecordWildCards
ScopedTypeVariables
StandaloneDeriving
TupleSections
TypeFamilies
TypeOperators
TypeSynonymInstances
other-extensions:
CPP
DeriveAnyClass
PartialTypeSignatures
if flag(debug)
cpp-options: -DDEBUG
if os(windows)
build-depends: Win32 >= 2.6.1.0 && < 2.14
-- For libraries that come with GHC, we take the shipped version as default lower bound.
build-depends:
, aeson >= 1.1.2.0 && < 2.3
, array >= 0.5.2.0 && < 0.6
, async >= 2.2 && < 2.3
, base >= 4.12.0.0 && < 4.19
, binary >= 0.8.6.0 && < 0.9
, blaze-html >= 0.8 && < 0.10
, boxes >= 0.1.3 && < 0.2
, bytestring >= 0.10.8.2 && < 0.12
, case-insensitive >= 1.2.0.4 && < 1.3
, containers >= 0.6.0.1 && < 0.7
, data-hash >= 0.2.0.0 && < 0.3
, deepseq >= 1.4.4.0 && < 1.5
, directory >= 1.3.3.0 && < 1.4
, dlist >= 0.8 && < 1.1
, edit-distance >= 0.2.1.2 && < 0.3
, equivalence >= 0.3.2 && < 0.5
-- exceptions-0.8 instead of 0.10 because of stack
, exceptions >= 0.8 && < 0.11
, filepath >= 1.4.2.1 && < 1.5
, ghc-compact == 0.1.*
, 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.5
, haskeline >= 0.7.4.3 && < 0.9
-- monad-control-1.0.1.0 is the first to contain liftThrough
, monad-control >= 1.0.1.0 && < 1.1
, mtl >= 2.2.2 && < 2.4
, murmur-hash >= 0.1 && < 0.2
, parallel >= 3.2.2.0 && < 3.3
, peano >= 0.1.0.1 && < 0.2
, pretty >= 1.1.3.3 && < 1.2
, process >= 1.6.3.0 && < 1.7
, regex-tdfa >= 1.3.1.0 && < 1.4
, split >= 0.2.0.0 && < 0.2.4
, stm >= 2.4.4 && < 2.6
, STMonadTrans >= 0.4.3 && < 0.5
, strict >= 0.4.0.1 && < 0.6
, text >= 1.2.3.1 && < 2.1
, time >= 1.8.0.2 && < 1.13
, time-compat >= 1.9.2 && < 1.10
-- time-compat adds needed functionality missing in time < 1.9
, transformers >= 0.5.5.0 && < 0.7
, unordered-containers >= 0.2.9.0 && < 0.3
-- unordered-containers < 0.2.9 need base < 4.11
, uri-encode >= 1.5.0.4 && < 1.6
, vector >= 0.12 && < 0.14
, vector-hashtables == 0.1.*
, zlib == 0.6.*
executable agda
import: language
main-is: Main.hs
hs-source-dirs:
src/full
src/main
-- exposed-modules:
other-modules:
Agda.Benchmarking
Agda.ImpossibleTest
Agda.Interaction.Base
Agda.Interaction.ExitCode
Agda.Interaction.FindFile
Agda.Interaction.Library.Base
Agda.Interaction.Monad
Agda.Interaction.Options
Agda.Interaction.Options.Base
Agda.Interaction.Options.HasOptions
Agda.Interaction.Options.Help
Agda.Interaction.Options.Lenses
Agda.Interaction.Options.Warnings
Agda.Syntax.Abstract
Agda.Syntax.Abstract.Name
Agda.Syntax.Abstract.Pattern
Agda.Syntax.Abstract.PatternSynonyms
Agda.Syntax.Abstract.Pretty
Agda.Syntax.Abstract.Views
Agda.Syntax.Builtin
Agda.Syntax.Common
Agda.Syntax.Concrete
Agda.Syntax.Concrete.Fixity
Agda.Syntax.Concrete.Glyph
Agda.Syntax.Concrete.Name
Agda.Syntax.Concrete.Pattern
Agda.Syntax.Concrete.Pretty
Agda.Syntax.Fixity
Agda.Syntax.Info
Agda.Syntax.Internal
Agda.Syntax.Internal.Elim
Agda.Syntax.Internal.Generic
Agda.Syntax.Internal.MetaVars
Agda.Syntax.Internal.Names
Agda.Syntax.Internal.Univ
Agda.Syntax.Literal
Agda.Syntax.Notation
Agda.Syntax.Position
Agda.Syntax.Scope.Base
Agda.Syntax.Scope.Monad
Agda.Syntax.TopLevelModuleName
Agda.Syntax.Translation.AbstractToConcrete
Agda.TypeChecking.CompiledClause
Agda.TypeChecking.Coverage.SplitTree
Agda.TypeChecking.Errors
Agda.TypeChecking.Free
Agda.TypeChecking.Free.Lazy
Agda.TypeChecking.Monad
Agda.TypeChecking.Monad.Base
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.Imports
Agda.TypeChecking.Monad.MetaVars
Agda.TypeChecking.Monad.Options
Agda.TypeChecking.Monad.Pure
Agda.TypeChecking.Monad.Signature
Agda.TypeChecking.Monad.State
Agda.TypeChecking.Monad.Trace
Agda.TypeChecking.Positivity.Occurrence
Agda.TypeChecking.Pretty
Agda.TypeChecking.Pretty.Call
Agda.TypeChecking.Pretty.Warning
Agda.TypeChecking.Reduce.Monad
Agda.TypeChecking.Substitute
Agda.TypeChecking.Substitute.Class
Agda.TypeChecking.Substitute.DeBruijn
Agda.TypeChecking.Warnings
Agda.Utils.AffineHole
Agda.Utils.Applicative
Agda.Utils.AssocList
Agda.Utils.Bag
Agda.Utils.Benchmark
Agda.Utils.BiMap
Agda.Utils.Boolean
Agda.Utils.CallStack
Agda.Utils.CallStack.Base
Agda.Utils.CallStack.Pretty
Agda.Utils.Either
Agda.Utils.Empty
Agda.Utils.FileName
Agda.Utils.Float
Agda.Utils.Function
Agda.Utils.Functor
Agda.Utils.Graph.AdjacencyMap.Unidirectional
Agda.Utils.Hash
Agda.Utils.IO.UTF8
Agda.Utils.Impossible
Agda.Utils.Lens
Agda.Utils.List
Agda.Utils.List1
Agda.Utils.List2
Agda.Utils.ListT
Agda.Utils.Map
Agda.Utils.Maybe
Agda.Utils.Maybe.Strict
Agda.Utils.Memo
Agda.Utils.Monad
Agda.Utils.Null
Agda.Utils.POMonoid
Agda.Utils.Parser.MemoisedCPS
Agda.Utils.PartialOrd
Agda.Utils.Permutation
Agda.Utils.Pretty
Agda.Utils.ProfileOptions
Agda.Utils.SemiRing
Agda.Utils.Semigroup
Agda.Utils.Singleton
Agda.Utils.Size
Agda.Utils.SmallSet
Agda.Utils.String
Agda.Utils.Suffix
Agda.Utils.Time
Agda.Utils.Trie
Agda.Utils.Tuple
Agda.Utils.TypeLevel
Agda.Utils.TypeLits
Agda.Utils.Update
Agda.Utils.WithDefault
Agda.Version
autogen-modules:
Paths_Agda
other-modules:
Paths_Agda