-
Notifications
You must be signed in to change notification settings - Fork 0
/
atp.cabal
156 lines (148 loc) · 3.59 KB
/
atp.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
cabal-version: 2.4
name: atp
version: 0.1.0.0
synopsis: Interface to automated theorem provers
description:
Express theorems in first-order logic and automatically prove them using
third-party reasoning tools.
homepage: https://github.com/aztek/atp
bug-reports: https://github.com/aztek/atp/issues
license: GPL-3.0-only
license-file: LICENSE
author: Evgenii Kotelnikov
maintainer: evgeny.kotelnikov@gmail.com
category: Theorem Provers, Formal Methods, Logic, Math
tested-with:
GHC == 7.10.3,
GHC == 8.0.2,
GHC == 8.2.2,
GHC == 8.4.4,
GHC == 8.6.5,
GHC == 8.8.4,
GHC == 8.10.3
extra-source-files:
CHANGELOG.md
test/**/*.hs
source-repository head
type: git
location: git://github.com/aztek/atp.git
flag Werror
default: False
manual: True
-- Build test suites that require some theorem provers to be installed.
flag provers
default: False
manual: True
library
hs-source-dirs: src
default-language: Haskell2010
exposed-modules:
ATP
ATP.Codec.TPTP
ATP.Error
ATP.FOL
ATP.Pretty.FOL
ATP.Prove
ATP.Prover
other-modules:
ATP.Internal.Enumeration
ATP.FirstOrder.Core
ATP.FirstOrder.Alpha
ATP.FirstOrder.Smart
ATP.FirstOrder.Simplification
ATP.FirstOrder.Occurrence
ATP.FirstOrder.Conversion
ATP.FirstOrder.Derivation
ghc-options:
-Wall
if flag(Werror)
ghc-options: -Werror
build-depends:
base >= 4.8 && < 5.0,
text >= 1.2.3 && < 1.3,
tptp >= 0.1.3 && < 0.2,
containers >= 0.5.11 && < 0.7,
mtl >= 2.2 && < 3.0,
ansi-wl-pprint >= 0.6.6 && < 0.7,
process >= 1.6.3 && < 1.7
if impl(ghc < 8)
ghc-options:
-fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns
build-depends:
semigroups >= 0.18 && < 1.0
if impl(ghc >= 8)
ghc-options:
-Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns
-Wredundant-constraints
test-suite property
type: exitcode-stdio-1.0
hs-source-dirs: test
default-language: Haskell2010
main-is: Property/Main.hs
other-modules:
Property.Generators
Property.Modifiers.AlphaEquivalent
Property.Modifiers.Simplified
ghc-options:
-Wall -threaded
if flag(Werror)
ghc-options: -Werror
build-depends:
base,
containers,
text,
mtl,
generic-random >= 1.2.0.0 && < 1.3,
QuickCheck >= 2.4 && < 3.0,
atp
if impl(ghc < 8)
ghc-options:
-fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns
build-depends:
semigroups >= 0.18 && < 1.0
if impl(ghc >= 8)
ghc-options:
-Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns
-Wredundant-constraints
test-suite doc
type: exitcode-stdio-1.0
hs-source-dirs: test
default-language: Haskell2010
main-is: Doc/Main.hs
other-modules:
Property.Generators
ghc-options:
-Wall -threaded
if flag(Werror)
ghc-options: -Werror
-- TODO: Make it work
buildable: False
build-depends:
base,
containers,
text,
generic-random >= 1.2.0.0 && < 1.3,
QuickCheck >= 2.4 && < 3.0,
atp,
doctest
test-suite unit
type: detailed-0.9
hs-source-dirs: test
default-language: Haskell2010
test-module: Unit.Main
ghc-options:
-Wall -threaded
if flag(Werror)
ghc-options: -Werror
if flag(provers)
buildable: True
else
buildable: False
-- TODO: Workaround the pesky bug in ghc 8.0
-- https://stackoverflow.com/q/39310043/1344648
if (impl(ghc >= 8.0.0)) && (impl(ghc < 8.1.0))
buildable: False
build-depends:
base,
Cabal >= 1.16.0,
atp