LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
243 stars 34 forks source link

Remove ghc dependency #521

Closed TerrorJack closed 4 years ago

TerrorJack commented 4 years ago

The ghc dependency has become redundant some time ago, removing it shouldn't break builds. Additionally, this enables sbv to be built by Asterius.

LeventErkok commented 4 years ago

Thanks! I don't remember how that dependency crept in, but always good to remove them. Are you aware of any tools that can detect unnecessary dependencies in the cabal file? Would be good to run it occasionally.

Also, would love to see if SBV can run in the browser via Asterius. If you have a demo set-up, I'd like to take a look.

Thanks..

TerrorJack commented 4 years ago

See https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/using-warnings.html#ghc-flag--Wunused-packages for a recent GHC option to warn about unused packages.

Someone else is planning to use sbv for generating smtlib program as the input of emscripten-compiled z3. Will surely keep you updated if that goes well :)