## Stream: new members

### Topic: Polynomial evaluation

#### Dan Stanescu (Aug 21 2020 at 16:52):

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 (Aug 21 2020 at 16:53):

I would generalise the ring and the finset

#### Johan Commelin (Aug 21 2020 at 16:53):

See mv_polynomial.eval_prod

#### Dan Stanescu (Aug 21 2020 at 23:50):

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 (Aug 21 2020 at 23:51):

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

#### Dan Stanescu (Aug 21 2020 at 23:52):

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

#### Bryan Gin-ge Chen (Aug 21 2020 at 23:54):

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 (Aug 21 2020 at 23:56):

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 (Aug 21 2020 at 23:58):

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 (Aug 21 2020 at 23:59):

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

#### Scott Morrison (Aug 22 2020 at 00:05):

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 (Aug 22 2020 at 00:06):

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 (Aug 22 2020 at 00:08):

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 (Aug 22 2020 at 00:09):

1. write #lint at the bottom of a file

#### Scott Morrison (Aug 22 2020 at 00:10):

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

#### Scott Morrison (Aug 22 2020 at 00:10):

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

Last updated: May 09 2021 at 18:17 UTC