Stream: Ltac2

Topic: How can I control the depth of "Message.of_constr"?


view this post on Zulip Michael Soegtrop (Mar 21 2021 at 17:43):

@Pierre-Marie Pédrot : from a certain depth on, I get ellipses in the output of "Message.of_constr". I tried to change "Set Printing Depth", but this doesn't seem to have an effect. Is there a way to get a complete constr output from "Message.of_constr"?

view this post on Zulip Michael Soegtrop (Mar 21 2021 at 18:26):

It might be a CoqIDE issue - checking ...

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2021 at 19:46):

No, AFAIK it's a limitation of the printing engine. You'd have the same issue with the vanilla Print command.

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2021 at 19:47):

I think I remember there was an open issue about this.

view this post on Zulip Michael Soegtrop (Mar 21 2021 at 19:59):

With coqc (instead of CoqIDE) I can control the output with "Set Printing Depth". See also (https://github.com/coq/coq/pull/13972). But of cause it could be that with Ltac2 there are additional issues. It is hard to imagine that the output of Message.of_constr can somehow be manipulated by the IDE as Emilio described in the PR. But then I learned not to underestimate what is possible since I work with Coq ;-)


Last updated: Jan 31 2023 at 11:01 UTC