Skip to content
This repository was archived by the owner on Oct 14, 2023. It is now read-only.
This repository was archived by the owner on Oct 14, 2023. It is now read-only.

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

Open
@kevinsullivan

Description

@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.
    • 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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions