Upstreaming #help command?

Stream: batteries

[François G. Dorais]

This came up while discussing batteries#948. The #help command family is clearly useful to everyone and nothing about it is Mathlib specific. Any objections to upstreaming?

[Mario Carneiro]

SGTM

[François G. Dorais]

PR batteries#969

[François G. Dorais]

Mathlib PR #17230

[Kim Morrison]

I left some comments; I think this needs more tests.

[Kim Morrison]

Also two other possibilities to consider:

1. I move this direct to Lean. (Either we'd need more tests written by someone else, or I'd need to find the time to write them.)
2. We move this to a standalone repo leanprover-community/lean-help, on the theory that it is clearly useful to everyone. :-)

[François G. Dorais]

I like both these options.

1. That would be great since I can't imagine someone not wanting #help. It's always hard to tell whether something actually fits in Lean's bandwidth.
2. I hadn't thought of that. While I dislike the monolithic model in general, this doesn't feel like something that really needs to be a separate tool.

[Mario Carneiro]

Kim Morrison said:

1. I move this direct to Lean. (Either we'd need more tests written by someone else, or I'd need to find the time to write them.)

I wonder whether you should make a bot that comments this on every PR

[Mario Carneiro]

actually both suggestions could be applied to almost every PR

[François G. Dorais]

Butterfly much!? :-)

[Kim Morrison]

It's no secret that I don't like having a repository without a clearly defined scope upstream of Mathlib. We've thought a bit in the past about the scope of Batteries, but I don't think ever come to a really satisfactory conclusion --- hopefully we can make more progress on this in future (I would suggest that this happens as a maintainers level discussion first).

That said, I make and merge plenty of PRs to Batteries, so I don't think it's entirely fair to say that I would make these suggestions about every PR.

In this particular case, I agree it is a positive change to move #help from Mathlib to Batteries (not necessarily the best possible change, but certainly positive), although as I said above I would like more tests so we're less likely to have mysterious breakages in future.

[Mario Carneiro]

It does seem like a discussion that repeats regularly. I think we should move on from that conversation, because the considerations are the same in every case and at least so far we've determined that batteries is sticking around

[Mario Carneiro]

If you want to move things upstream or start a discussion in the FRO to upstream something in batteries, that's up to you

[François G. Dorais]

I always thought of it as a multistep process.

1. A useful thing appears in Mathlib.
2. The more general utility of said thing is noticed and asked for elsewhere.
3. The thing is moved to Batteries where it gets some updates and more thorough testing.
4. The thing is so useful that it gets moved to Lean (or the FRO decides to build its own copy-thing).

Many steps are skipped in reality but that actually reduces the effectiveness of this process.