Newlines are stripped by `m!`

Stream: lean4

[Eric Wieser]

Is this deliberate behavior for docs#Lean.MessageData interpolation?

import Lean

#eval Lean.logInfo <| f!"Newline\nplease"  --ok
#eval Lean.logInfo <| Std.Format.group <| f!"Newline\nplease"  --ok

#eval Lean.logInfo <| m!"Newline\nplease"  --ok
#eval Lean.logInfo <| Lean.MessageData.group <| m!"Newline\nplease"  --no newline

[Eric Wieser]

(If you look at the generated term, m! is sneakily replacing \n with Format.line)

[Eric Wieser]

Still curious about this

[Sebastian Ullrich]

I think the replacement behavior might be older than Format understanding literal newlines. So, might be a bit too late to change now even if we think it would be reasonable

[Eric Wieser]

My impression is that MessageData.group is very rarely used, and so actually such a change would impact very few callers

[Sebastian Ullrich]

Oh it is used a ton around e.g. terms, but perhaps not so much on the level where \n is used

[Eric Wieser]

Sorry, that's what I meant; I would expect string literals containing \n to mainly appear as throwError m!"" etc