reduce decls Debug noise

[shua]

Decls debug rendering is a bit noisy, especially since decls does not change, but is printed for every step that failed. With this change, decls is only printed in the prove judgement, with the expectation that this is the main entrypoint for proofs.

[FullyNonlinear]

In my personal opinion, I prefer the original output format. The major benefit of the original format is that I can easily definitively map each field output to the name of the field without further knowledge of how each field is displayed, thanks to the list of field outputs having a fixed length on the top level.

That being said, I don't have a problem with skipping fields that are empty containers, as long as the name of the fields that are non-empty get displayed in the output.

In addition, if the verbosity of the debug output of decls is annoying enough, positioning it at the end of the line after any other useful information could also be another solution. (I understand that decls usually doesn't change across the lines. )

[shua]

Can you give me an example of an issue you had where it was helpful to see specifically which field in Decls the item was in?

[FullyNonlinear]

Can you give me an example of an issue you had where it was helpful to see specifically which field in Decls the item was in?

Here is one example that immediately comes to my mind:

test test::coherence_orphan::CoreTraitLocal_for_AliasToKnown_in_Foo ... ok
prove goal={}, assumptions={}, env=Env { variables: [], bias: Soundness }, decls=decls(222, [trait Foo <ty> ], [impl <ty> Foo(^ty0_0) where {Foo(^ty0_0)}], [impl ! Foo(u32)], [], [], [], {Foo}, {})

In this example, there are two fields that both start with the prefix impl, namely impl_decls and neg_impl_decls. For someone who knows well how to parse the new output format already, they would know to look ahead further to figure out which is the usual impl_decls and which is the neg_impl_decls. (I actually didn't know that until I mapped the output to the fields under the current format.) For beginners who do not have that information, it would be hard for them to know definitively which subsequences belong to which field. (Again, this is just my personal experience and opinion :blush: )

[shua]

That's fair, so with this PR the output would look like

decls[ trait Foo <ty>, impl <ty> Foo(^ty0_0) where {Foo(^ty_0)}, impl ! Foo(u32) ]

and you're issue was that it wasn't clear you needed to call eg decls.neg_impl_decls(foo_trait_id) to get that value? That makes sense, I was coming from "why did my proof fail?" but not I hadn't really thought of it from the point of view of a dev needing to add a lookup of some id and not sure which field to use.

I'll try a slightly more verbose output, thanks for the feedback.

[lcnr]

as a general question: should we mention the decls at all in the proof trace?

I am not that happy about using .. for empty fields but also don't like the current impl without field names too much. Ideally we could just avoid that entirely :3

[shua]

@lcnr the decls should only have to be output once in the trace of a proof, because they shouldn't change. So I guess we could just print them in some top-level function like prove_goal and don't print them anywhere else?

[lcnr]

@lcnr the decls should only have to be output once in the trace of a proof, because they shouldn't change. So I guess we could just print them in some top-level function like prove_goal and don't print them anywhere else?

yeah, exactly :+1: