Zulip Chat Archive

Stream: new members

Topic: lean in browser on classroom PC

Mike Shulman (Oct 28 2022 at 21:07):

Matthew Ballard said:

  • Sign up for GitPod
  • Make a blank repo for your notes at GitHub
  • Add this yaml file to it (you can delete the attempt to run get-cache.sh)
  • Navigate to gitpod.io/#https://github.com/$USER/$REPO
  • Run elan self update
  • Run leanproject new

Thanks! This worked okay, except that it told me I needed to run elan default stable before leanproject new. Unfortunately, when I actually got to the classroom and tried to run it there and load a mathlib file, it gave me a bunch of out of memory errors. At first I thought maybe the classroom PC wasn't very powerful, but now I'm getting the same errors on my workstation:

excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)

any ideas?

Notification Bot (Oct 28 2022 at 21:08):

22 messages were moved here from #new members > notation names by Mike Shulman.

Matthew Ballard (Oct 28 2022 at 21:59):

This seems relevant. To clarify, you did the same steps on the classroom PC and your home machine?

Mike Shulman (Oct 28 2022 at 22:51):

Yes, same thing. It doesn't seem to save the leanproject configuration; every time I open it up it has to re-run leanpkg configure. Then when I open up a file that imports something from mathlib, it spins for a while and I get the "excessive memory consumption" error.

Mike Shulman (Oct 28 2022 at 22:51):

Restarting the tab doesn't help.

Eric Wieser (Oct 28 2022 at 23:16):

That yaml file is a bad template to start from

Eric Wieser (Oct 28 2022 at 23:17):

Try this one: https://github.com/eric-wieser/lean-graded-rings/blob/master/.gitpod.yml

Kevin Buzzard (Oct 29 2022 at 05:52):

Sounds like you're not only using mathlib, you're compiling mathlib on the fly. This takes a few hours...

Mike Shulman (Oct 31 2022 at 21:24):

@Kevin Buzzard Ok, I'm going to move these messages to the other topic too then.

Mike Shulman (Oct 31 2022 at 21:26):

Hmm, maybe I'm not. I can't figure out how to do that, although I managed to do it before.

Kevin Buzzard (Oct 31 2022 at 21:26):

Whether or not you move things, my point was simply that if things grind to a halt the moment you import something from mathlib, then one natural diagnosis is that your computer is embarking on the 5 hour process of compiling mathlib from scratch, and this problem can often be fixed by doing something like leanproject get-mathlib-cache in the root directory of the project, which downloads fully compiled binaries from the internet.

Mike Shulman (Oct 31 2022 at 21:26):

Anyway, in the other topic Eric Weiser suggested a different .gitpod.yml which seems to have fixed the problem so far.

Mike Shulman (Oct 31 2022 at 21:27):

I think by doing exactly that and then somehow "saving" it, which wasn't happening before.

Patrick Massot (Oct 31 2022 at 21:28):

Mike, is this the move you wanted?

Mike Shulman (Oct 31 2022 at 21:28):

Yes, thanks! And now that we're here, thanks @Eric Wieser, that seems to have done the trick.

Eric Wieser (Oct 31 2022 at 22:33):

Note that it's not that the lean-liquid .gitpod.yml is bad; the problem is that all the things that make it not bad happen in the get-cache.sh script that you were told to discard!

Mike Shulman (Oct 31 2022 at 22:34):

(-:

Matthew Ballard (Nov 01 2022 at 00:39):

:tear:

Last updated: Dec 20 2023 at 11:08 UTC