vs code

Stream: new members

[Rebecca Bellovin]

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]

@Rebecca Bellovin Ouch, that sounds painful :oops:

[Johan Commelin]

When did you install lean?

[Rebecca Bellovin]

last week

[Johan Commelin]

Do you have leanproject?

[Johan Commelin]

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

[Johan Commelin]

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

[Rebecca Bellovin]

yes, I typed leanproject get tutorials to get the tutorials

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

What does leanproject --version say?

[Rebecca Bellovin]

leanproject, version 0.0.6

[Johan Commelin]

Ok, so that's also not the issue

[Johan Commelin]

That's the newest version

[Johan Commelin]

@Rebecca Bellovin Are you using VScode?

[Rebecca Bellovin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Rebecca Bellovin]

I generally use vi :)

[Johan Commelin]

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

[Johan Commelin]

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

[Rebecca Bellovin]

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

[Johan Commelin]

Hmm... hopefully VScode is now usable again.

[Johan Commelin]

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

[Rebecca Bellovin]

don't think so, no

[Johan Commelin]

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

[Johan Commelin]

Ok, weird.

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Rebecca Bellovin]

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

[Johan Commelin]

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

[Johan Commelin]

Ok, sure! Enjoy the tutorials!

[Rebecca Bellovin]

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]

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

[Rebecca Bellovin]

thanks! hopefully everything will magically start working

[Patrick Massot]

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]

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]

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]

This is very weird

[Patrick Massot]

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]

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]

This shouldn't happen

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Gabriel Ebner]

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]

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]

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]

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

[Jalex Stark]

uh try brew install python3?

[Alex Mathers]

I feel like such an idiot, thank you

[Jalex Stark]

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

[Jalex Stark]

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]

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]

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]

Will do :)

[John Hui]

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]

(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]

@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.