Fix resolution of executable names on Windows.

[lovettchris]

This lakefile.lean fails to build on windows because the command 'npm' has to be resolved to C:\Program Files\nodejs\npm.cmd and there is a special Windows API that does that called SearchPath. I've tested that this fix works and lake build is able to successfully complete the npm command using a locally patched version of lean.exe.

[github-actions]

Thanks for your contribution! Please make sure to follow our Commit Convention.

[Kha]

Could you provide references to other stdlib implementations showing that this is the correct approach for such an API?

[lovettchris]

Could you provide references to other stdlib implementations showing that this is the correct approach for such an API?

Most unix-like tools that are using spawn are using the standard C library _spawnlp for their Windows version and the version provided in the Microsoft C runtime does a FindExecutable call. We are not using the std C library, instead we are using the lower level CreateProcess call which requires the file name be fully resolved already. I'm not sure why we are using CreateProcess instead of spawn, but probably for stdio redirection?

Many unix-derrived tools also get this wrong and try and reverse engineer the algorithm in FindExecutable, for example, see cmake implementation of spawn which calls search_path to compute the application_path given to CreateProcess and the search path is implementation is big and complex - including the helper function path_search_walk_ext which looks for *.exe and *.cmd an *.com file extensions and so on. It's just easier to use FindExecutable. Note I also verified FindExecutable is utf-8 friendly so I was able to find an app in a folder containing large unicode characters.

But I did a bit more testing and found some more improvements. If the given command is already a full path pointing to an existing file then FindExecutable can do some weird things reverting to "8.3 short file format" which we don't want and I also generalized the adding of double quotes to handle the case where the incoming command also contains spaces already.

[Kha]

I'm way out of my depth here, but the FindExecutable docs say: "Use FindExecutable for documents." Surely we don't want Process.spawn "foo.docx" to open Word?

[Kha]

My question about other stdlibs stands btw. If everyone else has to special-case npm.cmd on Windows, we may have to accept that.

[Kha]

Another common option with process spawn APIs is an opt-in shell : Bool parameter. On Windows I assume that would use cmd.exe and would make npm work as is.

[lovettchris]

"Use FindExecutable for documents." Surely we don't want Process.spawn "foo.docx" to open Word?

@Kha, you are right, FindExecutable is doing too much, so I switched to using SearchPath instead. I also tested the "We must escape the arguments to preseving spacing" code a bit more and it seems to be correct.

[lovettchris]

@Kha - I think we still need to merge this so that Lake on Windows behaves better (See leanprover-community/lean4-samples#3).

[leodemoura]

@lovettchris Thanks for working on this issue. It seems there is one pending issue on this thread.

Could you provide references to other stdlib implementations showing that this is the correct approach for such an API?

Could you please provide references? I think this is a valid concern.

[lovettchris]

Could you please provide references? I think this is a valid concern.

How about the llvm debugger which has a ProcessLauncherWindows that calls the Win32 CreateProcess using a ProcessLaunchInfo::GetExecutableFile where this is checked (for example in MonitoringProcessLauncher and when the path does not exist it calls ResolveExecutableLocation which calls the Windows implementation of sys::findProgramByName which uses win32 Searchpath.

[Kha]

@lovettchris Good to see that others use similar workarounds, but I hope you can appreciate the difference between doing so in a private API in some software with clear use cases versus in a public API in a language's standard library.
By the way, I learned that the batch story is even worse: that passing a .cmd file name to CreateProcess like this PR does works at all is undocumented behavior, with the documentation stating the opposite:

To run a batch file, you must start the command interpreter; set lpApplicationName to cmd.exe and set lpCommandLine to the following arguments: /c plus the name of the batch file.

[Vtec234]

Fwiw, I adjusted the originally mentioned lakefile to select npm.cmd on Windows, which is perhaps closer to the "select downstream but not in stdlib" approach.

[lovettchris]

Thanks, meanwhile I'm trying to fix it with this: #1257

[leodemoura]

I am closing this PR. @Kha raised an important point, and @lovettchris found an alternative fix.