[Agda] debugPrint : Does it work correctly?

[Apostolis Xekoukoulotakis]

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/20180306/065b3b12/attachment.html>