[Agda] debugPrint : Does it work correctly?

[Ulf Norell]

You need to get rid of the space after -v or put test:20 on its own line.
Each line in the Agda2 Program Args is treated as a single argument
so what you have is equivalent to the command-line

  agda --caching "-v test:20"

This is actually still a valid option and gets parsed as setting the
verbosity
level for the label " test" (with a leading space). You can verify this by
adding a space also in the argument to debugPrint.

/ Ulf

On Tue, Mar 6, 2018 at 10:15 PM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> It works if you put an option on the file itself.
>
> I was changing the "Agda2 Program Args" from emacs.
>
> I have "-v test:20"
> and  "--caching"
>
> With your example without  the Options pragma, I do not get any output.
>
> On Tue, Mar 6, 2018 at 10:45 PM, Ulf Norell <ulf.norell at gmail.com> wrote:
>
>> What values did you try? Setting the option `-v X.Y.Z:N` (in an OPTIONS
>> pragma for instance) should enable any debugPrints with arguments "X.Y.Z*"
>> M with M =< N.
>>
>> For instance, this works as expected for me (prints DEBUG in the *Agda
>> debug* buffer):
>>
>> {-# OPTIONS -v test:20 #-}
>>
>> open import Agda.Builtin.Reflection
>> open import Agda.Builtin.Unit
>> open import Agda.Builtin.String
>> open import Agda.Builtin.Nat
>> open import Agda.Builtin.List
>>
>> macro
>>   foo : Term → TC ⊤
>>   foo _ = debugPrint "test.debug" 10 (strErr "DEBUG" ∷ [])
>>
>> A : Set
>> A = foo
>>
>> Changing the verbosity level to below 10 (or to a different label like
>> test.foo) makes it not print anything.
>>
>> / Ulf
>>
>> On Tue, Mar 6, 2018 at 8:36 PM, Apostolis Xekoukoulotakis <
>> apostolis.xekoukoulotakis at gmail.com> wrote:
>>
>>> I do know how verbosity levels work.
>>>
>>> According to
>>> https://github.com/agda/agda/blob/9ff3310f27a006675656d453d3
>>> 338df233e4ca78/CHANGELOG.md#reflection
>>>
>>> the String at debugPrint seems to act like a filter.
>>>
>>> I have tested it with multiple values and it does not seem to filter the
>>> logs at the *Agda debug* buffer.
>>>
>>> Am I misinterpreting something?
>>>
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180307/f21921dd/attachment.html>