Be careful when renaming widely used identiers

Stream: general

[Weiyi Wang]

This is just a funny little thing that happened to me. I was working on adding stuff to mathlib, and when renaming identifiers using the "Rename Symbol" feature, I accidentally renamed One(the class in Init.Prelude).
The next thing that happened was vscode running through the entire mathlib to rename all occurrence of One, eating all the RAM, making everything unresponsive and eventually it crashed my pc.
And this was not the end. The rename wasn't saved in mathlib, but saved as "unsaved edits" in vscode. vscode will automatically open these files upon opening the project with a little dot indicating there was unsaved edits from last time. So when I open mathlib again, it opened thousands of files it edited last time, firing lean server up again. I couldn't use the "close all" button because it just ask me about unsaved change one by one, and the it just eat all RAM again in the background. Quite a stalemate.

If you ever get yourself in this situation, here is how I resolved it:

• rename the mathlib folder so vscode recognize it as a new project
• delete the unsaved file cache. On linux it is ~/.config/Code/Backups. Not sure about other OS