Thomas Lamiaux (May 22 2024 at 18:11): 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
Thomas Lamiaux (May 22 2024 at 18:11):Would there be a way to do that ?
Gaëtan Gilbert (May 22 2024 at 18:14):https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#coq:cmd.Redirect ?
Notification Bot (May 22 2024 at 18:24):Thomas Lamiaux has marked this topic as resolved.
Notification Bot (May 22 2024 at 18:34):Thomas Lamiaux has marked this topic as unresolved.
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
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
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: Oct 13 2024 at 01:02 UTC