Zulip Chat Archive

Stream: new members

Topic: vs code


Rebecca Bellovin (May 18 2020 at 13:12):

Hi all, I'm having a problem writing lean code in vs code, which is that it semi-regularly decides to chew up the entire CPU (it goes to ~99.5% and I can't do anything for 10 minutes, including move the mouse). I'm running xubuntu 20.04 with an i7 cpu and the laptop is six months old; I installed lean following the directions https://leanprover-community.github.io/install/debian.html, and this happens when I try to do the real analysis exercises in the tutorial.

Johan Commelin (May 18 2020 at 13:13):

@Rebecca Bellovin Ouch, that sounds painful :oops:

Johan Commelin (May 18 2020 at 13:13):

When did you install lean?

Rebecca Bellovin (May 18 2020 at 13:13):

last week

Johan Commelin (May 18 2020 at 13:13):

Do you have leanproject?

Johan Commelin (May 18 2020 at 13:15):

I think I'm asking: did you also follow the steps on this page: https://leanprover-community.github.io/install/project.html

Johan Commelin (May 18 2020 at 13:15):

Also: welcome in the chatroom :hello: :smiley:

Rebecca Bellovin (May 18 2020 at 13:16):

yes, I typed leanproject get tutorials to get the tutorials

Johan Commelin (May 18 2020 at 13:17):

Somehow it is deciding that it should recompile everything, whereas leanproject should give you a compiled version of the library.

Johan Commelin (May 18 2020 at 13:18):

I think there was a slight hiccup with leanproject exactly last week.

Johan Commelin (May 18 2020 at 13:18):

What does leanproject --version say?

Rebecca Bellovin (May 18 2020 at 13:19):

leanproject, version 0.0.6

Johan Commelin (May 18 2020 at 13:19):

Ok, so that's also not the issue

Johan Commelin (May 18 2020 at 13:19):

That's the newest version

Johan Commelin (May 18 2020 at 13:19):

@Rebecca Bellovin Are you using VScode?

Rebecca Bellovin (May 18 2020 at 13:22):

yes
I was hoping there was a better way to write lean than vs code...

Johan Commelin (May 18 2020 at 13:24):

If you like emacs... that's also supported

Johan Commelin (May 18 2020 at 13:25):

Inside the tutorials project, does leanpkg build finish within say 5 seconds?

Rebecca Bellovin (May 18 2020 at 13:25):

I generally use vi :)

Johan Commelin (May 18 2020 at 13:25):

I'm also a vim fan. But vim is not so good at interactively updating proof states

Johan Commelin (May 18 2020 at 13:26):

VScode has a vim extension though, but it's not the real thing

Rebecca Bellovin (May 18 2020 at 13:26):

no, leanpkg build has finished but it took probably closer to 30s

Johan Commelin (May 18 2020 at 13:28):

Hmm... hopefully VScode is now usable again.

Johan Commelin (May 18 2020 at 13:28):

Maybe you accidentally touched a file in the library? Did you "Jump to definition" (aka Ctrl-click) on anything?

Rebecca Bellovin (May 18 2020 at 13:28):

don't think so, no

Johan Commelin (May 18 2020 at 13:28):

Even adding a space or newline will make lean recompile those files in the library.

Johan Commelin (May 18 2020 at 13:28):

Ok, weird.

Johan Commelin (May 18 2020 at 13:29):

At least it didn't take 50 minutes. That's what a complete recompile of the library may cost you, depending on hardware

Johan Commelin (May 18 2020 at 13:29):

Please let us know if the orange bars play up again!

Johan Commelin (May 18 2020 at 13:29):

And if you want to develop a vim mode. That would be cool!

Rebecca Bellovin (May 18 2020 at 13:30):

I...don't think I have time for that at the moment

Johan Commelin (May 18 2020 at 13:30):

I was thinking of maybe doing something with vim + tmux + https://github.com/leanprover-community/lean-client-python

Johan Commelin (May 18 2020 at 13:30):

Ok, sure! Enjoy the tutorials!

Rebecca Bellovin (May 18 2020 at 13:30):

but coqide runs fine on my laptop, and I think there is a coq plugin for vim, so I don't see why it shouldn't work in principle

Johan Commelin (May 18 2020 at 13:31):

Coq has a lot less interaction for its proof state. But sure, in principle this should all be possible.

Rebecca Bellovin (May 18 2020 at 13:31):

thanks! hopefully everything will magically start working

Patrick Massot (May 18 2020 at 14:08):

One source of hope for vim users is Oni2 whose stated goal is to merge vim and VScode (using vim for all text handling and running VScode extensions). But it's not usable yet.

Alex J. Best (May 18 2020 at 14:14):

I'm waiting to see what Lean 4's LSP looks like, hopefully that will work nicely with (neo?)vim as well, we'll see!

Rebecca Bellovin (May 18 2020 at 14:21):

things haven't locked up again, but something went wrong enough that vscode currently has a popup saying Server has stopped due to signal SIGKILL (unfortunately, I was off making lunch, so I didn't see what happened before that)

Patrick Massot (May 18 2020 at 14:21):

This is very weird

Patrick Massot (May 18 2020 at 14:22):

About vim, let's say clearly: there is no obstruction at all to building a Lean 3 neovim plugin beside the usual wall of days having only 24 hours.

Rebecca Bellovin (May 18 2020 at 14:42):

well, it just froze up; vs code then popped up a dialog saying that the window wasn't responding, and offering to reopen, keep waiting, or close it

Johan Commelin (May 18 2020 at 14:44):

This shouldn't happen

Johan Commelin (May 18 2020 at 14:45):

Clearly there is something in your setup that is not the way the install guide intends it to be.

Mario Carneiro (May 18 2020 at 19:47):

This happens to me somewhat commonly, when I've run out of memory and swap space

Mario Carneiro (May 18 2020 at 19:48):

the Server has stopped due to signal SIGKILL is an indication that the OOM killer killed lean

Mario Carneiro (May 18 2020 at 19:51):

One thing that pretty reliably has lean eating up many gigabytes of memory is having multiple files of mathlib open at the same time at very different points in the dependency order and modifying them in VSCode (forcing lean to recompile many files and keep them all in memory)

Gabriel Ebner (May 18 2020 at 20:09):

@Mario Carneiro For this special use case, you can look at --old

Mario Carneiro (May 18 2020 at 20:10):

oh, that does sound useful. Do I have to change the vscode lean invocation line for this?

Gabriel Ebner (May 18 2020 at 20:11):

Yes, for now you need to manually add the option in the vscode configuration. I'm thinking about adding some kind of UI for it to the extension.

Alex Mathers (May 19 2020 at 03:47):

I'm having a similar CPU issue as discussed above, except I've learned I don't have leanproject (so hopefully this is my issue). My issue right now is with installing it but I'm very ignorant about these types of things, I'm hoping someone can tell me what's going wrong. It seems it may have to do with my pip installation? The exact error message comes as follows: I am entering sudo pip3 install mathlibtools and getting

WARNING: The directory '/Users/alexmathers/Library/Caches/pip' or its parent directory is not owned or is not writable by the current user. The cache has been disabled. Check the permissions and owner of that directory. If executing pip with sudo, you may want sudo's -H flag.
ERROR: Could not find a version that satisfies the requirement mathlibtools (from versions: none)
ERROR: No matching distribution found for mathlibtools

Also, I'm on MacOS if that matters; let me know if I've omitted any other important info

Alex Mathers (May 19 2020 at 03:50):

also just tried running sudo -H pip3 install mathlibtools and am getting a much longer error:

Traceback (most recent call last):
  File "/usr/local/bin/pip3", line 6, in <module>
    from pkg_resources import load_entry_point
  File "/System/Library/Frameworks/Python.framework/Versions/2.7/Extras/lib/python/pkg_resources/__init__.py", line 3241, in <module>
    @_call_aside
  File "/System/Library/Frameworks/Python.framework/Versions/2.7/Extras/lib/python/pkg_resources/__init__.py", line 3225, in _call_aside
    f(*args, **kwargs)
  File "/System/Library/Frameworks/Python.framework/Versions/2.7/Extras/lib/python/pkg_resources/__init__.py", line 3254, in _initialize_master_working_set
    working_set = WorkingSet._build_master()
  File "/System/Library/Frameworks/Python.framework/Versions/2.7/Extras/lib/python/pkg_resources/__init__.py", line 583, in _build_master
    ws.require(__requires__)
  File "/System/Library/Frameworks/Python.framework/Versions/2.7/Extras/lib/python/pkg_resources/__init__.py", line 900, in require
    needed = self.resolve(parse_requirements(requirements))
  File "/System/Library/Frameworks/Python.framework/Versions/2.7/Extras/lib/python/pkg_resources/__init__.py", line 786, in resolve
    raise DistributionNotFound(req, requirers)
pkg_resources.DistributionNotFound: The 'pip==20.1' distribution was not found and is required by the application

Andrew Ashworth (May 19 2020 at 03:51):

You have Python 2 installed but are calling a Python 3 program

Jalex Stark (May 19 2020 at 03:53):

uh try brew install python3?

Alex Mathers (May 19 2020 at 04:10):

I feel like such an idiot, thank you

Jalex Stark (May 19 2020 at 04:14):

nah it's easy to just be scared when you're reaching into the guts of your computer

Jalex Stark (May 19 2020 at 04:15):

If asking for such detailed help makes you uncomfortable, just commit to give similar help in the future so as to have a net positive effect on the amount of the "basic tech support" resource available here

Jalex Stark (May 19 2020 at 04:16):

and of course, if you can think of ways to modify the documentation that would have caused you to not run into the error, bring them up

Jalex Stark (May 19 2020 at 04:16):

for every person that comes and gets explicit help here there have to be several who bounce off of lean and will be immune to trying again for several months...

Alex Mathers (May 19 2020 at 04:27):

Will do :)

John Hui (May 19 2020 at 06:42):

another note to add on vim setup: i use it only for Lean but I found this plugin that basically hooks into neovim and allow you to reuse your vimrc and your plugins: https://marketplace.visualstudio.com/items?itemName=asvetliakov.vscode-neovim

John Hui (May 19 2020 at 06:44):

(At some point, I would love to help develop a Lean plugin for Vim. But before I go about doing that, I want to try hacking around a bit with Coqtail, a vim plugin for Coq, to better understand its architecture etc.)

Rebecca Bellovin (May 19 2020 at 21:55):

@Mario Carneiro interesting, that's good to know. But I haven't had any mathlib files open, I've just been doing the tutorial, so I'm not sure why lean should need so much memory.


Last updated: Dec 20 2023 at 11:08 UTC