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
240 stars 33 forks source link

Consider splitting examples in to separate package #659

Closed georgefst closed 1 year ago

georgefst commented 1 year ago

It's quite unconventional to include examples in the library itself, and there are obvious benefits to the package being slimmer. Note that Cabal has reasonably good support these days for defining "multiple public libraries" in a single .cabal file.

Personally, my primary motivation for this is cross-compilation. This is difficult due to the use of TemplateHaskell in the Documentation folder, even though the core library doesn't use it.

LeventErkok commented 1 year ago

I keep them together to reduce maintenance issues. When they're together, they don't go out of sync. And I like that the hackage documentation always includes examples.

I've never tried to cross-compile SBV; so I'm not sure what the exact ramifications are. I see one reference to TemplateHaskell in the SBV/Client.hs file; so it's probably not something you can get rid of by removing documentation part.

If a "smaller" core is desirable; I'd be more than OK for you to make a clone, chop off the documentation part, keep in synch with sbv; and put it out on hackage. It's free software after all. You can call it, sbv_core_crosscompile or something else you like to make it obvious what the goal is. Otherwise, I think I'd like to keep the package as is.

georgefst commented 1 year ago

When they're together, they don't go out of sync.

This would be a concern if they were in separate repositories, but I don't think it's an issue if defining two libraries in one sbv.cabal file (or even one executable per example). Anyway, I do understand there are probably other reasons why the current approach might be easier to maintain, at least with current tooling.

I see one reference to TemplateHaskell in the SBV/Client.hs file

Somehow, this actually doesn't prevent cross-compilation. Maybe because it's "only" a quasi-quote, rather than full-blown TH. But then removing the TemplateHaskell pragma does cause errors. I don't know enough about TH to know what's going on there.