parsing issue with `interpolatedStr`

Stream: lean4

[Alexander Bentkamp]

The interpolatedStr parser does not seem to like a many parser coming directly before it:

import Lean

open Lean
open Parser

elab "Foo1" msg:interpolatedStr(term) : tactic => do
  pure ()

example : False := by
  Foo1 "\{" -- works!
  sorry

elab "Foo2" "!"* msg:interpolatedStr(term) : tactic => do
  pure ()

example : False := by
  Foo2 "\{" -- invalid escape sequence
  sorry

Is there any way to get around this? And what is causing this?

[Sebastian Ullrich]

Oh, that is an interesting issue. There is a common token parser that most parsers are based on, but interpolatedStr is not. So "!" tries to use this common token parser and check if the result is the token !, but the token parser fails because the input is not a valid (non-interpolated) string literal. And because the failure is not on the first character, we don't backtrack (I believe I changed this at some point because without it we get worse error messages at other points).

[Sebastian Ullrich]

The simplest fix on Lean's side would probably be to finally implement lean4#407

[Sebastian Ullrich]

It looks a bit weird, but atomic("!")* fixes this as well

[Alexander Bentkamp]

I am not worried that atomic looks weird. I am very happy that it works! Thanks :smile: