Syntax: Lean

Guideline Criteria: N/A (already added)

Lean is an interactive theorem prover.
The current syntax was added in #1446 four years ago (2021-03-01, v0.18.0):

Lean.sublime-syntax has been added manually from https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json via conversion.

bat/doc/assets.md

Line 105 in b7f9662

* `Lean.sublime-syntax` has been added manually from https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json via conversion.

https://github.com/leanprover/vscode-lean was for Lean 3, and the repo was archived a month ago (2025-04-02). It is succeeded by https://github.com/leanprover/vscode-lean4.

Could we update Lean 3 to Lean 4? Is a PR welcome?

Further details

The existing Lean 3 .sublime-syntax also works reasonably well for Lean 4. (I've used it successfully for months through typst.)

There's only one known edge case: f'x', where 'x' is incorrectly parsed as a string.

-- Apostrophes are allowed in variable names
variable (f'x' : ℕ)

-- But somehow, Klingon variables are parsed correctly…
variable (bangwI' jablu'DI' QaQqu' nay' Ghay'cha' he' : ℕ)

Links

• Significant Changes from Lean 3 - Lean 4 Doc
  • Replace some , with =>
  • Add the fun+match notation
  • Replace begin … end with by …
  • Unify the two keywords variables and variable as variable
  • Change the syntax of the tactic combinators like <;>
  • …
• Lean 4 survival guide for Lean 3 users · leanprover-community/mathlib4 Wiki
• Syntax Highlighting Lean in LaTeX — Lean
• #general > Status of Lean 3? - Lean - Zulip
• #general > License of Mathematics in Lean? - Lean - Zulip
• Add support for Lean 4 github-linguist/linguist#6616
• Commits history
  • https://github.com/leanprover/vscode-lean/commits/master/syntaxes/lean.json
  • https://github.com/leanprover/vscode-lean4/commits/8835d118a538d7a5c705a748f53e35612f351c9d/syntaxes/lean.json
  • leanprover/vscode-lean4@ca65431 moves lean.json to lean4.json
  • https://github.com/leanprover/vscode-lean4/commits/master/vscode-lean4/syntaxes/lean4.json

Additional info

Directly conversion will raise the following error.

Traceback (most recent call last):
  File "…\sublime_text_build_4200_x64\Lib\python38\sublime_plugin.py", line 1601, in run_
    return self.run()
  File "…\sublime_text_build_4200_x64\Packages\Default.sublime-package\convert_syntax.py", line 433, in run
  File "…\sublime_text_build_4200_x64\Packages\Default.sublime-package\convert_syntax.py", line 358, in convert
  File "…\sublime_text_build_4200_x64\Packages\Default.sublime-package\convert_syntax.py", line 312, in make_context
Exception: no entry in repository for stringBlock

Fixed in leanprover/vscode-lean4#623.