## Stream: general

### Topic: leanproject build deletes changes

#### Rémy Degenne (Mar 08 2021 at 08:49):

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 (Mar 08 2021 at 08:53):

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 (Mar 08 2021 at 08:54):

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 (Mar 08 2021 at 08:56):

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

#### Rémy Degenne (Mar 08 2021 at 08:57):

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

#### Rémy Degenne (Mar 08 2021 at 09:00):

I'll be careful. Thanks for the reply!

#### Eric Wieser (Mar 08 2021 at 09:01):

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 (Apr 26 2021 at 18:03):

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 (Apr 26 2021 at 18:45):

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 (Apr 26 2021 at 18:50):

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 (Apr 26 2021 at 18:50):

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 (Apr 26 2021 at 18:51):

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

#### Kevin Buzzard (Apr 26 2021 at 19:00):

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

#### Patrick Massot (Apr 26 2021 at 21:03):

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 (Apr 26 2021 at 22:25):

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

Last updated: May 14 2021 at 00:42 UTC