[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