Levent Erkök

Our bound finder is producing unexpected values. Here's the simplified example: ```haskell {-# LANGUAGE ScopedTypeVariables #-} import Data.SBV findBounds = do x satWith z3 $ \x y -> (x .==...

@peddie Hi Matt.. See my notes above regarding how we should proceed with this. I'm stumped as to why z3 isn't producing the correct value: clearly we're hitting some undefined...

Cool ideas! Coq would be really nice if we can get it to spit out the bounds. I've been looking at the z3 source code to see if I can...

This'll require a bit of experimenting to find the API. My first thought is that the functions of `minimize`/`maximize` should move to the `SolverContext` class. The types will most likely...

Sounds good!

No worries. I firmly believe in "need based development." Looks like you do not need this feature, so it's best to focus on other parts instead. Cheers.

Looks like Gauge depends on basement, which causes most of benchmark suites fail to compile with GHC 9.2.1; would be great basement got a GHC 9.2.1 release.

A year after this ticket, I tried again with GHC 9.2.2; alas the very same error persists. Any chance some haddock guru might take a look at this?

@ulysses4ever Maybe it's a cabal issue; but most likely cabal/haddock/ghc all conspiring to have this problem. I found the following related tickets if it helps: https://github.com/haskell/cabal/issues/888 https://github.com/haskell/haddock/issues/158

I think this is TH as well. Even though this project is a plugin, it also has TH. I experimented a bit, and it does appear TH is the main...