[Agda] tracing & profiling

[mechvel at scico.botik.ru]

Yes, this  Debug.Trace.trace  in the Agda lib  prints what it is needed,
and is helpful.

Thank you.

--
SM


On 2020-01-20 16:12, Guillaume Allais wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda