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 I
believe 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.hs
I 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