name: lean-bindings
version: 0.1
author: Joe Hendrix
maintainer: jhendrix@galois.com
license: Apache-2.0
license-file: LICENSE
build-type: Simple
cabal-version: >= 1.9.2
category: Language, Formal Languages, Foreign, FFI, Theorem Provers

synopsis: Haskell bindings to the Lean Theorem Prover.
description:
            This package contains Haskell bindings to the
            <http://leanprover.github.io/ Lean Theorem Prover>.
            .
            To get started using this library, you should install Lean first,
            and then install this library, providing paths to the Lean header
            and library via @--extra-include-dirs@ and @--extra-lib-dirs@ repectively.
            .
            To use this library, we recomend using a /qualified/ import, such as:
            .
            @
            import qualified Language.Lean as Lean
            @
            .
            The library currently is still a work in progress.  To see the current
            interface, we recommend starting with the documentation for
            "Language.Lean", and consulting the individual module imports there.


source-repository head
  type: git
  location: https://github.com/GaloisInc/lean-haskell-bindings.git

flag use-integer-simple
  description: Use this when compiling using a ghc that uses integer-simple instead of integer-gmp.
  default: False

library
  build-depends:
    base >= 4.6 && < 5,
    bytestring,
    lens,
    text

  if flag(use-integer-simple)
     build-depends: integer-simple
  else
     build-depends: integer-gmp

  extra-libraries:
    leanshared
  hs-source-dirs: src
  build-tools: c2hs
  ghc-options: -Wall
  exposed-modules:
    Language.Lean
    Language.Lean.Internal.String
    Language.Lean.Internal.Exception
    Language.Lean.Internal.Exception.Unsafe
    Language.Lean.Internal.Name
    Language.Lean.Internal.Options
    Language.Lean.Internal.Univ
    Language.Lean.Internal.Expr
    Language.Lean.Internal.Decl
    Language.Lean.Internal.IOS
    Language.Lean.Internal.Typechecker
    Language.Lean.Internal.Inductive
    Language.Lean.Decl
    Language.Lean.Env
    Language.Lean.Exception
    Language.Lean.Expr
    Language.Lean.Inductive
    Language.Lean.IOS
    Language.Lean.List
    Language.Lean.Module
    Language.Lean.Name
    Language.Lean.Options
    Language.Lean.Typechecker
    Language.Lean.Univ

test-suite test
  type: exitcode-stdio-1.0
  build-depends:
    base,
    lean-bindings,
    lens,
    tasty,
    tasty-ant-xml,
    tasty-hunit
  extra-libraries:
    leanshared
  other-modules:
    Tests.Env
    Tests.Expr
    Tests.Name
    Tests.Options
    Tests.Univ

  ghc-options: -Wall -threaded
  hs-source-dirs: test
  main-is: Main_test.hs