twee-2.7.1: twee.cabal
cabal-version: 2.2
name: twee
version: 2.7.1
synopsis: An equational theorem prover
homepage: https://twee.smallbone.se
license: BSD-3-Clause
license-file: LICENSE
author: Nick Smallbone
maintainer: nicsma@chalmers.se
category: Theorem Provers
build-type: Simple
extra-source-files: README.md examples/*.p misc/*.hs misc/*.pl
description:
Twee is an experimental equational theorem prover based on
Knuth-Bendix completion.
.
Given a set of equational axioms and a set of equational
conjectures it will try to prove the conjectures.
It will terminate if the conjectures are true but normally
fail to terminate if they are false.
.
The input problem should be in TPTP format (see
https://www.tptp.org). You can use types and quantifiers, but apart
from that the problem must be equational.
source-repository head
type: git
location: https://codeberg.org/nick8325/twee
branch: main
flag static
description: Build a static binary.
default: False
manual: True
flag parallel
description: Build a special parallel version of Twee.
default: False
manual: True
flag rtsopts
description: Enable -rtsopts (e.g. for setting maximum memory use.)
default: False
manual: True
common executable-stuff
hs-source-dirs: executable
default-language: Haskell2010
build-depends: base < 5,
twee-lib == 2.7.1,
containers,
pretty,
split,
jukebox == 0.5.15,
ansi-terminal >= 0.9,
symbol,
hashable,
bytestring,
binary,
process
other-modules: SequentialMain
ghc-options: -W -fno-warn-incomplete-patterns
if flag(static)
ghc-options: -optl -static
if flag(rtsopts)
ghc-options: -rtsopts
executable twee
import: executable-stuff
main-is: Main.hs
executable twee-lpo
import: executable-stuff
main-is: Main.hs
cpp-options: -DUSE_LPO
executable parallel-twee
import: executable-stuff
if !flag(parallel)
buildable: False
main-is: ParallelMain.hs
build-depends: async, unix
c-sources: executable/link.c
Test-Suite twee-test
type: exitcode-stdio-1.0
Default-language: Haskell2010
hs-source-dirs:
test
main-is: Main.hs
build-depends: base < 5, QuickCheck, twee-lib == 2.7, containers, pretty, tasty, tasty-quickcheck, hashable, binary, bytestring
other-modules:
Common
Index
Nest
Ordering
Serial
TermOrder
Terms
ghc-options:
-threaded
-feager-blackholing
-with-rtsopts=-N