Zulip Chat Archive

Stream: new members

Topic: Order of checks in CI

Stuart Presnell (Mar 31 2022 at 22:55):

What's the order in which checks are performed in the GitHub CI? I ask because I've just had a commit fail CI (on #13086), seemingly because I forgot to provide docstrings for some defs — but this failure only arose after 101 minutes had been spent on the "Build mathlib" phase.

Eric Wieser (Mar 31 2022 at 22:57):

In principle the docstring could have been added in minute 100

Eric Wieser (Mar 31 2022 at 22:57):

With add_decl_doc

Eric Wieser (Mar 31 2022 at 22:57):

So you really can't run that linter accurately without building everything

Eric Wieser (Mar 31 2022 at 22:58):

Of course, the linter could become the stricter "has a docstring in the same file", but we don't have infrastructure to run linters in parallel with the build yet

Stuart Presnell (Mar 31 2022 at 23:03):

Doesn't adding a docstring for foo just involve a line like add_decl_doc foo? So you could search the entire codebase for that without having to spend 100 minutes building all of mathlib.

Reid Barton (Mar 31 2022 at 23:05):

In practice do we add docstrings to declarations from a different file? (Outside of cases where we add docstrings to definitions in the core library perhaps.)

Eric Wieser (Mar 31 2022 at 23:23):

Stuart, you can't tell whether add_decl_doc in the last file is a command or not until you've parsed all the notation up till that point

Eric Wieser (Mar 31 2022 at 23:23):

The only way to parse lean reliably is to compile it, and that's what we're already doing

Eric Wieser (Mar 31 2022 at 23:26):

Obviously I'm describing pathological cases that we don't care about, but hopefully that gives some insight into why it's last fragile to do it a different way to what we currently do

Stuart Presnell (Mar 31 2022 at 23:29):

But in the present case the def had no adjacent docstring and there's nothing that could be a candidate add_decl_doc ... in the codebase. Isn't it worth spending a few milliseconds doing a quick search that will occasionally find a definite failure quickly?

Reid Barton (Mar 31 2022 at 23:34):

PRs welcome :upside_down:

Reid Barton (Mar 31 2022 at 23:34):

TBH, I do find this sort of thing very annoying as well.

Stuart Presnell (Mar 31 2022 at 23:38):

Unfortunately I don't know where I'd even start with writing the relevant code, or even where I'd look for examples of the code that currently runs the CI.

Stuart Presnell (Mar 31 2022 at 23:39):

Is there someone suitably knowledgable and keen that we could bat-signal on this? :smile:

Damiano Testa (Apr 01 2022 at 01:44):

You could have a quick check on your computer, where you grep a couple of lines above every def and make sure that the string -/ is present. Maybe only on the diff with the previous commit or on a single file.

Not a full check, but might catch some actually missing doc-strings.

Bryan Gin-ge Chen (Apr 01 2022 at 01:45):

What I usually do is put #lint at the bottom of the file. It'd be nice if the linters had nicer integration with VS Code, but that's not likely to happen until we port them over to Lean 4.

Yaël Dillies (Apr 01 2022 at 09:28):

On the other hand, something has to be checked last. There is no point in cyclically prioritising some check because "it would have caught my error faster".

Reid Barton (Apr 01 2022 at 10:05):

True but imagine you have two checks that take 1 and 10000 seconds respectively--on average you will be much better off doing the cheap check first, and no one will complain that they had to wait an extra second to get their failure after 10001 seconds.

Stuart Presnell (Apr 01 2022 at 13:13):

And moreover every time the cheap check fails that's 10000 seconds of redundant computation that you've avoided, meaning more resources for other users, better scalability as mathlib and its user-base grows, and (as a side benefit) less unnecessarily wasted electricity.

Stuart Presnell (Apr 01 2022 at 13:19):

I always feel a small (but surely disproportionate) twinge of guilt whenever I make the CI computers do work needlessly. If I wanted to get computers to waste power and generate heat for no purpose at all I'd have invested in bitcoin!

Last updated: Dec 20 2023 at 11:08 UTC