leanpkg doesn't work on Windows when lean is copied to C:\Program Files\lean\

[varosi]

Prerequisites

1. install/copy Lean in C:\Program Files\lean\
2. add it to PATH

Description

leanpkg doesn't work on Windows when lean is copied to C:\Program Files\lean\

Steps to Reproduce

1. run: leanpkg from PS or CMD

Expected behavior: [What you expect to happen]
leanpkg to run correctly on Windows under normal installation place for that OS

Actual behavior: [What actually happens]

C:\Users\Vassil>leanpkg
'Files\lean\bin\..' is not recognized as an internal or external command,
operable program or batch file.
C:\Program:1:0: error: file 'C:\Program' not found
<unknown>:1:1: error: file 'C:\Program' not found

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.
Lean (version 3.4.1, commit 17fe3decaf8a, Release)

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[kbuzzard]

This is just the canonical problem that Windows has with file names with spaces in, right?

[varosi]

It is not canonical problem. Other tools have no such a problems. It’s Windows specific. I think that somewhere inside, an executable is called and the path to it is not quoted. In Windows shells you need to put quotes around paths that could have spaces in them. Otherwise spaces will separate path to different command line arguments, which usually is not intended.

[solson]

The problem is the lack of quoting in leanpkg.bat. I'm going to open a PR soon with a fix.