Get tasks currently running?

Stream: lean4

[Thomas Murrills]

Is there a way to see what tasks are currently running? Or, even indirectly, see the number of tasks or the state of the thread pool?

The context here is #mathlib4 > slow linting step CI?, in which occasionally CI linting steps seem to continue running even after linting finishes. It's a bit of a shot in the dark, but I'm wondering if maybe some linter started a task behind the scenes which simply hasn't ended.

Also happy to hear other ideas for how to debug this or what may be going on! :)

[Henrik Böving]

Is there a way to see what tasks are currently running

Debuggers like gdb can show you what each individual thread is currently doing. "What tasks are running" is a bit of a tough question, how do you identify a task after all. But if you want to know what your system is busy with, that's going to tell you.

see the number of tasks or the state of the thread pool?

I'd say get a lean build in reldebug mode and start printing out the internal state in your debugger.

[Thomas Murrills]

Hmmm. This problem is only occasional and has only appeard in CI, in which something like that sounds infeasible(?)...but maybe I could try to reproduce it locally by just running runLinter on mathlib over and over? :grinning_face_with_smiling_eyes:

[Thomas Murrills]

Henrik Böving said:

I'd say get a lean build in reldebug mode and start printing out the internal state in your debugger.

By the way, is there documentation somewhere on how to do this? I'm not familiar with these tools but happy to learn. :)

[Henrik Böving]

but maybe I could try to reproduce it locally by just running runLinter on mathlib over and over? :grinning_face_with_smiling_eyes:

that's what we do for these bugs yes

By the way, is there documentation somewhere on how to do this? I'm not familiar with these tools but happy to learn. :)

you do a normal Lean build from source but instead of cmake --preset release you do cmake --preset reldebug

[Thomas Murrills]

Oh, that's nice and easy :) Is this Linux-only, though? ctrl+f in lean4 suggests(?) I need ubuntu-latest (but I don't really know how to read these files yet). (EDIT: aha, I was looking at what CI specifically does)

[Henrik Böving]

You should be able to build on all major platforms that we support https://github.com/leanprover/lean4/blob/master/doc/make/index.md

[Thomas Murrills]

Ok great, now I know any errors are my own. :grinning_face_with_smiling_eyes: Thanks for the pointers! :)