antiquot bug

Stream: lean4

[Arthur Paulino]

I just found this bug on leanprover/lean4:nightly-2022-04-26:

If you paste the following code:

syntax "foo " (" bar " ident)? : tactic

macro_rules
  | `(tactic| foo $[bar $id]) => sorry

It fails, as expected. But then if you type in the exclamation mark by hand:

syntax "foo " (" bar " ident)? : tactic

macro_rules
  | `(tactic| foo $[bar $id]?) => sorry

It fails again with the same error, but this failure is unexpected.
Then if you erase id and type it out again - or if you just edit it in any way, leaving at least a valid name for the ident syntax reference - it suddenly works

[Arthur Paulino]

The error message is

elaboration function for 'antiquot' has not been implemented

And from a working state, you can erase the exclamation mark and type it out again to trigger the error

[Arthur Paulino]

I named this thread antiquot bug but I don't really know if this is an appropriate name

[Sebastian Ullrich]

Yes, it's a bad interaction between the antiquotation syntax and the language server

[Arthur Paulino]

Not sure if this is relevant, but I'm using the lean4 extension version v0.0.71

[Sebastian Ullrich]

Should be fixed with https://github.com/leanprover/lean4/tree/829c81d67751b837bb292ae6e7999c4cb7488106/