Order of checks in CI

Stream: new members

[Stuart Presnell]

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]

In principle the docstring could have been added in minute 100

[Eric Wieser]

With add_decl_doc

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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]

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]

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

[Eric Wieser]

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]

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]

PRs welcome :upside_down:

[Reid Barton]

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

[Stuart Presnell]

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]

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

[Damiano Testa]

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]

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]

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]

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]

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]

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!