Zulip Chat Archive

Stream: mathlib4

Topic: mathlib4#665 - Data.Stream.Defs


Ruben Van de Velde (Dec 01 2022 at 15:49):

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

Reid Barton (Dec 01 2022 at 16:57):

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 (Dec 01 2022 at 16:57):

The fields need docs now, apparently

Reid Barton (Dec 01 2022 at 17:05):

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

Kevin Buzzard (Dec 01 2022 at 20:28):

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 (Dec 01 2022 at 20:48):

The existing mechanism for this is the nolints.txt file

Mario Carneiro (Dec 01 2022 at 20:48):

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

Reid Barton (Dec 02 2022 at 07:47):

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

Reid Barton (Dec 02 2022 at 07:47):

Ideally we would port/align nolints.txt automatically

Mario Carneiro (Dec 02 2022 at 08:42):

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 (Dec 02 2022 at 10:07):

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


Last updated: Dec 20 2023 at 11:08 UTC