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.
Seg fault on lean.exe #1972
Open
Description
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.
- Specifically, check out the wishlist, open RFCs,
or feature requests.
- Specifically, check out the wishlist, open RFCs,
- Reduced the issue to a self-contained, reproducible test case.
- Checked that your issue isn't already filed.
Description
Cannot use lean.exe. On MSYS32 I use PATH:d/..., and then using lean --version gives a segmentation fault. I first came across the error when VSCode said lean.exe gave an error.
Steps to Reproduce
- I haven't changed anything on my PC, except windows updated last night, so I am 99% sure that is causing the problem.
- I am running windows home single language, version 1809, OS build 17751.1.
Expected behavior: MSYS32 should tell me what version of lean I'm using.
Actual behavior: Segmentation fault
Reproduces how often: 100%
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. (how ironic)
Using lean nightly 21/06/18, same thing happened when I tried 23/08.
Additional Information
It's the windows insider something update, I don't know that much about programming/CS, and I'm not sure what I will lose if I try to revert the update.
Metadata
Metadata
Assignees
Labels
No labels