Zulip Chat Archive
Stream: general
Topic: Lean 3.8 library changes
Yury G. Kudryashov (Mar 24 2020 at 16:59):
I created an issue to track proposed changes to the core library. Additions are welcome, and I guess PRs are even more welcome.
Yury G. Kudryashov (Mar 24 2020 at 18:40):
What's the policy for non-master branches in leanprover-community/lean?
Yury G. Kudryashov (Mar 24 2020 at 18:43):
Mario Carneiro (Mar 24 2020 at 18:43):
I would say same as mathlib
Gabriel Ebner (Mar 24 2020 at 18:43):
It's completely different from mathlib.
Mario Carneiro (Mar 24 2020 at 18:44):
there should probably be some policy about not tagging though
Gabriel Ebner (Mar 24 2020 at 18:44):
In mathlib, it is important that you use branches in the leanprover-community organization because the CI produces oleans. In the lean repo there is no such benefit.
Gabriel Ebner (Mar 24 2020 at 18:45):
But if you have write access, feel free to create branches in the lean repo.
Mario Carneiro (Mar 24 2020 at 18:45):
the original reason we started using leanprover-community branches in mathlib was to make collaboration easier
Yury G. Kudryashov (Mar 24 2020 at 18:45):
I don't have write access to the lean repo. Forked & made a PR.
Mario Carneiro (Mar 24 2020 at 18:45):
multiple people can commit to the same branch without having to PR to a PR
Yury G. Kudryashov (Mar 24 2020 at 18:46):
Side effect of me having no write access: I can't assign milestones/labels.
Gabriel Ebner (Mar 24 2020 at 18:47):
Ah, ok then we need to hand out write access.
Gabriel Ebner (Mar 24 2020 at 18:47):
Who wants write access on the Lean repo?
Yury G. Kudryashov (Mar 24 2020 at 18:51):
Me.
Gabriel Ebner (Mar 24 2020 at 18:51):
Added.
Bryan Gin-ge Chen (Mar 24 2020 at 18:52):
Me too. Perhaps people who have submitted PRs in the past should get an invitation?
Gabriel Ebner (Mar 24 2020 at 18:52):
I'm currently going through the list.
Gabriel Ebner (Mar 24 2020 at 18:55):
I hope I didn't miss anybody. Feel free to ask for write access on the Lean repo if I didn't invite you already.
Gabriel Ebner (Mar 24 2020 at 18:57):
The rules are the same as for mathlib: create branches as you like, try to make PRs from branches of the Lean repo, assign/tag issues if you want.
Yury G. Kudryashov (Mar 25 2020 at 21:01):
CI seems to be stuck on lean#161
Bryan Gin-ge Chen (Mar 25 2020 at 21:05):
Here's the job on travis. I just restarted the one macOS build that failed.
(BTW, if you write lean#161 it will link to the right PR.)
Bryan Gin-ge Chen (Mar 25 2020 at 21:11):
Uh oh, it looks like that macOS job has been timing out pretty consistently recently, and when it does succeed it's always very close to the 50 min time limit. (compare 1 2 3).
Gabriel Ebner (Mar 25 2020 at 21:52):
Yes this is a known issue.
Yury G. Kudryashov (Mar 28 2020 at 01:30):
It timed out again.
Last updated: Dec 20 2023 at 11:08 UTC