Zulip Chat Archive

Stream: new members

Topic: Broke lean dependency?

ROCKY KAMEN-RUBIO (May 27 2020 at 19:38):

I accidentally ran leanpkg build instead of leanproject up and now my .lean files aren't compiling. I'm getting an error message saying "Server has stopped due to signal SIGABRT." whenever I open a new lean file in VSCode, and no tactic proofs or #check statements are giving me lean states. Thoughts?

Jalex Stark (May 27 2020 at 19:46):

did you try restarting VSCode yet?

Jalex Stark (May 27 2020 at 19:47):

(the error message you quoted is telling you that the lean server stopped, so getting the lean server to start again is the natural next move)

Jalex Stark (May 27 2020 at 19:48):

or I guess cmd-shift-P: restart lean is cleaner

ROCKY KAMEN-RUBIO (May 27 2020 at 19:51):

I tried restarting VSCode a few times but still get the same issue.

Jalex Stark (May 27 2020 at 19:52):

what happens when you run leanproject up?

Jalex Stark (May 27 2020 at 19:54):

(like, what messages get printed into your terminal?)

ROCKY KAMEN-RUBIO (May 27 2020 at 19:55):

Command '['leanpkg', 'upgrade']' died with <Signals.SIGABRT: 6>.

Jalex Stark (May 27 2020 at 19:57):

do you have any working projects on your computer? e.g. a fresh copy of leanproject get tutorials?

ROCKY KAMEN-RUBIO (May 27 2020 at 20:08):

Yeah I have another project that still seems to be working. I guess one solution is to just copy my src directory into that project?

Jalex Stark (May 27 2020 at 20:09):

uh, that is a decent band-aid

Jalex Stark (May 27 2020 at 20:09):

but the full suggestion was to poke at what is different about those two folders

Jalex Stark (May 27 2020 at 20:10):

e.g. maybe the broken one has a corrupted toml

ROCKY KAMEN-RUBIO (May 27 2020 at 20:28):

Copying over the src file seems to be working for now. I'll take a look and see if I can figure out what exactly broke.

Last updated: Dec 20 2023 at 11:08 UTC