## 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?

lean#161

#### 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

#### 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?

Me.

#### 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: May 08 2021 at 10:12 UTC