Stream: Elpi users & devs

Topic: coq.say but silent on make

view this post on Zulip Cyril Cohen (Jan 17 2024 at 16:00):

How to display messages like the one Coq outputs when we manually enter a definition, inductive etc (e.g. "foo is declared...") but that are not displayed while using coqc in compilation mode? Is there a flag? Another predicate than coq.say? (I tried coq.info and coq.notice, which I do not know what they correspond to wrt coq.say, but neither worked)

view this post on Zulip Davide F (Jan 17 2024 at 20:17):

I think that this possibility is not available in the current version of coq-elpi. Enrico will surely correct me if I'm wrong.
If you add this in the builtins:

MLCode(Pred("coq.say-quiet",
    VariadicIn(unit_ctx, !> B.any, "Prints a notice message if not silenced"),
    coq_print pp (Flags.if_verbose Feedback.msg_info)), (* Flags.if_verbose seems to be the key*)
  DocAbove);

and call coq.say-quiet somewhere in your code, does it do what you need?

view this post on Zulip Enrico Tassi (Jan 17 2024 at 22:52):

Hum, I guess we might add a @if-interactive! => coq.say "bla" that controls the Flags.if_verbose thing.... not 100% sure

Last updated: Oct 13 2024 at 01:02 UTC