Workflow

Stream: general

[Yaël Dillies]

To keep @Oleksandr Manzyuk discussion, out of #PR reviews, here are a few ideas I have to accelerate the mathlib workflow:

• Allow cache cherry-picking. Often, I want to work on some feature which depends on a previous one very low down in the import tree, but I don't care about recompiling everything in between because I trust hardly anything will break and fixing what does is part of the original branch's work. So a button to change the cache of the single file low down in the import tree to the one with the first new feature would allow me to work on the second one without waiting.
• Do not run the Infoview on VScode's diff view, or run it on a separate instance. Before committing, I usually check what my diff is from VScode and BEM Lean runs on the original version of the file which is shown on the left. When I work on several files in parallel, this means that I have to wait for all files to recompile to continue working (and they are sometimes quite far)

[Yury G. Kudryashov]

I use --old instead of idea 1