[ new ] Add support for bi-directional pipes on POSIX systems (resolves #2935)

[dunhamsteve]

Description

Adds a popen2 function to System.File.Process which allows Idris to run subprocesses with access to both the input and output file streams. It currently doesn't support windows, but updates are welcome if it's possible and somebody knows how to do it (and can verify that it works). This feature was requested by @jfdm in #2935, and I think @ohad was asking about it last year.

With this change you can do:

import System.File

main : IO ()
main = do
    Right (inFile, outFile) <- popen2 "idris2"
        | Left err => printLn err
    _ <- fPutStrLn outFile ":h\n"
    closeFile outFile
    Right result <- fRead inFile
        | Left err => printLn err
    putStrLn result
    putStrLn "done"

But I'd recommend writing be done on a separate thread from reading to avoid deadlocking if the subprocess is waiting for a reader while we're waiting to write.

Let me know if any changes are needed.

Should this change go in the CHANGELOG?

Yes, I added a note to the CHANGELOG.

[jfdm]

Thanks for this!

It was on my TODO list for this week, so thanks for checking this item off.

[jfdm]

I have had a quick look at the code, it was more easier than I imagined. Kudos.

I do have a minor quibble.

I wonder if a small layer of encapsulation should be added.
That is, one could:

1. add a record as the 'Right' return type for popen2, thus enabling differentiation between the two handles; and optionally;
2. extend the API for popen to support working with the returned record.

Then again that could be a bit OTT for such a low-level process API.

[gallais]

👍 I think it's a good idea to break the symmetry in the type.

The example was confusing to me as I understood in/out to be from the POV of the
callee but it was in fact from the POV of the caller.

[mattpolzin]

I'm still reading over the C code but I do think we should add a test that touches this new code prior to merging as well.

[dunhamsteve]

I was thinking something along the lines of:

||| Result of a popen2 command, containing the 
public export
record SubProcess where
  constructor MkSubProcess
  ||| Process id of the spawned process
  pid : Int
  ||| The input stream of the spawned process
  input : File
  ||| The output stream of the spawned process
  output : File

Where input is the handle you write to on the Idris side and output is what you read from. There doesn't appear to be a wait primitive - should we keep the pid here? Do we want to add wait and possibly kill to make use of that pid? The output should eof when the process is done, but we might want more control over the process itself.

The popen interface exposed above is higher level and the waiting is done internally to the C library when the special pclose is called.

[mattpolzin]

RE having use of the PID, even without wait and kill we already have the ability to send signals to it exposed in the base lib.

[EDIT] more accurately, kill is already exposed, but under the name sendSignal.

[dunhamsteve]

I switched it over to a Record, added a test case, and got it working on windows.

[mattpolzin]

Nice. Thanks!