search

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
204 stars 39 forks source link

Annoying warning about recursion depth being exceeded #3927

Closed ehildenb closed 2 weeks ago

ehildenb commented 3 weeks ago

We've had several users ask about the importance of the recursion depth warning (including this one: https://discord.com/channels/824582698147905556/1013598994133434430/1249744367502229605). Indeed, this warning is quite verbose, and provides very little information other than "you can turn on deeper recursion".

Can it be made to happen less? Like, only report it once per simplification? Or once per context?

geo2a commented 2 weeks ago

I have spend some time figuring out how to only output the warning once, and I think we should not do it this way. The reason for my reluctance is that we would need to make the logging stateful, which will quickly become unmaintainable.

As an alternative, I propose to hide these messages by-default and allow re-enabling them with -l EquationWarnings, see the PR #3937. We could then enable this option in pyk if we run with --verbose.