<div dir="ltr"><div><div>It works if you put an option on the file itself.<br><br></div>I was changing the "Agda2 Program Args" from emacs.<br><br></div><div>I have "-v test:20"<br></div><div>and  "--caching"<br><br></div><div>With your example without  the Options pragma, I do not get any output.<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Mar 6, 2018 at 10:45 PM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>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.<br><br></div><div>For instance, this works as expected for me (prints DEBUG in the *Agda debug* buffer):<br><br></div><div>{-# OPTIONS -v test:20 #-}<br><br>open import Agda.Builtin.Reflection<br>open import Agda.Builtin.Unit<br>open import Agda.Builtin.String<br>open import Agda.Builtin.Nat<br>open import Agda.Builtin.List<br><br>macro<br>  foo : Term → TC ⊤<br>  foo _ = debugPrint "test.debug" 10 (strErr "DEBUG" ∷ [])<br><br>A : Set<br>A = foo<br><br></div><div>Changing the verbosity level to below 10 (or to a different label like test.foo) makes it not print anything.<br></div><div><br></div>/ Ulf<br></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">On Tue, Mar 6, 2018 at 8:36 PM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@<wbr>gmail.com</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div dir="ltr"><div><div><div><div>I do know how verbosity levels work.<br><br></div>According to <br><a href="https://github.com/agda/agda/blob/9ff3310f27a006675656d453d3338df233e4ca78/CHANGELOG.md#reflection" target="_blank">https://github.com/agda/agda/b<wbr>lob/9ff3310f27a006675656d453d3<wbr>338df233e4ca78/CHANGELOG.md#re<wbr>flection</a><br><br></div>the String at debugPrint seems to act like a filter.<br><br></div>I have tested it with multiple values and it does not seem to filter the logs at the *Agda debug* buffer.<br><br></div>Am I misinterpreting something?<br><br><br></div>
<br></div></div>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>