## 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: May 17 2021 at 21:12 UTC