[Agda] debugPrint : Does it work correctly?

[Ulf Norell]

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/9ff3310f27a006675656d453d3338d
> f233e4ca78/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/1d426353/attachment.html>