Zulip Chat Archive

Stream: condensed mathematics

Topic: CI failing


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

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.

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

Hmm, I can look into in when I'm on the train (45 mins from now)

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

docstrings are very welcome!!

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

you should probably glance over my commits from a couple of days ago to check I'm not writing nonsense!

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

ok, will do

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

It is embarrassing how much of the theory I have forgotten

Johan Commelin (Apr 02 2022 at 11:47):

@Kevin Buzzard Those commits look great!


Last updated: Dec 20 2023 at 11:08 UTC