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.

Seg fault on lean.exe #1972

Open
Open
@alisever

Description

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

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