You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Oct 14, 2023. It is now read-only.
Reduced the issue to a self-contained, reproducible test case.
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.
The text was updated successfully, but these errors were encountered:
Lean 3 is essentially frozen while the developers work on Lean 4, so without any easy-to-reproduce test case it's unlikely that you'll get much help.
I would suggest trying to build from source. If you can do that, perhaps following the instruction for the "debug" build will result in at least a more help error message.
(You might also consider running Lean inside Linux Subsystem for Windows?)
Sign up for freeto subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Prerequisites
or feature requests.
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
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.
The text was updated successfully, but these errors were encountered: