Create a CodeMirror language plugin for Lean

Programming Lean
1

Hi,

I’d like to request the creation of a codemirror-lang-lean repository for the Lean track.

Currently, the Lean track uses Haskell as a fallback for syntax highlighting in the online editor. While Haskell is a reasonable approximation, it doesn’t cover Lean-specific keywords
like theorem, lemma, sorry, #check, #eval, inductive, structure, namespace, tactic, where, etc.

There is no existing CodeMirror 6 plugin for Lean — neither official nor community-maintained.

I’d be happy to implement the grammar once the repo is set up.

Related issue: Create a CodeMirror mode for Lean · Issue #156 · exercism/lean · GitHub

Thanks!

2

Hi there

You can create the correct infra on your own account if you want and then we can later set-up the repo on the exercism end which can be filled by changing the git origin. The founder of exercism is really busy at the moment, so I recommend not waiting and “just” doing the work.