multiple input pipes

Stream: lean4 dev

[James Gallicchio]

Is there a way to pass multiple input pipes to a process I'm spawning from Lean?

In bash for example I can do cat <(echo "hi") <(echo "bye") and bash will make file descriptors for each of these sub-processes and pass /dev/fd/X in the arg list of cat so when it opens those files it is actually opening the pipe.

Does core provide a way to do this? Is it even possible to do platform independently (i.e. on Windows)? I know very little about how OS primitives work but am seeing something called "named pipes" that exist in both unix and windows maybe? :frowning:

[Eric Wieser]

On linux you can probably wrap C's mkfifo

[James Gallicchio]

Yeah... I'm trying to decide in the short-term whether it's easier to give an API for mkfifo or to just spawn a bash process with the command substitution

[James Gallicchio]

A related issue, if I have a Handle that I want to set as the stdout of a new process, I think the only way I can do so right now is spawn the process as stdout := .piped and then spawn another thread copying from one handle to the other?

[Eric Wieser]

I think you can set the stdout directly to the handle?

[Eric Wieser]

Ah, you're right, you can't pass a handle of your own making

[Eric Wieser]

Ah, you're right, you can't pass a handle of your own making

[James Gallicchio]

Yeah... Maybe it can just be added as an option for the pipe configuration? Not sure what correctness issues come up with doing so.