Stream: Coq users

Topic: trace/print during runtime?


view this post on Zulip Sam Stites (Jun 02 2021 at 00:53):

Probably a silly question, but I was wondering if it would be possible to print an expression at runtime, similar to Haskell's trace function.

view this post on Zulip Li-yao (Jun 02 2021 at 12:11):

This package reduction-effects might fit the bill: https://github.com/coq-community/reduction-effects

view this post on Zulip Sam Stites (Jun 02 2021 at 13:55):

this looks right, but doesn't work for me : / I guess the project I am working in is non-trivial enough that it sidesteps something from this library.

view this post on Zulip Li-yao (Jun 02 2021 at 14:21):

It might be worth submitting a bug report if you can somehow minimize it.

view this post on Zulip Yannick Forster (Jun 03 2021 at 07:24):

Can you elaborate a bit more what doesn't work? I remember that I had the problem that just nothing happened as well at some point, but either I moved the From ReductionEffect Require Import PrintingEffect. around or I put Declare ML Module "redeffect_plugin". in the file where I wanted to use the effects. One of those fixed the problem for me, although I didn't understand why


Last updated: Jan 27 2023 at 00:03 UTC