multiple goals

Stream: batteries

[Kim Morrison]

I was perhaps slightly hasty in merging batteries#895, which I see now as I'm repairing it on nightly-testing has a number of proofs that have multiple goals that are not managed using focus notation, e.g. at https://github.com/leanprover-community/batteries/pull/895/files#diff-7f6f2022caefd253ab58d36270f54286b95fdf21e1e8199626ab9f22f3d1e5efR190

1. I presume we agree this isn't great style and should be avoided where possible.
2. Does Mathlib have a linter for it? Can we have it?

[Damiano Testa]

The linter is written, and @Michael Rothgang has been helping to push it through, but there are a huge number of exceptions.

[Damiano Testa]

Btw, Michael is not subscribed to this channel, so he won't feel summoned.

[Damiano Testa]

It is called the multiGoals linter but I'm on mobile and can't give you the PR number.

[Damiano Testa]

Actually, #12339 may be it

[Damiano Testa]

The linter only checks for missing focusing dots, not for unnecessary ones.

[Damiano Testa]

There is a PR with an extension to the linter that does that, but since progress on the initial multiGoal linter was slow, I left it dormant.

[Kim Morrison]

Thanks for the update. No urgency on this, mostly this gets caught in review (and in this case I was the reviewer so I'm not blaming anyone! :-)

[Mario Carneiro]

Agreed we should enable and enforce this on batteries

[Damiano Testa]

As far as testing goes, I was quite pleased with how the linter worked on Mathlib. If you want to try it out on batteries, at least to add some focusing dots, it should be pretty smooth sailing.

[Damiano Testa]

I forget exactly what happens, but I seem to recall that if you blindly add a focusing dot on the first line flagged by the linter and indent all the lines flagged by the linter, it should magically work.

[Damiano Testa]

(Recursively, sometimes.)

[Damiano Testa]

The intention was to make it as self-correcting as possible. I was going to plug it into a "refactor"-like step, but that is on hold for both the linter and refactor! :smile:

[Damiano Testa]

I'm giving the PR another push, but splitting out the focusing dots into 3 smaller PRs: #17313, #17314, #17315. I'm mentioning it here, in case someone might be interested in reviewing... :smile:

[Kim Morrison]

Left comments on all of them. I find the on_goals confusing.

[Damiano Testa]

I removed most of the on_goals: their use, in the context of the linter, is usually to maintain a proof where a tactic generates multiple goals, you massage the first goal a bit, and then you discharge all goals (the massaged one and the remaining ones) with all_goals or something similar.

[Damiano Testa]

There was discussion about making this proof startegy (delaying side-goals until something has happened), and a couple of prototypes, but nothing concrete.

So, I resorted to using on_goals, to not drag the process further.

[Damiano Testa]

For reference, this conversation (and the one linked from there) was the discussion about the side-goals.