shake --update does not work

Stream: general

[Yaël Dillies]

I tried running lake exe shake LeanAPAP --update within LeanAPAP and I got the following output

gitpod /workspace/LeanAPAP (master) $ lake exe shake LeanAPAP --update
././././LeanAPAP/Prereqs/Convolution/Order.lean:
  remove #[LeanAPAP.Mathlib.Tactic.Positivity]
././././LeanAPAP/Prereqs/Expect/Order.lean:
  remove #[Mathlib.Data.Real.Basic, LeanAPAP.Prereqs.Expect.Basic]
  add #[Mathlib.Tactic.Positivity.Core]

[Yaël Dillies]

... but nothing happened. No noshake.json file was created nor did it error saying that it couldn't create the file. I thought maybe it did fail to create the file and just didn't report it, so I created scripts/noshake.json and rerunning the command resulted in this very weird output!

gitpod /workspace/LeanAPAP (master) $ lake exe shake LeanAPAP --update
warning: mathlib: repository '././.lake/packages/mathlib' has local changes

[Yaël Dillies]

@Mario Carneiro, is shake --update in a downstream project even supported?

[Yaël Dillies]

Ahah, I figured out what happened: My first lake exe shake LeanAPAP --update updated the scripts/noshake.json within mathlib rather than the one in LeanAPAP