Skip to content
This repository has been archived by the owner on Oct 14, 2023. It is now read-only.

Seg fault on lean.exe #1972

Open
alisever opened this issue Sep 2, 2018 · 1 comment
Open

Seg fault on lean.exe #1972

alisever opened this issue Sep 2, 2018 · 1 comment

Comments

@alisever
Copy link

alisever commented Sep 2, 2018

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.

@semorrison
Copy link
Contributor

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 free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants