On 2022-10-18 00:10, Scott Talbert wrote:
On Mon, 17 Oct 2022, Ivan Perez wrote:On 2022-10-14 01:41, Scott Talbert wrote:Everything has now built successfully on all architectures, so Ibelieve copilot* should migrate to testing (bookworm) in about 3 days.:)It's now in bookworm! :)))And just as soon as it made it into bookworm, it's scheduled to be kicked out on Nov 16 due to cvc4 being FTBFS (haskell-what4 build depends on it for tests).
Oh crap.
:( I suppose I could work around that by disabling more tests, if it doesn't get fixed.
Please...!
BTW, does copilot require any solvers to be present to be useful? I think we handled all of the haskell dependencies, but are there any other non-haskell packages needed?
Copilot doesn't require solvers to be useful. Some features use solvers, but the main purpose, which is generating C code from specifications, does not require solvers.
What4 supports multiple solvers: https://hackage.haskell.org/package/what4-1.3/docs/What4-Solver.html This example uses Z3 instead of CVC4: https://github.com/Copilot-Language/copilot/blob/master/copilot/examples/what4/Structs.hsI think disabling some tests in what4 is the way to go at present. I'll contact their team to see what the right thing to do is moving forward (e.g., maybe a cabal flag, like with other solvers?)
Ivan