MessageData without context

Stream: general

[Joachim Breitner]

Kim Morrison said:

Shall I change this to:

I would have expected this to help, but it seems that my understanding of MetaM and MessageData is still incomplete.

[llllvvuu]

Joachim Breitner said:

Kim Morrison said:

Shall I change this to:

I would have expected this to help, but it seems that my understanding of MetaM and MessageData is still incomplete.

You were right about addMessageContextFull working here, just needed to be put in another place as well (Batteries has a linter frontend that wraps every warning, so even though the warning itself has content, the wrapper text didn't have context. The wrapper stuff is in CoreM so I added addMessageContextPartial in batteries#838 and that worked)

[Joachim Breitner]

I wish these two functions had docstrings and maybe better names (addLocalMessageContext and addGlobalMessageContext?).

Would you consider batteries#838 a proper fix, or a work-around for a bug in lean?

[Joachim Breitner]

Probably we want both: The fix in the linter, so that there is a context (so that hovers can work), but also the fix in lean to have degrade gracefully if someone did not set a context. Or is it better to fail badly so that developers fix their MessageData?

[llllvvuu]

Or is it better to fail badly so that developers fix their MessageData?

I commented this in #4433 as well, but either judgment call seems fine. If the documentation and error messages align towards this being a requirement to use the API, then as a user I'd be happy to accommodate as I did in batteries#838. Particularly "(invalid MessageData.lazy, missing context)" could prescribe some courses of actions, although that's a bit tricky as we just saw.

[Joachim Breitner]

Is my theory true that without the batteries fix (and only the lean fix), the message would appear, but the names would not be hoverable?

[llllvvuu]

It's a bit tricky to test this since there is no missing context issue in #lint, but only in lake exe runLinter. So I guess there may be some code path in #lint that is adding context that is missing from the runLinter CLI.

[llllvvuu]

Hmm I guess I could simulate this by wrapping the relevant Exprs in toString

[Joachim Breitner]

Or maybe it’s the difference between MessageData.format and MessageData.msgToInteractiveAux.

[Joachim Breitner]

It might be good to understand the issue fully, and document the results

[llllvvuu]

doing pure m!"#check {toString (← mkConstWithLevelParams declName)} /- {warning} -/" instead of pure m!"#check {← mkConstWithLevelParams declName} /- {warning} -/" in batteries does seem to remove the hover

[llllvvuu]

Joachim Breitner said:

Or maybe it’s the difference between MessageData.format and MessageData.msgToInteractiveAux.

Ah, I think you're right. The runLinter CLI does: IO.print (← fmtResults.toString) whereas #lint (good) does logError fmtResults and if I change that to logError (← fmtResults.toString) then it's bad

[Joachim Breitner]

Is fmtResults here a MessageData with a context node? If so, maybe we can fix MessageData.format.

[llllvvuu]

It is MessageData interpolated of two things: m!"#check {← mkConstWithLevelParams declName} /- {warning} -/". In this case, {warning} does have context from addMessageContextFull, but {← mkConstWithLevelParams declName} does not have context.

It looks like logAt does inject context, but toString does not. I think the real fix for batteries would be to put addMessageContext in front of the IO.print instead of where I put it.

[Joachim Breitner]

Exactly; if you are going to pass a MessageData to IO, you have to use addMessageContextPartial while you still can, i.e. with access to the environment and options.

[Joachim Breitner]

Just checking if we are not deadlocked: are you still investigating something about this? When and if you are done and have a concrete course of action, please drop a short note here or at the lean4 PR.

[Joachim Breitner]

Ah, and maybe add docstrings explaining this to the message data type and the addMessageContext functions: that a MessageData value makes most sense within context, and when taking it out of context (e.g. leaving MetaM), the context ought to be added to it. So hopefully the next person debugging this has an easier time :-)

[llllvvuu]

I'm all set on my end. Up to you whether no context should degrade vs error. I've added the documentation so that it's navigable either way.

[Joachim Breitner]

Sent to the merge queue. Thanks for bearing with me here!