Zulip Chat Archive

Stream: condensed mathematics

Topic: master/dev

Johan Commelin (Jul 17 2022 at 22:32):

I suggest that we no longer casually push to master. Instead, we should do all our work on branches. Adam and I can then merge updates to master when they are ready. In this way, we can make sure that we preserve the green checkmark on master.

I suggest dev as the main development branch, but I also encourage the use of short-lived feature branches.

Adam Topaz (Jul 17 2022 at 22:54):

FYI: I just created some branch protection rules that should prevent accidental pushes to master.
They should now require an approval on a PR and a passing CI to be merged.

Filippo A. E. Nuccio (Jul 18 2022 at 07:27):

And are the other non-master branches can we push freely?

Johan Commelin (Jul 18 2022 at 08:54):

Yes, that should just work as usual.

Ben Toner (Jul 18 2022 at 13:19):

@Johan Commelin Currently we only store oleans for builds on master. Is it okay with you if I change the CI so that we also store oleans for non-master branches?

Johan Commelin (Jul 18 2022 at 13:20):

Hmmm, would be fine with me. But let me check with the people who pay for the storage.

Ben Toner (Jul 18 2022 at 13:25):

cool -- i would guess < $10/year but let me know if you want me to work it out

Adam Topaz (Jul 18 2022 at 14:14):

Quick update: we removed the branch protection rule about nolints. The CI checks are now:

  1. Successful build
  2. Successful lint
  3. liquid_tensor_experiment stays sorry-free

Johan Commelin (Jul 20 2022 at 11:16):

@Ben Toner If you could enable this for non-master branches, that would be great. Our mathlib-bump branches will greatly benefit from it.

Ben Toner (Jul 20 2022 at 11:49):

part 1: https://github.com/leanprover-community/lean-liquid/pull/102

Ben Toner (Jul 20 2022 at 11:50):

part 2, coming soon, is stopping the clean-up script from deleting them

Johan Commelin (Jul 20 2022 at 11:50):

I suggest we merge this after the mathlib bump. That one should auto-merge in ~30 mins.

Ben Toner (Jul 20 2022 at 11:55):

Ugh, I messed up your auto-merge by pushing my changes to the bump_may_19 change as well (so we wouldn't have to rebuild after merge). Sorry, I didn't know auto-merge was a thing.

Eric Wieser (Jul 20 2022 at 12:35):

You could force-push to undo those two commits

Eric Wieser (Jul 20 2022 at 12:35):

Then it could be merged now

Ben Toner (Jul 20 2022 at 12:42):

better to leave it running -- if i push again it'll just interrupt CI again

Last updated: Dec 20 2023 at 11:08 UTC