Zulip Chat Archive

Stream: general

Topic: Lean 3.8 library changes


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

view this post on Zulip Yury G. Kudryashov (Mar 24 2020 at 18:40):

What's the policy for non-master branches in leanprover-community/lean?

view this post on Zulip Yury G. Kudryashov (Mar 24 2020 at 18:43):

lean#161

view this post on Zulip Mario Carneiro (Mar 24 2020 at 18:43):

I would say same as mathlib

view this post on Zulip Gabriel Ebner (Mar 24 2020 at 18:43):

It's completely different from mathlib.

view this post on Zulip Mario Carneiro (Mar 24 2020 at 18:44):

there should probably be some policy about not tagging though

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

view this post on Zulip Gabriel Ebner (Mar 24 2020 at 18:45):

But if you have write access, feel free to create branches in the lean repo.

view this post on Zulip Mario Carneiro (Mar 24 2020 at 18:45):

the original reason we started using leanprover-community branches in mathlib was to make collaboration easier

view this post on Zulip Yury G. Kudryashov (Mar 24 2020 at 18:45):

I don't have write access to the lean repo. Forked & made a PR.

view this post on Zulip Mario Carneiro (Mar 24 2020 at 18:45):

multiple people can commit to the same branch without having to PR to a PR

view this post on Zulip Yury G. Kudryashov (Mar 24 2020 at 18:46):

Side effect of me having no write access: I can't assign milestones/labels.

view this post on Zulip Gabriel Ebner (Mar 24 2020 at 18:47):

Ah, ok then we need to hand out write access.

view this post on Zulip Gabriel Ebner (Mar 24 2020 at 18:47):

Who wants write access on the Lean repo?

view this post on Zulip Yury G. Kudryashov (Mar 24 2020 at 18:51):

Me.

view this post on Zulip Gabriel Ebner (Mar 24 2020 at 18:51):

Added.

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

view this post on Zulip Gabriel Ebner (Mar 24 2020 at 18:52):

I'm currently going through the list.

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

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

view this post on Zulip Yury G. Kudryashov (Mar 25 2020 at 21:01):

CI seems to be stuck on lean#161

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

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

view this post on Zulip Gabriel Ebner (Mar 25 2020 at 21:52):

Yes this is a known issue.

view this post on Zulip Yury G. Kudryashov (Mar 28 2020 at 01:30):

It timed out again.


Last updated: May 08 2021 at 10:12 UTC