Certain blackboard font characters break syntax-checking

[caelanritter]

I have lean4-mode 1.1.2, lsp-mode 20220514.1948, flycheck 20250109.714, running on arch. The following seems to be an issue for many of the blackboard font characters (typed with \bb), although not all of them (for example, ℙ). In a fresh Lean 4 project, if I type something like example (𝕜 : Prop) : 𝕜 → 𝕜 := fun h => h or even just variable (𝕜 : Prop), I get bizarre syntax errors (e.g., in the latter case 1:19: unexpected token ')'; expected command). This usually persists until I reset the lean process (with s-l w r), or replace 𝕜 with something friendlier like k and alter the buffer "enough" to make it recheck it properly. However, it's not entirely consistent: sometimes I can delete the whole buffer and still have it throw an error.

I can disable flycheck and still get these errors, so I figure something else is responsible, but I don't know enough about what all the different minor modes do to diagnose it properly.