-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathATP.cabal
169 lines (148 loc) · 4.83 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
157
158
159
160
161
162
163
164
165
166
167
168
169
name: ATP
version: 1.0.0
cabal-version: >= 1.6.0.3
build-type: Simple
license: GPL
license-file: LICENSE
author: Sean McLaughlin <[email protected]>
maintainer: Sean McLaughlin <[email protected]>
homepage:
bug-reports:
category: Theorem provers
synopsis: Haskell theorem proving algorithms.
description: A Haskell port of the code from John Harrison's book
Handbook of Practical Logic and Automated Reasoning.
tested-with: GHC == 6.10.4
extra-source-files: LICENSE
README.md
Makefile
ATP.cabal
notes/haskell.tex
library
hs-source-dirs: src
include-dirs: src
build-depends: base >= 4.1.0.0,
containers >= 0.2.0.1,
mtl >= 1.1.0.2,
parsec >= 2.0,
utf8-string >= 0.3.5,
HUnit >= 1.2.2.0,
pretty >= 1.0.1.0,
QuickCheck >= 2.1,
template-haskell >= 2.3.0.1,
hslogger >= 1.0.7,
syb >= 0.1.0.1,
directory >= 1.3.1.5
extensions: NoImplicitPrelude
MultiParamTypeClasses
ScopedTypeVariables
TypeSynonymInstances
OverlappingInstances
FlexibleInstances
DeriveDataTypeable
TemplateHaskell
QuasiQuotes
CPP
TemplateHaskellQuotes
cpp-options: -Wno-unicode-homoglyph
ghc-options: -Wall
-- These warnings are not turned on by -Wall
-fwarn-implicit-prelude
-fwarn-monomorphism-restriction
-fwarn-incomplete-record-updates
-fwarn-tabs
-fno-ignore-asserts
-- -v
-- Dump Core language
-- -ddump-simpl
-- Warnings as errors
-- -Werror
-- Allow comment lines next to literate lines
-optL -q
-- Profiling
-- -prof
-- -auto-all
exposed-modules: ATP.Util.Debug
ATP.Util.Impossible
ATP.Util.Lex
ATP.Util.Lib
ATP.Util.List
ATP.Util.ListSet
ATP.Util.Log
ATP.Util.Log.Class
ATP.Util.Misc
ATP.Util.Monad
ATP.Util.Parse
ATP.Util.Parse.Parse
ATP.Util.Prelude
ATP.Util.Print
ATP.Util.Print.Print
ATP.Util.TH
ATP.Util.Tuple
ATP.Util.UnionFind
ATP.Bdd
ATP.Combining
ATP.Completion
ATP.Complex
ATP.Cong
ATP.Cooper
ATP.Decidable
ATP.DefCnf
ATP.Dlo
ATP.Dp
ATP.EqElim
ATP.Equal
ATP.Fol
ATP.Formula
ATP.FormulaSyn
ATP.Geom
ATP.Grobner
ATP.Herbrand
ATP.Interpolation
ATP.Intro
ATP.IntroSyn
ATP.MPoly
ATP.Meson
ATP.Order
ATP.Paramodulation
ATP.Poly
ATP.Prolog
ATP.Prop
ATP.PropExamples
ATP.Qelim
ATP.Real
ATP.Resolution
ATP.Rewrite
ATP.Skolem
ATP.Stal
ATP.Tableaux
ATP.TestFormulas
ATP.Unif
ATP.Test.Combining
ATP.Test.Complex
ATP.Test.Cooper
ATP.Test.Dlo
ATP.Test.Fo
ATP.Test.Grobner
ATP.Test.Real
ATP.Test.Taut
other-modules : Compat
executable atp
main-is: Main.lhs
hs-source-dirs: src
include-dirs: src
extensions: NoImplicitPrelude
MultiParamTypeClasses
ScopedTypeVariables
TypeSynonymInstances
OverlappingInstances
FlexibleInstances
DeriveDataTypeable
TemplateHaskell
QuasiQuotes
CPP
TypeApplications
cpp-options: -Wno-unicode-homoglyph
ghc-options: -fno-ignore-asserts
-- Allow comment lines next to literate lines
-optL -q