-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathapia.cabal
290 lines (265 loc) · 10.4 KB
/
apia.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
name: apia
version: 1.0.3
build-type: Simple
cabal-version: >= 1.10
author: Andrés Sicard-Ramírez with contributions by Jonathan Prieto-Cubides
license: MIT
license-file: LICENSE
maintainer: Andrés Sicard-Ramírez <[email protected]>
category: Dependent types
homepage: https://github.com/asr/apia
bug-reports: https://github.com/asr/apia/issues/
synopsis: Program for proving first-order formulae written in Agda using ATPs
tested-with: GHC == 8.4.3
GHC == 8.2.2
GHC == 8.0.2
GHC == 7.10.3
description:
This package provides a program for proving first-order
theorems written in the dependently typed language Agda
<http://wiki.portal.chalmers.se/agda/pmwiki.php> using first-order
automatic theorem provers (ATPs), via the translation of the Agda
formulae to the TPTP format which is a standard for input and output
for the ATPs <http://www.cs.miami.edu/~tptp/>.
extra-source-files:
src/Apia/undefined.h
README.md
data-dir: src/data
data-files: apia.yml
source-repository head
type: git
location: git://github.com/asr/apia.git
executable apia
main-is: Apia/Main.hs
hs-source-dirs: src
include-dirs: src/Apia
default-language: Haskell2010
default-extensions: NoImplicitPrelude
build-depends: Agda == 2.6.0.1
, base >= 4.8.0.0 && < 4.12
, bytestring >= 0.10.6.0 && < 0.11
, containers >= 0.5.6.2 && < 0.6
, deepseq >= 1.4.1.1 && < 1.5
, directory >= 1.2.2.0 && < 1.4
, filepath >= 1.4.0.0 && < 1.5
, ghc-prim >= 0.3.0.0 && < 0.6
, mtl >= 2.2.1 && < 2.3
-- pretty 1.1.1.2 and 1.1.1.3 do not follow the
-- package versioning policy.
, pretty >= 1.1.2.0 && < 1.2
, process >= 1.2.3.0 && < 1.7
, regex-compat >= 0.95.1 && < 0.96
, safe >= 0.3.5 && < 0.4
, text >= 0.11.3.1 && < 1.3
, unordered-containers >= 0.2.5.0 && < 0.3
, yaml >= 0.8.17 && < 0.9
-- We don't write an upper bound for cpphs because the `build-tools`
-- field can not be modified in Hackage.
-- If your change the lower bound of cpphs also change it in the
-- `.travis.yml` file.
build-tools: cpphs >= 1.20.8
other-modules:
Apia.ATPs
Apia.CheckTPTP
Apia.Common
Apia.Defaults
Apia.Dump
Apia.FOL.Constants
Apia.FOL.Primitives
Apia.FOL.Types
Apia.Monad.Base
Apia.Monad.Environment
Apia.Monad.Reports
Apia.Monad.Utils
Apia.Options
Apia.Prelude
Apia.Snapshot
Apia.TPTP.ConcreteSyntax
Apia.TPTP.Files
Apia.TPTP.Types
Apia.Translation
Apia.Translation.Functions
Apia.Translation.Terms
Apia.Translation.Types
Apia.Utils.AgdaAPI.DeBruijn
Apia.Utils.AgdaAPI.EtaExpansion
Apia.Utils.AgdaAPI.IgnoreSharing
Apia.Utils.AgdaAPI.Interface
Apia.Utils.AgdaAPI.RemoveProofTerms
Apia.Utils.AgdaAPI.Vars
Apia.Utils.Except
Apia.Utils.IO
Apia.Utils.List
Apia.Utils.Monad
Apia.Utils.Name
Apia.Utils.PrettyPrint
Apia.Utils.Show
Apia.Utils.String
Apia.Utils.Text
Apia.Utils.CommitVersion
Apia.Utils.Version
Paths_apia
ghc-options: -w
-Werror
-- Using cpphs as the C preprocessor.
-pgmP cpphs -optP --cpp
if impl(ghc >= 7.10)
ghc-options: -fwarn-alternative-layout-rule-transitional
-- The above option isn't documented in GHC 7.10.1.
-fwarn-deprecated-flags
-fwarn-deriving-typeable
-fwarn-dodgy-exports
-fwarn-dodgy-foreign-imports
-fwarn-dodgy-imports
-fwarn-duplicate-exports
-fwarn-empty-enumerations
-fwarn-hi-shadowing
-fwarn-identities
-fwarn-incomplete-patterns
-fwarn-incomplete-record-updates
-fwarn-incomplete-uni-patterns
-fwarn-inline-rule-shadowing
-fwarn-missing-fields
-- 18 July 2014. We cannot enable this option
-- because we are using the Paths_apia module.
-- -fwarn-missing-import-lists
-fwarn-missing-methods
-fwarn-missing-signatures
-fwarn-monomorphism-restriction
-fwarn-name-shadowing
-fwarn-orphans
-fwarn-overflowed-literals
-fwarn-overlapping-patterns
-fwarn-tabs
-fwarn-type-defaults
-fwarn-typed-holes
-fwarn-unrecognised-pragmas
-fwarn-unused-binds
-fwarn-unused-do-bind
-fwarn-unused-imports
-fwarn-unused-matches
-fwarn-unsupported-calling-conventions
-fwarn-unsupported-llvm-version
-fwarn-unticked-promoted-constructors
-fwarn-warnings-deprecations
-fwarn-wrong-do-bind
-- The `-fwarn-context-quantification` and
-- `-fwarn-duplicate-constraints` options will be deprected in GHC
-- 8.0.1.
if impl(ghc >= 7.10) && impl(ghc < 8.0)
ghc-options: -fwarn-context-quantification
-fwarn-duplicate-constraints
-fwarn-missing-local-sigs
-- This option will be removed in GHC 8.0.1.
-fwarn-pointless-pragmas
if impl(ghc >= 8.0)
ghc-options: -Wmissing-local-signatures
-Wmissing-monadfail-instances
-Wmissing-pattern-synonym-signatures
-Wnoncanonical-monad-instances
-Wnoncanonical-monoid-instances
-Wredundant-constraints
-Wsemigroup
-Wunrecognised-warning-flags
-Wunused-foralls
if impl(ghc >= 8.2)
ghc-options: -Wcpp-undef
-Wsimplifiable-class-constraints
-Wunbanged-strict-patterns
-- From Agda.cabal: 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
ghc-prof-options: -fprof-auto
-- From Agda.cabal:
--
-- 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.
test-suite apia-tests
type: exitcode-stdio-1.0
hs-source-dirs: test
main-is: Main.hs
other-modules: Fail.Errors.Test
, Succeed.NonConjectures.Test
, Utils
build-depends: base >= 4.8.0.0 && < 4.12
, directory >= 1.2.2.0 && < 1.4
, filepath >= 1.4.0.0 && < 1.5
, tasty >= 0.10 && < 1.1
, tasty-silver >= 3.1.8 && < 3.2
, text >= 0.11.3.1 && < 1.3
default-language: Haskell2010
ghc-options: -w
-Werror
-- Using cpphs as the C preprocessor.
-pgmP cpphs -optP --cpp
if impl(ghc >= 7.10)
ghc-options: -fwarn-alternative-layout-rule-transitional
-- The above option isn't documented in GHC 7.10.1.
-fwarn-deprecated-flags
-fwarn-deriving-typeable
-fwarn-dodgy-exports
-fwarn-dodgy-foreign-imports
-fwarn-dodgy-imports
-fwarn-duplicate-exports
-fwarn-empty-enumerations
-fwarn-hi-shadowing
-fwarn-identities
-fwarn-incomplete-patterns
-fwarn-incomplete-record-updates
-fwarn-incomplete-uni-patterns
-fwarn-inline-rule-shadowing
-fwarn-missing-fields
-- 18 July 2014. We cannot enable this option
-- because we are using the Paths_apia module.
-- -fwarn-missing-import-lists
-fwarn-missing-methods
-fwarn-missing-signatures
-fwarn-monomorphism-restriction
-fwarn-name-shadowing
-fwarn-orphans
-fwarn-overflowed-literals
-fwarn-overlapping-patterns
-fwarn-tabs
-fwarn-type-defaults
-fwarn-typed-holes
-fwarn-unrecognised-pragmas
-fwarn-unused-binds
-fwarn-unused-do-bind
-fwarn-unused-imports
-fwarn-unused-matches
-fwarn-unsupported-calling-conventions
-fwarn-unsupported-llvm-version
-fwarn-unticked-promoted-constructors
-fwarn-warnings-deprecations
-fwarn-wrong-do-bind
-- The `-fwarn-context-quantification` and
-- `-fwarn-duplicate-constraints` options will be deprected in GHC
-- 8.0.1.
if impl(ghc >= 7.10) && impl(ghc < 8.0)
ghc-options: -fwarn-context-quantification
-fwarn-duplicate-constraints
-fwarn-missing-local-sigs
-- This option will be removed in GHC 8.0.1.
-fwarn-pointless-pragmas
if impl(ghc >= 8.0)
ghc-options: -Wmissing-local-signatures
-Wmissing-monadfail-instances
-Wmissing-pattern-synonym-signatures
-Wnoncanonical-monad-instances
-Wnoncanonical-monoid-instances
-Wredundant-constraints
-Wsemigroup
-Wunrecognised-warning-flags
-Wunused-foralls
if impl(ghc >= 8.2)
ghc-options: -Wcpp-undef
-Wsimplifiable-class-constraints
-Wunbanged-strict-patterns