leanproject build deletes changes

Stream: general

[Rémy Degenne]

Doing leanproject build just deleted all my uncommited changes in the affected folder (including deleting a new file). I can reproduce it: I write something in a mathlib file, save, execute leanproject build, and the change is gone.
Is is a problem of my installation? Has leanproject been recently modified such that it is now supposed to do that? Any idea of how I can modify that behaviour or what additional info I could look for to understand what happens?

[Rémy Degenne]

a more detailed account of what I did: I created a branch l2_space on the mathlib github page, did leanproject get -b mathlib:l2_space, wrote some changes, did leanproject build, and my folder is back to the state it was in after leanproject get -b mathlib:l2_space.

[Eric Wieser]

https://github.com/leanprover-community/mathlib-tools/pull/96 fixes this. leanproject has always behaved like this, as far as I can tell

[Rémy Degenne]

It feels like it never did this to me before yesterday but I must be wrong.

[Rémy Degenne]

Thankfully I lost only some copy/pasted things from another folder, so I lost only 10min really.

[Rémy Degenne]

I'll be careful. Thanks for the reply!

[Eric Wieser]

I'm now just using that branch instead of the released version of mathlibtools, as I've blown away files multiple times this way and don't want to risk it any more.

[Bolton Bailey]

Yep, this just happened to me as well. Is it possible yet to update to a version of leanproject that doesn't have this problem?

[Kevin Buzzard]

Why not just do lean --make src? This has the extra advantage that you can add -M6000 and stop Lean from taking your desktop down.

[Bolton Bailey]

Great advice. If lean --make src is the better practice though, it seems like the guidance on the contribution guidelines page should say to do this rather than leanproject build. Can this be changed?

[Rémy Degenne]

Personally, I think the reason I did leanproject build and was caught by that issue once was that I followed the instructions on the "how to contribute page" https://leanprover-community.github.io/contribute/index.html . It states among other steps:

• edit the necessary files, e.g. src/data/set/basic.lean
• If you are anxious, leanproject build to check you didn't break anything.

[Bolton Bailey]

Wow, it seems we made the same comment at the same time

[Kevin Buzzard]

Oh I see! I hadn't realised that the claim was that the instructions are explicitly telling people to nuke their work!

[Patrick Massot]

Eric Wieser said:

https://github.com/leanprover-community/mathlib-tools/pull/96 fixes this. leanproject has always behaved like this, as far as I can tell

I'm pretty sure this bug was not present in the beginning. It was introduced when tweaking stuff. Eric, I think I was waiting for action from your side in this PR. Are you still interested in working on this?

[Eric Wieser]

Yeah, the ball is definitely in my court here. I realized that that PR messed up the workflow for people not working on mathlib, and haven't gotten around to getting back to it