leanproject upgrade-mathlib

Stream: new members

[Bolton Bailey]

I ran leanproject upgrade-mathlib to get access to one the lemmas I edited which was recently merged. After doing this I started getting a huge number of errors - for example

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

I also started getting messages saying things like

imported file '/Users/boltonbailey/Desktop/myproject/_target/deps/mathlib/src/data/polynomial/eval.lean' uses sorry

Not sure why I should ever get this message for a mathlib file. Can anyone troubleshoot what is going on?

Another thing - If I leanproject new to make a fresh project and copy my /src folder into it, everything works fine.

[Johan Commelin]

@Bolton Bailey did you restart lean in VScode, after upgrading mathlib?

[Bolton Bailey]

no let me try that

[Bolton Bailey]

Yep, this seems to have fixed it. Thank you.

[Bryan Gin-ge Chen]

This seems to be a common stumbling block. I wonder if there's a way for the extension to detect that it needs to be restarted? Or perhaps leanproject could output a reminder.

[Johan Commelin]

emacs seems to handle this fine, fwiw

[Bryan Gin-ge Chen]

Interesting! I wonder what lean-mode does differently.

[Bolton Bailey]

I was just following the instructions on https://leanprover-community.github.io/leanproject.html so a reminder there would be helpful.

[Bryan Gin-ge Chen]

I opened a PR: https://github.com/leanprover-community/leanprover-community.github.io/pull/164

Let me know if there's anything I should add / modify.

[Bolton Bailey]

Seems good to me.