Stream: MetaCoq

Topic: tmPrint in a file ?


view this post on Zulip Thomas Lamiaux (May 22 2024 at 18:11):

Hi, I am generating a bunch of terms and printing them with tmPrint to debug my functions.
The term is printed in info, but it is a bit annoying to view as my terms are big, so I would like to print them in a file. For instance, sth like:
`MetaCoq Run (test <% nat %>). >> test_nat

view this post on Zulip Thomas Lamiaux (May 22 2024 at 18:11):

Would there be a way to do that ?

view this post on Zulip Gaëtan Gilbert (May 22 2024 at 18:14):

https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#coq:cmd.Redirect ?

view this post on Zulip Notification Bot (May 22 2024 at 18:24):

Thomas Lamiaux has marked this topic as resolved.

view this post on Zulip Notification Bot (May 22 2024 at 18:34):

Thomas Lamiaux has marked this topic as unresolved.

view this post on Zulip Thomas Lamiaux (May 22 2024 at 18:35):

Is it possible to inline Require somehow ? During the execution of my functions, I am printing different stuffs, and I would like to print them in different files

view this post on Zulip Yannick Forster (May 22 2024 at 18:37):

Probably we could have a TemplateMonad command for Redirect? Otherwise, I have no better idea than postprocessing files, which should also be kind of straightforward

view this post on Zulip Thomas Lamiaux (May 22 2024 at 19:05):

Is it normal that Redirect only does something when I run make but not in the interactif mode ?


Last updated: Jul 23 2024 at 20:01 UTC