search

leanprover / lean3

Lean Theorem Prover
http://leanprover.github.io/
Apache License 2.0
2.15k stars 217 forks source link

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

Closed varosi closed 6 years ago

varosi commented 6 years ago

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 commented 6 years ago

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

varosi commented 6 years ago

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 commented 6 years ago

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