[Agda] tracing & profiling
mechvel at scico.botik.ru
mechvel at scico.botik.ru
Mon Jan 20 12:13:47 CET 2020
Dear Agda developers,
I have a complex program written in Agda, and have difficulties in
finding
which function takes the most of the run-time cost.
For n = 16 it evaluates fast and correct. For n = 17 is hangs for more
than hour,
and I interrupt it.
The "same" algorithm in Haskell evaluates fast for all n.
In Glasgow Haskell, I sometimes used tracing, and sometimes used
profiling with
setting cost centers. These two really helped a lot.
In Agda, I currently make various versions for the program that return
the list of
the computation _states_, with printing out the first n states.
This needs effort in changing signatures, and leads to some other
complications.
Probably tracing and/or profiling is not the main current feature
(problem) for Agda
to design, but is something of this sort already possible?
Thanks,
------
Sergei
More information about the Agda
mailing list