Zulip Chat Archive

Stream: general

Topic: Pipes in lean on windows


Keeley Hoek (Sep 24 2018 at 11:14):

Just a quick question for someone in-the-know: does lean lack an implementation of pipes on windows? I'm looking in src/library/pipe.(h/cpp) and it looks empty for windows---am I missing something?

Keeley Hoek (Sep 24 2018 at 12:46):

I guess since even the windows version is built with MSYS2 it doesn't matter

Sebastian Ullrich (Sep 24 2018 at 16:01):

See https://github.com/leanprover/lean/blob/0eebde1b8b24b087935b75542a3858715097fff2/src/library/process.cpp#L104


Last updated: Dec 20 2023 at 11:08 UTC