Zulip Chat Archive

Stream: new members

Topic: Broke lean dependency?


view this post on Zulip 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?

view this post on Zulip Jalex Stark (May 27 2020 at 19:46):

did you try restarting VSCode yet?

view this post on Zulip 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)

view this post on Zulip Jalex Stark (May 27 2020 at 19:48):

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

view this post on Zulip ROCKY KAMEN-RUBIO (May 27 2020 at 19:51):

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

view this post on Zulip Jalex Stark (May 27 2020 at 19:52):

what happens when you run leanproject up?

view this post on Zulip Jalex Stark (May 27 2020 at 19:54):

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

view this post on Zulip ROCKY KAMEN-RUBIO (May 27 2020 at 19:55):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Jalex Stark (May 27 2020 at 20:09):

uh, that is a decent band-aid

view this post on Zulip Jalex Stark (May 27 2020 at 20:09):

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

view this post on Zulip Jalex Stark (May 27 2020 at 20:10):

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

view this post on Zulip 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: May 17 2021 at 21:12 UTC