Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Running leanpkg build lib breaks on Windows with MSYS2 #486

Closed
1 task done
tydeu opened this issue May 25, 2021 · 0 comments
Closed
1 task done

Running leanpkg build lib breaks on Windows with MSYS2 #486

tydeu opened this issue May 25, 2021 · 0 comments

Comments

@tydeu
Copy link
Member

tydeu commented May 25, 2021

Prerequisites

  • 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

Trying to build a Lean 4 package as a library with leanpkg build lib results in a missing leanc.exe error on Windows with MSYS2. This likely is due to the fact that it is expecting it to be named leanc.exe instead of its actual name leanc (i.e. with no extension).

Steps to Reproduce

On Windows with MSYS2:

  1. Create a new directory (ex. mkdir hello)
  2. Initialize a Lean 4 package in the directory (ex. cd hello; leanpkg init Hello)
  3. Run leanpkg build lib on the package
  4. Observe the error

An error like the following should occur:

configuring Hello 0.1
> sh -c "<home>\.elan\toolchains\leanprover--lean4---nightly-2021-05-23\bin/leanmake" LEAN_OPTS="" LEAN_PATH="././build" lib >&2    # in directory .
lean  -o "build/Hello.olean" --c="build/temp/Hello.c.tmp" Hello.lean
mv "build/temp/Hello.c.tmp" "build/temp/Hello.c"
leanc -c -o build/temp/Hello.o build/temp/Hello.c -O3 -DNDEBUG
←[31m←[1merror: ←[0mtoolchain 'leanprover/lean4:nightly-2021-05-23' does not have the binary `<home>\.elan\toolchains\leanprover--lean4---nightly-2021-05-23\bin\leanc.exe`
make: *** [<home>\.elan\toolchains\leanprover--lean4---nightly-2021-05-23\bin/../share/lean/lean.mk:73: build/temp/Hello.o] Error 1
uncaught exception: external command exited with status 2

Expected behavior:

I would expect leanpkg build lib to work on Windows with MSYS2

Actual behavior:

It fails to run leanc due to expecting it to be named leanc.exe instead of leanc.

Reproduces how often:

Always.

Versions

Windows 20H2
Lean (version 4.0.0-nightly-2021-05-23, commit 28b055463fbc, Release)

I am using MSYS2 bash (MinGW 64-bit) as my terminal:

GNU bash, version 5.1.4(1)-release (x86_64-pc-msys)
Copyright (C) 2020 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>

Additional Information

None.

ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this issue Dec 2, 2022
Following @semorrison's video

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant