@gebner, this seems to have broken many uses of have. (e.g. https://github.com/leanprover-community/lean3port/blob/fc17055f3535e176358f651af1eefb5f6ede0f84/Leanbin/Init/Data/Fin/Ops.lean, but many others.) Note here ty is an optional node, and so $ty:term isn't working.

Mario's original code is a bit "low-level" using mkNode directly, but perhaps we should either revert to it, or switch to something that actually cases on whether h and ty are present. I'm happy to try sorting this out, but wanted to ask first what your motivation for making the change was.

Note here ty is an optional node, and so $ty:term isn't working.

Ah, this is what's happening here! The proper fix is to turn ty (and h!) into Option Syntax:

@[trTactic «have»] def trHave : TacM Syntax := do
  let h := (← parse (ident)?).map mkIdent
  let ty ← (← parse (tk ":" *> pExpr)?).mapM (trExpr ·)
  match ← parse (tk ":=" *> pExpr)? with
  | some pr => `(tactic| have $[$h:ident]? $[: $ty:term]? := $(← trExpr pr))
  | none => `(tactic| have $[$h:ident]? $[: $ty:term]?)

but wanted to ask first what your motivation for making the change was.

Manually constructing syntax trees is verbose and error-prone. You're also chasing a moving target: changing the syntax definition in seemingly "backwards-compatible" ways (e.g. by making some parts optional, etc.) changes the tree representation and breaks old manually constructed trees without any warning. I changed some syntax definitions in mathlib4 so I thought it was about time to upgrade the construction in mathport.

Mario expressed the same sentiment in leanprover-community/mathlib4#80 (comment):

Yes, of course I use [syntax quotations] whenever I can, but unfortunately I quite often ran into the limitations of syntax quotation. Every single use of mkNode et al instead of `(foo) in mathport (probably around 50% of uses) is necessary, and probably a good starting point for finding future improvements of the notation.

(Of course I took his comment as a challenge...)

Note that using `(foo) is also error prone, in a different way. I pretty much have to double check the generated term every time because Syntax isn't strongly typed and type errors are common (like this very example).

I would rather have syntax changes break the build rather than silently change the output of compilation, because pretty much any syntax change requires review here. In this case we have two almost-overlapping syntax constructors, and it is important that lean picks the right one in each case and does not introduce a choice node. "Backward compatible" syntax changes can absolutely break this code, even if you use `(foo) notation.

I've sent this off to CI as #61.