[Agda] debugPrint : Does it work correctly?

[Apostolis Xekoukoulotakis]

I do know how verbosity levels work.

According to
https://github.com/agda/agda/blob/9ff3310f27a006675656d453d3338df233e4ca78/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?

[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 <

Post by Apostolis Xekoukoulotakis
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
https://lists.chalmers.se/mailman/listinfo/agda

[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.

Post by 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
{-# 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 <

Post by Apostolis Xekoukoulotakis
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
https://lists.chalmers.se/mailman/listinfo/agda

[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 <

Post by 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.

Post by 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
{-# 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 <

Post by Apostolis Xekoukoulotakis
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
https://lists.chalmers.se/mailman/listinfo/agda