Seg fault on lean.exe

[alisever]

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

1. I haven't changed anything on my PC, except windows updated last night, so I am 99% sure that is causing the problem.
2. 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.

[kim-em]

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?)