Polynomial evaluation

Stream: new members

[Dan Stanescu]

Hi all: I need advice on whether this somewhat specific polynomial evaluation lemma (and the corresponding finset.sum) should be PRd into mathlib (data.polynomial.eval.lean). I need to use it pretty heavily for the case of polynomials over ℝ, but I guess it could be extended to [comm_semiring R]. The proof is rather simple hence omitted.

lemma polynomial.eval_finset.prod (n : ℕ) (p : ℕ → polynomial ℝ) (x : ℝ):
    polynomial.eval x ( ∏ j in finset.range n, p j) =   ∏ j in finset.range n, polynomial.eval x (p j) := sorry

[Johan Commelin]

I would generalise the ring and the finset

[Johan Commelin]

See mv_polynomial.eval_prod

[Dan Stanescu]

Is there anything we should do if all checks of CI on a PR are successful except linting? I see there are lots of PRs in the same situation lately.

[Bryan Gin-ge Chen]

I think most contributors don't mind if you push a commit that fixes linting errors.

[Dan Stanescu]

OK, then the problem is that I have no idea about linting at all.

[Bryan Gin-ge Chen]

Ah, you can check the logs from CI to see what the errors are. Let me see if there's a good example.

[Bryan Gin-ge Chen]

You can click on "Details" next to the failed check on a PR and then click next to the linting step to see errors. The log should tell you what's wrong and how to fix it. For example, the linting errors on #3903 are here: https://github.com/leanprover-community/mathlib/pull/3903/checks?check_run_id=1014500486#step:5:8

[Dan Stanescu]

Thanks @Bryan Gin-ge Chen !

OK, so just to be sure: the person who opened the PR is always supposed to fix the linting errors. Correct?

[Bryan Gin-ge Chen]

Yes, they're held responsible (unless they state otherwise in a comment).

[Scott Morrison]

But I think one should assume unless said otherwise that it's okay to directly fix other people's linting errors if you feel so inclined.

[Scott Morrison]

The original author is responsible for shepherding the PR all the way through to completion (including linting), but it's a collaborative process, and it's super useful, and appreciated, when others either make suggestions via the github interface, or just push commits fixing things.

[Dan Stanescu]

I need a little more help so I can be more efficient myself.
First off, is there anything one can do to check linting before a PR?
Second, I do realize what the first error is and how to fix it. But the second, I'm not sure: I have {ι : Type*} [decidable_eq ι] in my arguments and the linter wants to replace with classical. Not sure how to do that in one lemma.
And third, if I fix these linting errors myself, how do I ask the system to check again?

[Scott Morrison]

1. write #lint at the bottom of a file

[Scott Morrison]

2. just delete those hypotheses, and run thee classical tactic at the beginning of the proof

[Scott Morrison]

3. push a new commit to the PR branch, and continuous integration will automatically re-run the linter