| 20 Feb 2026 |
magic_rb | they work exactly the same | 12:39:36 |
sterni | woobilicious: well you wrote a patch for the path issues, so it should work | 12:54:02 |
sterni | the code gen and execution part means that we have little confidence it will work at runtime which the test suite helps with | 12:54:51 |
| 21 Feb 2026 |
woobilicious | sterni: the maintainer doesn't think the patch is a good idea, doesn't think we'd need to run tests, we'd still need to package mathsat, and any other SAT solvers nixpkgs is missing, it's way too much effort for a package that no one is using. I agree that it would be nice to run but the return on maintenance burden isn't there. | 01:49:34 |
woobilicious | the other issue is we really shouldn't mark the package broken when say, the cvc5 tests are failing, when A user might have no interest in using cvc5 backend, and only the z3 backend. | 01:55:13 |
woobilicious | Error in option parsing: Cannot use --nl-cov without configuring with --poly. This is a cvc5 test that fails for example. | 01:56:33 |