-
Notifications
You must be signed in to change notification settings - Fork 26
/
cogent.cabal
337 lines (310 loc) · 9.88 KB
/
cogent.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
cabal-version: 3.0
-- ^^^ `cabal-version` is not the version of cabal-install nor
-- that of the Cabal library. It's the cabal specification version.
-- c.f. https://www.haskell.org/cabal/users-guide/file-format-changelog.html#spec-history
-- Initial cogent.cabal generated by cabal init. For further documentation,
-- see http://haskell.org/cabal/users-guide/
name: cogent
version: 3.0.2
-- synopsis:
-- description:
-- license:
-- license-file: LICENSE
author: The Cogent Team and Contributors
maintainer: Zilin Chen <zilin.chen@student.unsw.edu.au>
homepage: https://trustworthy.systems/projects/TS/cogent.pml
bug-reports: https://github.com/au-ts/cogent/issues
-- copyright:
-- category:
build-type: Custom
tested-with: GHC==8.4.3, GHC==8.6.5, GHC==8.8.3, GHC==8.10.4, GHC==9.0.1
data-files:
static/jquery.min.js
static/style.css
static/toc.min.js
static/logo.png
lib/cogent-defns.h
lib/cogent-endianness.h
lib/gum/common/*.cogent
lib/gum/fs/linux/*.cogent
lib/gum/kernel/linux/*.cogent
lib/gum/test/test.cogent
lib/gum/anti/*.ac
lib/gum/anti/abstract/*.ah
lib/c/linux/abstract-defns.h
lib/c/rbt.h
isa/ROOT
isa/*.thy
flag builtin-arrays
description: Enable experimental arrays with SMT solving
manual: True
default: False
flag refinement-types
description: Enable experimental refinement types features
manual: True
default: False
flag docgent
description: Enable documentation generator (drastically embiggens build time)
manual: True
default: False
flag haskell-backend
description: Enable PBT/Haskell backend
manual: True
default: False
flag llvm-backend
description: Enable LLVM backend
manual: True
default: False
source-repository head
type: git
location: https://github.com/NICTA/cogent/
custom-setup
setup-depends:
base >= 4.10 && < 4.17
, Cabal >= 3.0
-- ^^^ 3.0 is needed as we use Cabal in Setup.hs
, directory >= 1.2
, filepath >= 1.4.0.0
, process >= 1.2.0.0
library
hs-source-dirs: src
exposed-modules:
Cogent.C
, Cogent.C.Expr
, Cogent.C.Monad
, Cogent.C.Render
, Cogent.C.Syntax
, Cogent.C.Type
, Cogent.Common.Syntax
, Cogent.Common.Types
, Cogent.Compiler
, Cogent.Context
, Cogent.Core
, Cogent.Dargent.Allocation
, Cogent.Dargent.CodeGen
, Cogent.Dargent.Core
, Cogent.Dargent.Desugar
, Cogent.Dargent.Surface
, Cogent.Dargent.TypeCheck
, Cogent.Dargent.Util
, Cogent.Desugar
, Cogent.Flags
, Cogent.GetOpt
, Cogent.Glue
, Cogent.Inference
, Cogent.Interpreter
, Cogent.Isabelle
, Cogent.Isabelle.ACInstall
, Cogent.Isabelle.AllRefine
, Cogent.Isabelle.Compound
, Cogent.Isabelle.CorresProof
, Cogent.Isabelle.CorresSetup
, Cogent.Isabelle.Deep
, Cogent.Isabelle.GraphGen
, Cogent.Isabelle.MonoProof
, Cogent.Isabelle.NormalProof
, Cogent.Isabelle.ProofGen
, Cogent.Isabelle.Root
, Cogent.Isabelle.Shallow
, Cogent.Isabelle.ShallowTable
, Cogent.Isabelle.TypeProofs
, Cogent.Isabelle.IsabelleName
, Cogent.Mono
, Cogent.Normal
, Cogent.Parser
, Cogent.PrettyPrint
, Cogent.Preprocess
, Cogent.Quote
, Cogent.Reorganizer
, Cogent.Simplify
, Cogent.SuParser
, Cogent.Surface
, Cogent.TypeCheck
, Cogent.TypeCheck.ARow
, Cogent.TypeCheck.Base
, Cogent.TypeCheck.Errors
, Cogent.TypeCheck.Generator
, Cogent.TypeCheck.LRow
, Cogent.TypeCheck.Post
, Cogent.TypeCheck.Row
, Cogent.TypeCheck.Solver
, Cogent.TypeCheck.Solver.Simplify
, Cogent.TypeCheck.Solver.Unify
, Cogent.TypeCheck.Solver.Normalise
, Cogent.TypeCheck.Solver.Equate
, Cogent.TypeCheck.Solver.Goal
, Cogent.TypeCheck.Solver.Monad
, Cogent.TypeCheck.Solver.Rewrite
, Cogent.TypeCheck.Solver.SinkFloat
, Cogent.TypeCheck.Solver.Default
, Cogent.TypeCheck.Solver.Util
, Cogent.TypeCheck.Subst
, Cogent.TypeCheck.Util
, Cogent.Util
, Data.Bwd
, Data.DList
, Data.Ex
, Data.Fin
, Data.LeafTree
, Data.Nat
, Data.OMap
, Data.PropEq
, Data.Vec
-- Generated
, Paths_cogent
, Version_cogent
autogen-modules:
Paths_cogent
, Version_cogent
build-depends:
ansi-wl-pprint >= 0.6
, base >= 4.10 && < 4.17
, binary
, bytestring >= 0.10
, containers >= 0.5.8
, cpphs >= 1.19
, directory >= 1.2
, filepath >= 1.4.0.0
, graph-wrapper >= 0.2
, isa-parser >= 0.1.0.0
, language-c-quote >= 0.10.2
, mainland-pretty >= 0.2.6
, microlens >= 0.4.9
, microlens-ghc >= 0.4.9
, microlens-mtl >= 0.1.11
, microlens-th >= 0.4.1
, mtl >= 2.2.1
, parsec >= 3.1
, pretty-show-ansi-wl >= 1.5
, srcloc >= 0.4
, syb >= 0.4
, template-haskell
, transformers >= 0.4.2
if flag(haskell-backend)
exposed-modules: Cogent.Haskell.FFIGen
, Cogent.Haskell.HscGen
, Cogent.Haskell.HscSyntax
, Cogent.Haskell.Shallow
cpp-options: -DWITH_HASKELL
build-depends: haskell-src-exts >= 1.19, pretty
if flag(llvm-backend)
exposed-modules: Cogent.LLVM.Compile
cpp-options: -DWITH_LLVM
build-depends: llvm-hs >= 9.0.1, llvm-hs-pure >= 9.0.0
if flag(builtin-arrays) || flag(refinement-types)
exposed-modules:
Cogent.TypeCheck.SMT
, Cogent.TypeCheck.Solver.SMT
build-depends: sbv >= 8.0
if flag(builtin-arrays)
cpp-options: -DBUILTIN_ARRAYS
if flag(refinement-types)
cpp-options: -DREFINEMENT_TYPES
if flag(docgent)
cpp-options: -DWITH_DOCGENT
build-depends: ansi-terminal >= 0.6
, pandoc >= 1.19.2.4
, pandoc-types >= 1.16
, shakespeare >= 2.0
, text >= 0.11.3.1
, data-default >=0.5
, blaze-html >= 0.8.1
, blaze-markup >= 0.7
exposed-modules: Cogent.DocGent
default-language: Haskell2010
default-extensions: CPP
build-tool-depends:
alex:alex
, happy:happy
ghc-options:
-- -Wall
-- -Werror
-fno-warn-name-shadowing
-fno-warn-missing-signatures
-fno-warn-unused-matches
-O2
-optP-Wno-nonportable-include-path
-- -rtsopts
-- +RTS -K256M
-- if impl(ghc >= 7.10.1)
-- ghc-options: -fno-warn-unticked-promoted-constructors
Executable cogent
main-is: Main.hs
build-depends:
cogent
, ansi-wl-pprint >= 0.6
, atomic-write >= 0.2.0.4
, base >= 4.10 && < 4.17
, binary
, containers >= 0.5.8
, directory >=1.2
, filepath >= 1.4.0.0
, mainland-pretty >= 0.2.6
, pretty-show-ansi-wl >= 1.5
, process >= 1.2.0.0
, text >= 0.11.3.1
, time >= 1.5
, transformers >= 0.4.2
, microlens >= 0.4.8
if flag(llvm-backend)
cpp-options: -DWITH_LLVM
if flag(haskell-backend)
cpp-options: -DWITH_HASKELL
if flag(builtin-arrays)
cpp-options: -DBUILTIN_ARRAYS
if flag(docgent)
cpp-options: -DWITH_DOCGENT
default-language: Haskell2010
default-extensions: CPP
build-tool-depends:
alex:alex
, happy:happy
ghc-options:
-Wall
-- -Werror
-fno-warn-name-shadowing
-fno-warn-missing-signatures
-fno-warn-unused-matches
-O2
-optP-Wno-nonportable-include-path
-- -rtsopts
-- +RTS -K256M
-- if impl(ghc >= 7.10.1)
-- ghc-options: -fno-warn-unticked-promoted-constructors
test-suite test-util
type: exitcode-stdio-1.0
default-language: Haskell2010
default-extensions: CPP
main-is: test-util.hs
build-depends:
cogent
, base >= 4.10 && < 4.17
, containers >= 0.5.8
, directory >=1.2
, filepath >= 1.4.0.0
, mtl >= 2.2.1
test-suite test-quickcheck
buildable: True
type: exitcode-stdio-1.0
default-language: Haskell2010
default-extensions: CPP
main-is: tests-quickcheck-run.hs
hs-source-dirs: tests-quickcheck .
other-modules:
CogentTests.Dargent.Core
, CogentTests.Dargent.Surface
, CogentTests.Dargent.TypeCheck
, CogentTests.Dargent.Desugar
, CogentTests.Dargent.CodeGen
, CogentTests.Core
build-depends:
cogent
, base >= 4.10 && < 4.17
, Cabal >= 3.0
, containers >= 0.5.8
, mainland-pretty >= 0.2.6
, parsec >= 3.1
, QuickCheck >= 2.11.3
, transformers
, mtl >= 2.2.1
, ansi-wl-pprint >= 0.6