Performance when editing mathlib

Stream: general

[Wrenna Robson]

I was just trying to prepare a small PR in mathlib when I noticed a lemma - which on searching isn't used by anything - which had a name that looked wrong compared to similar lemmas. I changed it. This then caused my editing environment (VS Code in WSL2) to grind to a halt and eventually run out of memory after consuming like 10GB of it.

I understand that this is probably because changing this lemma in another file caused the first file to need to re-compile all its dependencies: but I don't think my computer can handle this. How do people edit multiple files in mathlib at once? Is it just a case of gritting your teeth? Are there ways to make this less painful?

[Riccardo Brasca]

You can have a look at this thread.

[Wrenna Robson]

Hmm - I'm not sure how much that helps with VS Code itself (because I'm not running builds from the command line).

[Wrenna Robson]

(It is still the case that I should create a new project folder for each PR I'm working on, right? That seems to be what all the guides say.)

[Riccardo Brasca]

I think you have to do something in the command line, but these tricks should save some time.

[Alex J. Best]

There's no need to have a new project for each PR unless you really need the source to be separate, even then if you use git worktree you only need to have one original git repo.

[Wrenna Robson]

Yeah, that's what I would have thought? But that isn't what the guide here says. https://leanprover-community.github.io/contribute/index.html

[Alex J. Best]

Does https://leanprover-community.github.io/tips_and_tricks.html#old-mode (which is what that thread lead to) help with your issues? It is useful even if not running on the commandline

[Alex J. Best]

Wrenna Robson said:

Yeah, that's what I would have thought? But that isn't what the guide here says. https://leanprover-community.github.io/contribute/index.html

Maybe that section should be called, making a first pull request!

[Alex J. Best]

Have you seen https://leanprover-community.github.io/leanproject.html?

[Wrenna Robson]

Yeah - but it implies you have to name the folder after the PR!

[Wrenna Robson]

I have seen that - I am not new to Lean/leanproject! But editing mathlib always seems to go awry so I don't make many PRs.

[Alex J. Best]

Here is my basic workflow:

cd mathlib
git checkout master
git pull # get the latest master
git checkout -b alexjbest/my_new_lemma # make a new branch with this name, that is currently the same as origin master
leanproject get-cache --fallback=download-all
... make edits
git push # <- this will possibly prompt you to do something more specific

[Wrenna Robson]

and mathlib is just a regular ol' git clone of the project?

[Patrick Massot]

leanproject pr my_new_lemma will do most of this for you

[Alex J. Best]

Yes but obtained with leanproject get mathlibintitially

[Wrenna Robson]

Patrick Massot said:

leanproject pr my_new_lemma will do most of this for you

I tried this but it said I didn't have a leanpkg file. I guess that's why I need to do the get?

[Alex J. Best]

Patrick Massot said:

leanproject pr my_new_lemma will do most of this for you

https://leanprover-community.github.io/leanproject.html should be modified to mention this, I don't see it there

[Patrick Massot]

The only difference between leanproject get mathlib and a manual git clone is that leanproject will download compiled lean files for you

[Wrenna Robson]

Right.

[Patrick Massot]

Wrenna Robson said:

Patrick Massot said:

leanproject pr my_new_lemma will do most of this for you

I tried this but it said I didn't have a leanpkg file. I guess that's why I need to do the get?

You should type that in an existing mathlib folder

[Wrenna Robson]

It does feel like https://leanprover-community.github.io/contribute/index.html could be edited to have a "first PR"/"setting up your mathlib environment" and then "PR workflow" section. This is useful stuff here but I might've done it wrong.

[Patrick Massot]

It doesn't really make sense to try to contribute before having ever downloaded mathlib.

[Patrick Massot]

Alex, please feel free to PR additions to the leanproject help webpage.

[Wrenna Robson]

Patrick Massot said:

It doesn't really make sense to try to contribute before having ever downloaded mathlib.

I'm not sure I understand?

[Wrenna Robson]

I have contributed before and I use mathlib all the time.

[Riccardo Brasca]

I think Patrick means that you want to download the oleans before editing anything.

[Wrenna Robson]

Oh - yes definitely.

[Alex J. Best]

Patrick Massot said:

Alex, please feel free to PR additions to the leanproject help webpage.

I unfortunately don't know the right usage of the command, as seen above I do it all by hand, because I wasn't aware of the command till today. For example, must one be on the latest master already to run this, or is that part handled automatically?

[Wrenna Robson]

Well, I created a PR using the above advice! https://github.com/leanprover-community/mathlib/pull/14645

[Wrenna Robson]

for reference:
leanproject get mathlib to get a mathlib copy.

Then leanproject pr branchname, which seemed to checkout master and get the cache too, though I'd already done that.

Then the actual work, and making local git commits etc.

After finish, git push --set-upstream origin branchname, and then I create a PR in github.

[Wrenna Robson]

Now I need to go to a wedding. But would welcome an eye on the PR! It probably needs tags and assignees and stuff - not sure what I should do for that.

[Riccardo Brasca]

Thanks! Can you please fix the title following the Commit Convention?

Also, you can use #backticks even in the PR description.

[Alex J. Best]

And you don't need to worry about assignees really, the only labels that you should add yourself to begin with are awaiting-ci (for when ci still has to run) and awaiting-review when you think it is ready for review.

[Eric Rodriguez]

Ooh, I didn't know abott leanproject pr. I always used gh pr checkout+ get cache manuakly

[Wrenna Robson]

Cool, done.

[Wrenna Robson]

@Riccardo Brasca does that commit message now look kosher?

[Riccardo Brasca]

feat(data/fintype/basic):... is the standard form.

[Wrenna Robson]

Right right. Should I do that even though I have a small edit to another file?

[Riccardo Brasca]

Yes, don't worry about the other file.

[Wrenna Robson]

Cool. Hmm, my build failed, but I can't work out how to see why.

[Riccardo Brasca]

I think it's not your fault. Let's see if it succeed now.

[Wrenna Robson]

Thanks for help on this. As it was the rename didn't make it in anyway.