leanpkg fails if there's a space in the pathname to the binary

[kevinsullivan]

Prerequisites

• [ X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Per title, leanpkg fails if there's a space in the path to the leanpkg executable (OSX, Windows). I know that MSR isn't further developing this version. I'm documenting the issue so that people know and so that it's a known issue. It's causing problems in a large class I'm teaching because many students have spaces in their path names. E.g., many students use Box to store files, and the top-level box directory name has a space in it.

Steps to Reproduce

It's easy to confirm. Just try it.

Expected behavior: leanpkg runs

Actual behavior: leanpkg issues error, main.lean not found

Reproduces how often: reproduces reliably

Versions

3.4.1

Additional Information

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

[semorrison]

This has been fixed in the latest nightly, available from https://github.com/leanprover/lean-nightly/releases.

If you tell your students to install Lean by using elan (e.g. see instructions at https://github.com/leanprover/mathlib/blob/master/docs/elan.md), and give them a leanpkg.toml file containing the line lean_version = "nightly-2018-10-28", then they should automatically end up with a copy of Lean that can survive spaces in filenames on Windows machines.

(It would be great to hear whether you can confirm this solves the issue.)