Backends.Process: the test-suite may fail randomly

[qaristote]

Describe the bug
When running the test suite of smtlib-backends, one of the assertions for the process backend may sometimes fail with the error Exception: waitForProcess: does not exist (No child processes). This doesn't happen too often so it shouldn't be too much of a problem but it can cause the CI checks to fail on correct code.

To Reproduce
Unknown.

Expected behavior
The tests shouldn't fail.

[facundominguez]

It is the process backend that fails, the Z3 backend doesn't use waitForProcess as far as I can tell.
Here's the output of a failure:
https://github.com/tweag/smtlib-backends/actions/runs/3685039572/jobs/6235500281

[facundominguez]

stopProcess makes some complicated things, and sometimes it may call to waitForProcess.

I think waitForProcess is terminating with an IOException, where ioe_errno is set to eCHILD.

Assuming a bug in stopProcess, one solution could be to catch and silence this kind of exceptions.

[qaristote]

It is the process backend that fails, the Z3 backend doesn't use waitForProcess as far as I can tell.

Indeed, my bad. I'll edit the issue accordingly.

[qaristote]

Oh this probably just happens because the sources all use ackCommand solver "(exit)", so the process stops itself before we can actually do it.

[facundominguez]

Sounds like a good conjecture.

[qaristote]

one solution could be to catch and silence this kind of exceptions

Do you think we should do that regardless of whether it's useful for our test-suite ? I'd say no because it would only allow unsafe uses of the Process backend, but maybe you disagree ?

[facundominguez]

Silencing exceptions is not ideal because it could mask other problems. But we don't need to do it now that we have something reasonable to try.

The documentation of the process backend should warn not to use close or with if the SMT solver is terminated with "(exit)".

[facundominguez]

Tests are still failing after #17:
https://github.com/tweag/smtlib-backends/actions/runs/3688466600/jobs/6243305111

[qaristote]

This seems like it's still an issue in ucsd-progsys/liquid-fixpoint#641. The origin of the bug seems to lie in the implementation of stopProcess which is used in Process.kill: fpco/typed-process#38.