[Agda-dev] Debugging non-TCM code

[Jesper Cockx]

>
> This works fine for TCM, but not for ReduceM, which is why we currently
> use traceSLn (which uses the 'around' style) instead of printSLn for
> debugging ReduceM code.


After a bit of experimenting, it seems that the 'in between' style *does*
work for ReduceM as well as for the TCM: I can replace all uses of
traceSDoc (in the 'around' style) with traceSDocM (in the 'in between'
style) and still get all debug messages in the right order, though I don't
really understand why. But then the question becomes: why are we currently
using the (more awkward) 'around' style for debugging for ReduceM?

Anyway, I'll create a pull request with my experimental changes, so the
ones who want can test if it preserves their debugging output.

-- Jesper

On Thu, Jul 13, 2017 at 3:13 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> Hi Andreas,
>
> Thanks for the answer, looking at the benchmarking code certainly helped.
> However, I'm not sure yet if your solution can be adapted to debugging. One
> difference between benchmarking and debugging is the style in which they're
> commonly used: benchmarking is put 'around' a piece of code, while
> debugging is usually put 'between' two pieces of code:
>
> x <- billTo account $ action
>
> vs
>
> x <- action1
> printSLn $ "debugging:" ++ show x
> action2 x
>
> In the case of billTo, this works because billTo uses strictness to ensure
> internally that the benchmarking data is logged at the right time. However,
> in the case of printSLn we are dependent on the strictness/lazyness of the
> ambient monad to print the debug messages in the right order (or even print
> them at all). This works fine for TCM, but not for ReduceM, which is why we
> currently use traceSLn (which uses the 'around' style) instead of printSLn
> for debugging ReduceM code. So either we have to use `seq` and similar
> functions to force debug statements to be evaluated at the right point, or
> we have to switch to the 'around' style for all debugging outside of the
> TCM.
>
> Another problem is that we often use reportSDoc instead of reportSLn,
> which takes a TCM Doc instead of a String, in order to enable
> pretty-printing etc. To show this TCM Doc, we need access to the TCEnv and
> the TCState, as well as IO. We can fake IO with unsafePerformIO, but this
> doesn't yet give us access to TCEnv and TCState. I see three possible ways
> around this:
>
> 1. Either we need to add constraints MonadReader TCEnv and ReadTCState to
> all code that uses debugging
> 2. Or we need to have global IORefs for the TCEnv and TCState
> 3. Or we need to limit the debugging we can do outside of the TCM to just
> strings/simple show
>
> Option 2 seems scary to me, so I think the best solution would be a
> combination of 1 and 3 where we can do simple String debugging in pure code
> and do more fancy debugging when we have read-access to TCEnv and TCState
> (such as in ReduceM). But if you have an idea how we can do better then I'd
> love to hear it.
>
> Using a global IORef for the InteractionOutputCallback seems like a good
> idea, because that way we can get debugging output from the ReduceM in
> Emacs instead of only at the command-line as we do currently. But this
> seems largely unrelated to the rest of the problems.
>
> -- Jesper
>
>
> On Wed, Jul 12, 2017 at 7:52 PM, Andreas Abel <abela at chalmers.se> wrote:
>
>> Dear Jesper,
>>
>> I have thought about this problem before, but never implemented the
>> solution.  It is similar to benchmarking non-TCM code.
>>
>>   Agda.Utils.Benchmark
>>
>> There is a monad
>>
>>   MonadBench
>>
>> that lets us access benchmark-related information.
>>
>>   Agda.Benchmarking
>>
>> This stores the benchmarkint-related information in an IORef and
>> implements MonadBench accordingly.
>> It provides recording of benchmarking data in pure code using
>> unsafePerformIO.
>>
>>   Agda.TypeChecking.Monad.Benchmark
>>
>> This implements benchmarking in the TCM, in particular, to communicate
>> with the IORef.
>>
>> I think I now remember what stopped me from doing it for debugging as
>> well.  The debug printing in interaction mode goes into the emacs buffer:
>>
>>   displayDebugMessage n s = liftTCM $
>>     appInteractionOutputCallback (Resp_RunningInfo n s)
>>
>> See Agda.Interaction.Response
>>
>>   type InteractionOutputCallback = Response -> TCM ()
>>
>> The emacs mode does
>>
>>     setInteractionOutputCallback $
>>         liftIO . mapM_ print <=< lispifyResponse
>>
>> It feels like somehow this could be refactored to happen in the IO
>> instead of the TCM, using tricks with IORefs and unsafePerformIO.
>>
>> It would be great if you got this to work, having debug info in
>> functional or ReduceM code would be a major improvement for the development
>> process.
>>
>> Best,
>> Andreas
>>
>>
>> On 12.07.2017 18:11, Jesper Cockx wrote:
>>
>>> Dear Agda developers,
>>>
>>> I'm working on fixing some of the current issues with --rewriting (#2433
>>> and #2573) but I'm running into a bit of a problem. For my fix, I needed to
>>> generalize some functions from TCM to an arbitrary monad satisfying some
>>> constraints, so they can also be used in ReduceM. Specifically, I have made
>>> the following changes to the type signatures:
>>>
>>> -getModuleParameterSub :: MonadTCM tcm => ModuleName -> tcm Substitution
>>> +getModuleParameterSub :: (Functor m, ReadTCState m) => ModuleName -> m
>>> Substitution
>>>
>>> -freeVarsToApply :: QName -> TCM Args
>>> +freeVarsToApply :: (Functor m, HasConstInfo m, ReadTCState m,
>>> MonadReader TCEnv m) => QName -> m Args
>>>
>>> -moduleParamsToApply :: ModuleName -> TCM Args
>>> +moduleParamsToApply :: (Functor m, Applicative m, MonadReader TCEnv m,
>>> ReadTCState m)
>>> +                    => ModuleName -> m Args
>>>
>>> However, this means these functions can no longer contain any debug
>>> statements. For TCM we have reportSDoc and for ReduceM we have traceSDoc,
>>> but these cannot be joined into one typeclass since they have different
>>> calling conventions (traceSDoc takes a continuation as an additional
>>> argument). So I'm at a loss at how to debug my code. There are also other
>>> occasions where you're neither in TCM nor in ReduceM but you still want to
>>> add some debug statements, but this seems to be impossible with the current
>>> infrastructure.
>>>
>>> Does anyone have an idea how to get out of this dilemma?
>>>
>>> -- Jesper
>>>
>>>
>>> _______________________________________________
>>> Agda-dev mailing list
>>> Agda-dev at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda-dev
>>>
>>>
>> --
>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>
>> Department of Computer Science and Engineering
>> Chalmers and Gothenburg University, Sweden
>>
>> andreas.abel at gu.se
>> http://www.cse.chalmers.se/~abela/
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20170713/5b0636e8/attachment-0001.html>