Zulip Chat Archive

Stream: new members

Topic: Excessive memory consumption editing mathlib files

Daan van Gent (Nov 03 2022 at 15:26):

I am trying to create a pull request containing the following lemmas . The step that remains is finding the right files to place them in. However, once I try to edit one of the existing files in mathlib I get excessive memory consumption errors, and it feels improper to make a pull request of code I cannot run myself. Could someone help me with my merge?

Ruben Van de Velde (Nov 03 2022 at 15:32):

You can put them in the right place, push the branch to github, and only open the PR once the CI is happy

Ruben Van de Velde (Nov 03 2022 at 15:32):

Or open as a draft PR

Kyle Miller (Nov 03 2022 at 15:33):

it's also ok having a PR that's tagged awaiting-author for as long as you want. Reviewers will generally not look at it because it won't show up on #queue

Alex J. Best (Nov 03 2022 at 15:34):

You could also try and use tip#old-mode to see if it helps locally, or look at the changes you want to make one at a time, generally these excessive memory consumption things happen when you change a file that is relatively basic, and have another file far later in the import heierachy open in a different tab, and lean wants to check every file in between and run out of space, having only one tab open at a time can avoid this, but youll need to do lean --make -j4 src/ on the command line after to rebuild locally

Daan van Gent (Nov 03 2022 at 15:49):

Somehow the excessive memory consumption slipped into all my lean files, even though I am now on a branch where I edited no mathlib files. Getting new cache does not seem to fix it, so I'll remove my mathlib folder and leanproject get again.

Last updated: Dec 20 2023 at 11:08 UTC