| 20 Feb 2026 |
 woobilicious | Who should I at in the PR? | 01:04:28 |
| woobilicious | nevermind I think I found the list. | 01:07:57 |
 sterni | woobilicious: we should run at least some of the tests with sbv given how much intervention it needs | 10:44:46 |
| sterni | 45min test execution time is not really a problem in most cases | 10:45:08 |
| woobilicious | sterni: upstream recommends turning tests off, and I have zero clue how to disable test sets and a lot of them are broken due to nix paths being checked in the test suite. I don't know what you mean by "given how much intervention it needs", the package has been marked for 3 years as broken only due to missing optional binaries, the aforementioned path mismatches causing test failures. SBV seems to be working for me fine here. Note that sbv tests do code generation for SAT solvers, and then calls those SAT solves, these are not trivial fixes. | 12:08:20 |
 magic_rb | alexfmpe
the escape character for "" is \, the escape character(s) for '''' is '' | 12:39:32 |
| 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 |
|  Void Mona(d) changed their display name from Uraraka ~ Ochaco to Void Mona(d). | 14:31:16 |
|  h7x4 changed their profile picture. | 19:25:58 |
| h7x4 changed their profile picture. | 19:30:15 |
| h7x4 changed their profile picture. | 19:33:40 |
