Understanding calling command line functions

Stream: new members

[Peter Tupoiu]

I'm trying to use a command line function and I'm getting a funny error:

def main : IO Unit := do
  -- let test <- IO.FS.readFile "lakefile.lean"
  -- IO.println test
  IO.println "HELLO!"
  let files <- IO.Process.run {cmd := "ls"}
  IO.println files

And when I run lean .\Main.lean --run I get:

HELLO!
uncaught exception: no such file or directory (error code: 2)

[Peter Tupoiu]

I was expecting it to just print the results of ls. Looking at IO.lean I expect that means it's unable to detect my current working directory?

(the IO.FS.readFile works fine, by the way)

[Sebastian Ullrich]

I don't think that's a standard Windows executable, are you sure it's in your PATH?

[Sebastian Ullrich]

And the .exe may be mandatory

[Peter Tupoiu]

Sebastian Ullrich said:

I don't think that's a standard Windows executable, are you sure it's in your PATH?

Hi Sebastian,

I am talking with Nix (not sure of their real name) on the FP discord server about this issue, and apparently there was a fix recently (or at least one to a related issue) in 4.10. The same happened with “dir” and “echo hello” as the commands.

(edit: Apparently ls is a powershell command)

[Richard Copley]

dir and echo aren't executables either, on Windows, as standard. They are handled by the interpreter cmd.exe (or by Powershell -- maybe they are provided separately as applets, but I don't know much about that). You could try executing cmd.exe /c "dir /b".

[Peter Tupoiu]

Richard Copley said:

dir and echo aren't executables either, on Windows, as standard. They are handled by the interpreter cmd.exe (or by Powershell -- maybe they are provided separately as applets, but I don't know much about that). You could try executing cmd.exe /c "dir /b".

Aha - this worked. Little bit arcane, but maybe that is just the price I pay for windows.

edit:
Final code

def main : IO Unit := do
  IO.println "HELLO!"
  let files <- IO.Process.run {cmd := "powershell.exe /c ls"}
  IO.println files