debugging

Stream: general

[Kenny Lau]

What are the debugging tools available for seeing what operation costs the most time? profiler only works for tactics (and the total time), and the length of trace.class_instances isn't really positively related to time

[Kenny Lau]

What are the debugging tools in general?

[Kenny Lau]

or is it correct to think that if those tools existed, we would have figured out the cause of the long elaboration time of polynomials?

[Mario Carneiro]

I think you are already familiar with all the timing tools lean has built in. If you want more you will have to build it yourself

[Kenny Lau]

so the two tools are all there is?

[Mario Carneiro]

there is also timeit but that's mostly for tactic programming and evaluating pure functions

[Koundinya Vajjha]

I found a few but I never used them.
- Check out #unify, declare_trace, #help. More commands in this file.
- Simple CLI tool for debugging tactics/programs: cli.lean
- Debugger/Monitor test file : basic_monitor.lean