Profiling?

Stream: new members

[N Gelwan]

I've got lean stuck on "busily processing...". Is there profiling? Debugging output or tracing?

[Kevin Buzzard]

Did you open the root directory of a correctly-formatted Lean 4 project using VS Code's "open folder" functionality?

[N Gelwan]

I imagine so. The issue arises after making a single change inside the file I've been working on. Otherwise everything works fine.

[N Gelwan]

Wait, are you suggesting that I open it to look for debug info?

I suspect not; there's nothing there.

[N Gelwan]

I can provide the _specific_ code that's causing the problem, but strictly speaking it's not necessary to the project, and I'd still like to figure out how to access (the interpreter's?) debugging info.

[Kevin Buzzard]

N Gelwan said:

Wait, are you suggesting that I open it to look for debug info?

I suspect not; there's nothing there.

No -- I was just checking that you weren't making a common rookie error.

[Kevin Buzzard]

Does restarting VS Code fix the problem? If not then I'm out of ideas (and hopefully someone else can comment on debugging info)

[N Gelwan]

No dice. Thanks for the shot, though.

I'll conjure up an MWE tomorrow, which we may be able to learn from even if we can't come up with a more general approach to debugging.

[Sebastian Ullrich]

We'd need more information to comment on debugging. Is it only hover etc. that's stuck or the orange bar as well? Does it terminate eventually?

[N Gelwan]

Orange bar stuck, too. Afaict doesn't terminate.

[Mario Carneiro]

What are the imports of the file?

[Mario Carneiro]

If it is a command that you wrote that causes the nontermination, what is the command?

[Mario Carneiro]

there are several different kinds of profiling tools but which one to use depends on the context

[Sebastian Ullrich]

Perpetually stuck is a bit problematic because then our in-Lean debugging tools won't print output. If you're comfortable with gdb or similar, attaching it and dumping stacktraces can provide some initial information.