Zulip Chat Archive

Stream: new members

Topic: Polynomial evaluation


view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 21 2020 at 16:53):

I would generalise the ring and the finset

view this post on Zulip Johan Commelin (Aug 21 2020 at 16:53):

See mv_polynomial.eval_prod

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Dan Stanescu (Aug 21 2020 at 23:52):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Aug 21 2020 at 23:59):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Aug 22 2020 at 00:09):

  1. write #lint at the bottom of a file

view this post on Zulip Scott Morrison (Aug 22 2020 at 00:10):

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

view this post on Zulip 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