Investigate smtlib for bsc constraint solving about bsc HOT 3 OPEN

Thanks for this carefully reasoned analysis. I think I mostly agree with you. In particular we really do need to fix our open source license compliance, and we absolutely do need to get a test suite up and running for this. Thankfully there's work being done in the background to open source Bluespec's test suite.

Someone else mentioned sbv to me as the 'standard Haskell SMT solver' before, so, dependencies and build issues allowing, I think we should use it.

I'll take a look at what sbv's transitive dependency graph is like. I do notice that sbv 8.1 and later (current is 8.6) require base 4.11 which means GHC 8.4 or later. That might be a little too new. However older versions of sbv (including the 7.12 in Debian) only require base 4.9 and GHC 8.0.

Also, @quark17 how often does bsc use the sat solver? If it's doing many many queries over the course of a compilation, running external executables for each one might be a significant performance overhead (particularly on macOS and Windows).

from bsc.

The thing about SBV is that it often does releases that contain GHC support "in tandem" with new features. For instance I wouldn't be surprised if sbv 7.12 didn't work on GHC 8.4 or later, for example. So if you want any features from the sbv 8.x series, or you simply want to allow users to use GHC 8.4 -- then you're out of luck. (In particular, Nixpkgs uses GHC 8.6 to build Bluespec, and I plan on submitting patches here to do Nix CI builds with GHC 8.6 as well.)

More generally, I think requiring GHC 8.4, or even GHC 8.6, or any "relatively recent" compiler, isn't really problematic (as I noted in some other ticket). The biggest sticking point is "can the user install that compiler?" but most distros follow a much more aggressive release schedule than LTS-oriented distros like Debian/Ubuntu/RHEL do where this would be an issue, and on those platforms there are often (supported) alternative ways of acquiring the needed compiler anyway. (Frankly, Ubuntu LTS is probably the easiest platform you can install various Haskell compilers on!)

Personally, I'd say the smart thing to do from a QA/burden/maintenance POV, is exactly CI and restrict "official" support to 1-2 compilers only (say, GHC 8.4 and 8.6, for now), and accept tentative patches for other users on an as-needed basis only. Bluespec (as a project) can bump the supported GHC version(s) once every 6-8 months, as needed. This is roughly the cadence at which the traditional Haskell community moves, and it makes dependencies like sbv pretty easy to handle.

from bsc.

Also, I can say that once the user does have a supported compiler installed, Haskell tooling these days is generally quite good about reliable, repeatable builds. In particular, cabal new-build (aka "cabal 3.0") are fairly game changing and mean anyone who can get the right GHC version can basically "instantly" do a build with a lockfile and get reproducible results. So I think the costs of constraining some support -- of adding support restrictions -- are well worth it here, because in return we can get pretty reliable and flexible builds for developer needs.

I'll also note that newer GHC features like "environment files" mean that we also do not have to opt into Cabal for building the bsc binary, so the migration can be progressive. Rather, we can use Cabal to only populate the needed (fixed, locked) dependencies for bsc, then just run ghc ourselves like we do now. So we don't need to mess with the build system much.

from bsc.