IO.Process.spawn doesn't work on Windows

Stream: lean4

[Yaël Dillies]

I was trying to use @Anand Rao Tadipatri's amazing lean-slides, but I couldn't get anything working. After some work, we managed to minimise it to the follow, which has nothing to do with lean-slides:

#eval do
  IO.println "Running a test command ..."
  let _ ← IO.Process.spawn {
    cmd := "dir"
  }

[Yaël Dillies]

This works just fine in eg the web editor, but on my Windows machine it fails with no such file or directory (error code: 2)

[Henrik Böving]

Is dir actually a binary and not just a built-in shell command under windows? Have you tried executing anything where you actually know that it exists as a binary file on your machine (maybe even just lean --help)

[Yaël Dillies]

You talk funny words, but I think what you mean is the following :-)

#eval do -- no such file or directory (error code: 2)
  IO.println "Running a test command ..."
  let _ ← IO.Process.spawn {
    cmd := "lean --help"
  }

[Yaël Dillies]

Error is just the same as before

[Henrik Böving]

What about

#eval do
  IO.println "Running a test command ..."
  let _ ← IO.Process.spawn {
    cmd := "lean"
    args := #["--help"]
  }

[Henrik Böving]

We have three tests that spawn processes using Process.spawn directly in our test suite so I really doubt something is fundamentally broken here

[Henrik Böving]

Oh and one other thing, maybe it has to be lean.exe instead of lean, I'm not too famliar with windows specifics in this regard

[Arthur Paulino]

@Yaël Dillies are you able to run dir on your terminal? Because that's what the spawned process is trying to do.

[Henrik Böving]

Henrik Böving said:

Is dir actually a binary and not just a built-in shell command under windows? Have you tried executing anything where you actually know that it exists as a binary file on your machine (maybe even just lean --help)

as explained here having the ability to do that does not imply that you can Process.spawn it

[Yaël Dillies]

It took forever to restart the file (Windows, why :melt:), but indeed Henrik's latest suggestion works

[Yaël Dillies]

So my original problem is probably a bug in lean-slides

[Anand Rao Tadipatri]

The bit of code I'll need to modify in lean-slides is

  let _stdioCfg ← IO.Process.spawn {
    cmd := "browser-sync",
    args := #["slides", "--port", 3000,
              "--watch", "--no-open"]
  }

which works fine on Linux.

@Yaël Dillies has confirmed that running the command

browser-sync slides --port 3000 --watch --no-open

directly on the command line in Windows works as intended.

Does anyone have any advice on how to modify the configuration to be able to spawn this process on Windows?

Browsersync is installed on the system as an npm package: https://browsersync.io/.

[Robin Arnez]

I have lean4#8547 and lean4#8597 regarding docs#IO.Process.spawn. For @Yaël Dillies's first example, what should work is:

#eval do
  IO.println "Running a test command ..."
  let _ ← IO.Process.spawn {
    cmd := "cmd.exe"
    args := #["/c", "dir"]
  }

but lean4#8547 makes that fail.

[Robin Arnez]

I have a PR for that (#8612) but we might want to transition to libuv's code instead.

[Patrick Massot]

Yaël Dillies said:

So my original problem is probably a bug in lean-slides

How can the fact that you use Windows be a bug in lean-slides??

[Anand Rao Tadipatri]

@Robin Arnez Thanks a lot! Switching to that library sounds promising indeed, I've reacted to both issues with a :+1: to bump up their priority.