!4#2994 NumberTheory.LegendreSymbol.MulCharacter

Stream: PR reviews

[Damiano Testa]

I checked out the PR, merged master and there were no errors, except some docs linter. I fixed those. Is it ok if I simply push back to GitHub? Do I need permissions to do so?

Thanks!

[Matthew Ballard]

You should be able to push it.

[Damiano Testa]

ERROR: Permission to leanprover-community/mathlib4.git denied to adomani.
fatal: Could not read from remote repository.

Please make sure you have the correct access rights
and the repository exists.

It is the first time that I work on mathlib4...

[Matthew Ballard]

@maintainers

[Scott Morrison]

@Damiano Testa, invite sent!

[Scott Morrison]

Sorry, I saw your earlier message, and assumed you'd already have access copied across from mathlib3 at some earlier point.

[Damiano Testa]

Thank you! PR pushed! Now I will see if there was really nothing left to do! :smile:

[Damiano Testa]

No, I've been away from Lean for quite some time and never started with the port, unfortunately.

[Matthew Ballard]

Scott Morrison said:

Sorry, I saw your earlier message, and assumed you'd already have access copied across from mathlib3 at some earlier point.

I also thought permissions were org wide.

[Damiano Testa]

There is a failure of the simpNF linter in a different file, here and the next lemma. However, #lint locally reports no issue. Should I just remove the @[simp] tags and see what happens?

[Matthew Ballard]

Yeah see if it breaks anything in the file. Then maybe backport the removal of simp attributes to check it doesn't break any depedent?

[Matthew Ballard]

These kinds of simpNF failures are annoying

[Damiano Testa]

All checks passed with the removal of the simp lemmas!

[Eric Wieser]

I assume you only removed the _attributes_ in !4#2994?

[Eric Wieser]

Note that the CI linter does not require you to add docstrings

[Damiano Testa]

Ah, sorry, I misspoke: I removed the tags! Btw, they are in a different file from the ported one, so they stand out.

[Damiano Testa]

As for the docstrings, I still think that they add the human touch...

[Eric Wieser]

The danger of adding docstrings while porting is that the people reviewing them are less likely to be familiar with the content than if you made a standalone doc PR

[Damiano Testa]

I did not think of this: as I jumped in after all the hard work had been done, I was just happy to contribute something... Should I remove the docstrings?

[Damiano Testa]

I added comments to the PR for the two added docstrings: this way, they are at least documented.