[Agda] tracing & profiling

[Guillaume Allais]

Hi Sergei,

If by tracing you mean using `Debug.Trace` then we do have such facilities
in the standard library: https://agda.github.io/agda-stdlib/Debug.Trace.html
Thanks to the rewrite rules, it will not change the compile time behaviour
of your program.

We also have a quick tutorial of the feature in the README:
https://agda.github.io/agda-stdlib/README.Debug.Trace.html

Cheers,
--
gallais

On 20/01/2020 11:13, mechvel at scico.botik.ru wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda