Zulip Chat Archive

Stream: new members

Topic: Git-iquette

Damiano Testa (Dec 13 2020 at 05:27):

Dear All,

I feel a little silly about asking this question, but when I started to learn Lean, I also started learning Git at the same time. I have been very conscious of not pushing anything to mathlib, since I did not want to create PRs with my failed attempts.

Now that I am more familiar with the process, I am starting to look back at my practices. Is it ok/expected that I push to mathlib branches with sorrys, commented out bit, errors, unconventional names,...?

So far, I have been keeping them all on my local repository.

Thank you!

Kenny Lau (Dec 13 2020 at 05:29):

yes, just make sure your branch is uninhabited

Kenny Lau (Dec 13 2020 at 05:29):

(and don't crash mathlib!)

Damiano Testa (Dec 13 2020 at 05:30):

uninhabited means that I use a name that is not already taken, right?

crash mathlib...? should I make sure that everything compiles without errors, but possibly with sorrys?

Kenny Lau (Dec 13 2020 at 05:32):

Damiano Testa said:

uninhabited means that I use a name that is not already taken, right?

Yes, exactly

crash mathlib...? should I make sure that everything compiles without errors, but possibly with sorrys?

This just means don't put codes that take 100 years to run, so make sure the code terminates before you push it.

Damiano Testa (Dec 13 2020 at 05:32):

Ok, I will be careful! Thanks!

Kenny Lau (Dec 13 2020 at 05:33):

Some ways for timeouts to happen are having dangerous instances and having looping simp lemmas

Kenny Lau (Dec 13 2020 at 05:33):

both of which can be avoided by making sure #lint is happy

Kenny Lau (Dec 13 2020 at 05:33):

You could also explicitly create an infinite loop, and #lint won't say anything about it, but I guess there would be no reason for you to do that

Damiano Testa (Dec 13 2020 at 05:34):

Ok, I will try to be careful. On my machine, there is a timeout for computations that is fairly short. I will make sure that compiling does not time out on my machine, before pushing it to mathlib

Kenny Lau (Dec 13 2020 at 05:34):

Just ask us if you need help

Damiano Testa (Dec 13 2020 at 05:35):

ok, thanks! at the moment, I am not even sure what there is that I might ask, but I will, as I have questions!

Bryan Gin-ge Chen (Dec 13 2020 at 05:35):

I wouldn't worry too much about crashing the mathlib repo's CI. We're building mathlib with some timeout options that should cause errors if some part takes too long.

If somehow that doesn't catch a loop, the github actions runner will terminate a job after 6 hours no matter what, and we can always manually cancel one before that if we notice something wrong.

Damiano Testa (Dec 13 2020 at 05:37):

Ok, thanks for the reassurance. As much as I can try to be careful, I am bound to push at some point something that times out on my machine and might "crash mathlib". I am just being realistic...

Bryan Gin-ge Chen (Dec 13 2020 at 05:40):

As someone who's hacked a bit on our CI setup, I'm looking forward to the stress tests! :wink:

Damiano Testa (Dec 13 2020 at 05:42):

Ahaha

Still, I will not try to crash mathlib on purpose. At my level, I hope that I am unlikely to crash mathlib anyway.
Yet, crashing something might be easier than accidentally proving a theorem...

Bryan Gin-ge Chen (Dec 13 2020 at 05:53):

One thing to keep in mind is that GitHub actions only lets us have 20 jobs running at the same time. So if possible, I would try to avoid pushing tons of commits (10+) within a short period of time (<2h). I think we haven't been close to hitting the limit in a while, but minimizing the number of jobs is a good idea anyways (more environmentally friendly).

Eric Wieser (Dec 13 2020 at 08:19):

Regarding ensuring the branch is uninhabited, I've mostly been pushing to branches named my-username/mybranch, which pretty much guarantees I can only clobber my own work and not anyone elses

Last updated: Dec 20 2023 at 11:08 UTC