mathlib4#665 - Data.Stream.Defs

Stream: mathlib4

[Ruben Van de Velde]

This is blocked only on some documentation comments. Is there anyone who's looked at this before? @Yury G. Kudryashov maybe?

[Reid Barton]

Does there need to be documentation (that was not in the original mathlib)?
Documentation is good, but I'd think it shouldn't block the porting process

[Ruben Van de Velde]

The fields need docs now, apparently

[Reid Barton]

Then there should be some kind of #nolint port annotation or whatever to not do it now.

[Kevin Buzzard]

There is, but when I ran into this with traversable monads I decided I should ask instead and then I decided that instead of asking I should just write docs myself as best as I could because that was probably better than no docs.

[Mario Carneiro]

The existing mechanism for this is the nolints.txt file

[Mario Carneiro]

which contains nolints which are "grandfathered in" (by contrast to those which are actually supposed to be suppressed, via the @[nolint] annotation)

[Reid Barton]

"No docs" is better than "docs written to appease the linter because we need to unblock porting dependent modules".

[Reid Barton]

Ideally we would port/align nolints.txt automatically

[Mario Carneiro]

Yes I agree. My litmus test is: If you can write a reasonable doc in less than 1 minute without any research, then do so, otherwise just leave it as is and when the linter complains run build/bin/runLinter --update to update the nolints file

[Eric Rodriguez]

I've added the nolints and merged master. Hopefully this can now get speedily merged.