Zulip Chat Archive

I found some time to work on LTE last week (and hope to find a lot more time to work on it this week). I filled in some sorries and pushed directly to master. I just noticed that my most recent push has a red x on CI and a complaint about a linter not working. Is this expected behaviour? The project itself seems to build fine (but I didn't lint locally). https://github.com/leanprover-community/lean-liquid/runs/5777741280?check_suite_focus=true

Johan Commelin (Apr 02 2022 at 09:51):

It's probably due to 537 missing docstrings

Kevin Buzzard (Apr 02 2022 at 09:55):

my most recent PR was adding one :-) It is certainly the case that getting back into the project is made harder by the lack of docstrings; every time I want to know what a def is and the docstring isn't there, I just PR it :-) But the actual error talks about a missing log rather than missing docstrings. I would happily PR docstrings, at least in areas which I hope to be working on in the near future.