[Agda-dev] Debugging non-TCM code

[Jesper Cockx]

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/a5ef74c8/attachment.html>