Syntax extensions from within the compiler

Stream: lean4 dev

[Henrik Böving]

@Siddharth Bhat and me were trying to add a syntax extension in the usual declare_syntax_cat syntax macro_rules style to the compiler in order to allow users to write LLVM IR on their own but our language server is refusing to speak with us now :(

But we are already doing stuff like this in Init right? Is there somethiign special about the Lean package that doesnn't allow us to use these extensions? And if there is, is there a nice reference we can copy from within Lean to implement our syntax extension?

[Mario Carneiro]

Syntax extensions in lean core are a bit weird because of the bootstrap

[Mario Carneiro]

If it's just an extension and not a modification it is not too bad, you first write the new syntax declarations, then update-stage0 and then write the usage code

[Mario Carneiro]

if you aren't using the syntax at all in core you shouldn't even need a bootstrap, you just add the syntax and the elaborator and then it should be usable with the stage1 compiler

[Henrik Böving]

So we just tried:

declare_syntax_cat llvm_test
syntax "foo" : llvm_test
syntax "[test|" llvm_test "]" : term

macro_rules
| `([test| foo]) => `(1)

#check [test| foo]

in a Lean 4 compiler file. Ran update-stage0 and our LSP died still. Is there something we are doing wrong?

[Sebastian Ullrich]

We avoid syntax in Lean in favor of builtin parsers, which don't have to be imported to be used. But your example seems to work for me...