shell pipe in lean

Stream: lean4

[Damiano Testa]

Following up from the thread about running a shell command in lean, I would like now to "pipe" a command into another one.

For example, how can I perform

echo "#eval 0" | lake env lean --stdin

in lean?

[Julian Berman]

Here the thing you want to know about is called "process substitution". In general pipes are overused interactively.

[Julian Berman]

Specifically... lake env lean <(echo '#eval 0') -- that's zsh syntax, but I think bash has copied it by now.

[Damiano Testa]

Oh, so I can use <(...) as one of the arguments?

[Julian Berman]

Ah sorry, the whole point of the question is in lean I guess? So what I told you is nonsense.

[Damiano Testa]

Oh, yes, basically, I want to avoid having to store the output of some command in a file to then have lean parse that file. Hence the question.

[Julian Berman]

No that too is shell syntax for creating a FIFO

[Damiano Testa]

(And all this within a Lean script.)

[Julian Berman]

I'm not sure whether core Lean exposes what's needed for doing that yourself, let's see...

[Damiano Testa]

I suspect that Child is relevant, but I was not able to work my head around it.

[Julian Berman]

(The functionality is of course part of libc, so it's a question of whether it's being exported to you)

[Damiano Testa]

(Near docs#IO.Process, I think.)

[Damiano Testa]

However, it uses handles and I have not really understood what they are.

[Julian Berman]

Yeah you're in the right place (and I've done nothing but tell you irrelevant things). I'm not sure I'll be any more help considering I don't this API either, but let's see, looking.

[Damiano Testa]

Great, thanks! If you can give me any insight, I would be very happy! :smile:

[Julian Berman]

If I follow scanning this right, the steps should be you need to set stdin (from StdioConfig, which SpawnArgs extends) to Stdio.piped

[Julian Berman]

And then you need to write to that pipe

[Julian Berman]

Then Child may indeed be relevant because Lean will probably wait for you to close that pipe before it exits.

[Julian Berman]

Let's see if I can do a proper example...

[Damiano Testa]

Wow, thanks! Even this has already clarified some of my ideas!

[Damiano Testa]

If you can literally do the example above, I think that I can probably take it from there: my actual command is piping a single shell command into lake env lean --stdin.

[Julian Berman]

(An even higher level API would look like https://docs.python.org/3/library/subprocess.html#subprocess.run and let you pass directly some file-like thing while spawning your subprocess, but I don't see such functionality yet)

[Julian Berman]

Ah yes if you have a shell command it may even be easier -- then you don't do the write, you want to pass the stdout directly from your previous process as the stdin of the child process

[Damiano Testa]

At the same time, I am trying to get docs#Lean.Elab.runFrontend to work -- maybe this allows me to bypass the shell entirely.

[Julian Berman]

(I don't have something working which is why I haven't responded yet :) -- the obvious first attempt was

def pipeLeft : IO.Process.SpawnArgs where
  cmd := "echo"
  args := #["Hello world!"]
  stdout := IO.Process.Stdio.piped

def cmd : IO.Process.SpawnArgs where
  cmd := "tac"

#eval do
  let child ← IO.Process.spawn pipeLeft
  IO.println <| ← IO.Process.run { cmd with stdin := child.stdout }

but that doesn't work, it looks like it's our job to actually connect the pipe. Not sure how yet.

[Damiano Testa]

Julian, thank you! I'll play some more with converting child to IO.Process.Stdio and also with using runFrontEnd directly: I hope that one of the two will work!

[Julian Berman]

Getting there, now by cheating and looking at https://github.com/leanprover/lean4/blob/9d4696123693b2f0deee658b8021236e5168b4de/tests/lean/Process.lean#L27

#eval do
  let child ← IO.Process.spawn {
    cmd := "echo",
    args := #["#check 37"]
    stdout := IO.Process.Stdio.piped
  }
  let stdout ← child.stdout.readToEnd
  let lean ← IO.Process.spawn {
    cmd := "lake",
    args := #["env", "lean", "--stdin"]
    stdin := IO.Process.Stdio.piped
  }
  lean.stdin.putStr stdout
  child.wait <|> lean.wait

The above is wrong for multiple reasons (it buffers the data in memory), but yeah sharing brain dumps in case anything helps you.

[Julian Berman]

(n.b. I think buffering in memory seems required, which probably I knew at one point and have forgotten -- the higher level Python API just looks like it does that buffering optimally by not doing everything and incrementally writing to the pipe, so maybe the above is not totally far off)

[Damiano Testa]

Thank you very much! I will have to play a bit with this to understand what it is doing.

It also seems to interact poorly with VSCode, in that it appears to freeze.

Anyway, this is very helpful and I am getting a better feel for how to deal with stdin and stdout.

[Julian Berman]

Yeah I noticed that (it freezes neovim too of course). "Run everything I type" is a really poor way to develop this kind of thing, I would be super afraid to develop anything that even touches IO.process or the FS package -- if/(hopefully when?) I write real programs in Lean I probably will do them with the LSP entirely off, unless someone who knows things tells us what the way to do this is. Live typing info is nice but "I accidentally blew away my computer which was running everything as I type" seems like a risk not worth taking.

[Damiano Testa]

Yes, I find myself constantly writing the commands in a def myCommand and then just below commenting and uncommenting #eval myCommand.

[Damiano Testa]

I am especially nervous when I use docs#IO.FS.writeFile.

[Julian Berman]

My recollection is there's some old issue by Gabriel somewhere that talks about this.

[Julian Berman]

https://github.com/leanprover/lean3/issues/1781 I guess though I thought there was a longer one somewhere.

[Damiano Testa]

Anyway, if I can actually bypass the shell entirely and use directly the runFrontEnd I would be happier!

[Julian Berman]

FWIW pendantically for terminology, there is (should be) no shell involved here unless Lean is secretly invoking one which I would strongly doubt, especially given the function is called spawn. This is "spawning external processes". But your sentiment is still understood/I agree that that sounds even nicer if it can be used.

[Damiano Testa]

Oh, I did not know about the issue, but it seems that the outcome is "live with it"! :smile:

[Damiano Testa]

If it is not a shell, then who is executing the "shell-like" commands?

[Julian Berman]

Your operating system has some primitive that says "start a process". A shell is one kind of program that calls that API to start processes. But you can call it directly (and that's what you're doing here).

[Julian Berman]

In fact there are a few such APIs -- on *nix operating systems the modern one is called man 2 posix_spawn -- and the older one is a combination of man 2 fork (which is an API that means "copy the current process") and man 2 exec (which is an API that means "replace the current process entirely with some other one", the combination of the two mean you can spawn new subprocesses)

[Damiano Testa]

So, these commands are just instructing the computer to do the same operations that running them in a shell would? (I am probably exposing some deep ignorance here, so feel free to say that this is nonsense!)

[Julian Berman]

No that's exactly right, your shell broadly does a 2 step process -- "parse the string you typed" and then "use the parsed thing to spawn some process".

[Julian Berman]

The language your shell uses (parses) to do the first part is nuts.

[Julian Berman]

So generally whenever one can avoid it (subjective opinion of course) it's right to avoid it.

[Damiano Testa]

Ok, thanks! What is that lower language?

[Julian Berman]

That's the language that adds things like ~ means "my home directory", <(...) means process substitution, | means "create a pipe and pipe", etc.

[Julian Berman]

Or even more basic things like echo hello means 2 arguments

[Julian Berman]

Which is why in your case you instead have a Lean array, the shell is what normally does the splitting.

[Damiano Testa]

That clears up so much! So the various steps of word splitting, globbing, variable expansions, these have to be done "manually" when using IO.Process, right? (It was not really clear to me what was allowed and what was not allowed).

[Julian Berman]

Exactly right.

[Damiano Testa]

Ok, that explains now why I need an array of arguments and not just a single string! :man_facepalming:

[Damiano Testa]

And hence, what you wrote above is how to "parse" a pipe and convert it into more basic operations.

[Julian Berman]

Yep, sounds like you've got it.

[Damiano Testa]

I realize that this is not genuinely a solution, but you could then also do cmd = "eval" , args = "just one string"?

[Julian Berman]

What is eval there?

[Julian Berman]

You're asking "can I get a shell to do all my work" I suspect, right?

[Damiano Testa]

Oh, the shell eval?

[Julian Berman]

If so the answer is "yes", you can do cmd = "bash", args = #["-c", "just one string"]

[Julian Berman]

(But now you run into fun stuff which you wish you won't want to know -- namely lots of things are not portable across shells, not all systems, will have all shells, even bash, installed, ...) It's a deep and terrible rabbit hole.

[Damiano Testa]

and the just one string could contain pipes and process substitutions. (I don't like this approach, but just testing my understanding)

[Julian Berman]

But yes it's still for better or worse common.

[Julian Berman]

Correct.

[Damiano Testa]

Ok, thank you very much: I learned a lot!

[Damiano Testa]

And with all this knowledge, I will try to avoid as much as possible using IO.Process! :smile:

[Julian Berman]

(To be clear which I'm sure you knew ha I think spawning processes, without shells, is in generally totally fine -- but as you say, if there's some even more appropriate API, great, saves the trouble)

[Damiano Testa]

Yes, I can probably work with the solution that you wrote above, but I would also like to catch messages that Lean would produce while parsing the string, so if I can "stay within Lean", it will probably simplify my code later on.

[Damiano Testa]

If anyone else wonders about the eventual solution, I got docs#Lean.Elab.runFrontend (or rather docs#Lean.Elab.process) to run:

  ...
  -- find the root of the project
  Lean.initSearchPath (← Lean.findSysroot)
  -- create the environment with `import Mathlib.Tactic.UpdateDeprecations`
  let env : Environment ← importModules #[{module := `Mathlib.Tactic.UpdateDeprecations}] {}
  -- process the `lake build` output, catching messages
  let (_, msgLog) ← Lean.Elab.process buildOutput env {}
  ...

(adapted from this code)

[Damiano Testa]

This bypasses, for my use-case, the need to pipe a lake build step into a lake env lean --stdin.

[James Gallicchio]

and if anyone does want to replicate pipe from Lean (and only on Unix), here's an example of using a FIFO special file: example, relevant utility file, fifo file man page