Zulip Chat Archive

Stream: general

Topic: leanproject build deletes changes


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rémy Degenne (Mar 08 2021 at 09:00):

I'll be careful. Thanks for the reply!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Bolton Bailey (Apr 26 2021 at 18:51):

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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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