github notifications

Stream: general

[Sean Leather]

Does anyone (with the right repository permissions) want to create streams and bots for GitHub notifications from https://github.com/leanprover/lean and https://github.com/leanprover/mathlib ?

[Mario Carneiro]

You should already be receiving notifications from mathlib, on the #travis stream. I doubt I can set up hooks for the lean repo since it inexplicably requires modifying the travis build script

[Sean Leather]

I'm referring to issues, PRs, comments, and commits, not Travis CI.

[Mario Carneiro]

well, I certainly can't, you need to be admin on the repo to set it up I think

[Sean Leather]

Exactly. :smile: Are you not an admin on mathlib?

[Mario Carneiro]

Nope, this is part of the reason I would prefer to move development elsewhere

[Mario Carneiro]

I'm just a really active contributor with push access

[Sean Leather]

Nope, this is part of the reason I would prefer to move development elsewhere

It sounds like there's more context to this statement that I am not aware of.

[Moses Schönfinkel]

Mario is going rogue.

[Mario Carneiro]

Mario is trying to figure out how to fork lean without making life more horrible for everyone

[Sean Leather]

It would be a shame to have fewer collaborators on and contributions to such a fork, were it to exist.

[Simon Hudon]

Is it still because of the instance situation?

[Mario Carneiro]

It's mostly been a politics thing - I don't think Leo is cultivating a good environment for an OSS to develop with his approach to PRs and issues management. The instance thing caused some of these problems to come to the fore, and although that's no longer directly an issue the problems have been there for a while and have not gone away. As it is, we're in a bit of a holding pattern, and I have no wish to lose collaborators and the like so I don't know whether there is a good way forward that avoids this

[Simon Hudon]

Did he explain why he's doing things this way?

[Simon Hudon]

I mean, is there some sort of dialogue going on that might help mitigate the situation?

[Mario Carneiro]

No, that is of course part of the problem. I have traded less than a hundred words with Leo since summer (when I met him in person)

[Simon Hudon]

You're in Jeremy's team right?

[Mario Carneiro]

I know very well why he's doing this though - he has no interest in managing general maintenance stuff and definitely doesn't want to maintain mathlib (not that I've ever asked him to), I think he's shellshocked from having to do this in lean 2. He has his projects to complete, and the other stuff is sucking out his enjoyment and stressing him out

[Mario Carneiro]

yes

[Simon Hudon]

Your team seems like such a big part of Lean. Does Leo appreciate your contribution?

[Sean Leather]

I think the comments on leanprover/lean#1521 are indicative of Leo's approach.

[Mario Carneiro]

I will let Leo answer that question himself

[Simon Hudon]

I'll have to look at that closely. Thanks! Btw, I see you seemed interested in coinductive types. You might be interested in my current PR: https://github.com/leanprover/mathlib/pull/71

[Simon Hudon]

I feel like I must sound a bit like a marriage counsellor but it seems like if he doesn't value your work, it will be hard to get him to make any kind of concession. I wonder if there's something he wishes you'd do (beside drop mathlib :stuck_out_tongue_closed_eyes: )

[Sean Leather]

Me: :smile:

In case it wasn't clear, I didn't mean to pick these out because I wanted to know about them. They were merely examples.

And, yes, I'm aware of your PR. And I'm impressed by it.

[Sean Leather]

@Simon Hudon: I think that is an example of how you go against Leo's assumptions:

On the other hand, you should not hold your breath for coinductive datatypes. They will not happen in the following years, unless someone as strong as @gebner or @Kha shows up and decides to implement this feature.

[Simon Hudon]

Thanks :) I can't compare myself to @Gabriel Ebner or @Sebastian Ullrich but it looks to me that something that does the job 30% of the way is better than nothing (at least for me). So let's just see how far I can get with it.

[Mario Carneiro]

I'm not totally sure about Simon's approach as a final solution for all coinductive datatypes, including nested inductive/coinductives and other things that might be nice, so I'm not sure how much it is worth focusing on extending the capabilities of the package if we are going to move to something else later

[Mario Carneiro]

Specifically, I want to see if the BNF approach used in isabelle also works for lean

[Mario Carneiro]

That said, I am certainly happy to have a decent coverage of basic coinductive types and will merge Simon's PR when it stabilizes

[Simon Hudon]

Thanks for the comment. I believe you're referring to Johannes' paper. I'm still learning that stuff so when I wrap my head around that BNF stuff, I may well try it out.

[Sebastian Ullrich]

Decoupling Lean is certainly on both Leo's and my wish list. As Mario wrote in another topic, things like a command for coinductive types should be written purely in Lean in the future, and it shouldn't matter whether this happens in the core lib or a separate package. I'll get to decoupling users from the Lean master... sometime this week.

[Sebastian Ullrich]

To go back to the original topic, we can add commit RSS feeds for arbitrary repos. Personally, that would be sufficient for me since I already get e-mails about all the other things by following the repos on Github.

[Kevin Buzzard]

To go back to the original topic, we can add commit RSS feeds for arbitrary repos. Personally, that would be sufficient for me since I already get e-mails about all the other things by following the repos on Github.

Lean and mathlib, please :-)

[Sebastian Ullrich]

Ah, you need a Python bot running somewhere for that. Yeah, no.