doomemacs/modules/lang/lean
Henrik Lissner 6acf163cf7
refactor!: replace smartparens with electric
BREAKING CHANGE: This moves smartparens out of core and formally
deprecates it. The package has been a performance liability and is only
being used for pair management, so the rest of its functionality was
overkill for what we needed it for.

Instead, I'm waiting for electric.el's support for N-character pairs in
Emacs 31. In the meantime, I delegate to yasnippet (later, tempel)
snippets to handle more complex pairs like /* ... */ or <?php ... ?>.

- To restore auto-pairing functionality (which is all Doom was using
  smartparens for, really), enable :emacs (electric +pair). This is not
  a perfect replacement for all of smartparens' capabilities. More
  complex pairing is being relegated to snippets (for example, /* ... */
  and <?php ... ?> comment blocks will soon have snippets for them).

- To restore the old smartparens functionality, enable :config (default
  +smartparens). Keep in mind that this is temporary! In v3, smartparens
  will be removed entirely OR moved to its own module; this hasn't been
  decided yet.

Fix: #5759
Fix: #5894
Fix: #6223
Fix: #8093
Fix: #8620
2026-02-21 17:00:48 -05:00
..
.doommodule feat: add .doommodule files 2024-09-14 20:47:39 -04:00
config.el refactor!: replace smartparens with electric 2026-02-21 17:00:48 -05:00
doctor.el docs(lean): add doctor checks 2025-12-31 20:03:00 -05:00
packages.el bump: :lang 2026-02-13 16:31:15 -05:00
README.org feat(lean): add v4 support & +v3 flag 2025-12-30 22:59:09 -05:00

:lang lean

Description   unfold

This module adds support for the Lean programming language to Doom Emacs. It supports Lean 4 by default (powered by doom-package:nael), with optional support for Lean 3 behind a doom-module:+v3 flag.

Maintainers

This module has no dedicated maintainers. Become a maintainer?

Module flags

+lsp
Enable LSP support for nael-mode (Lean 4). Requires doom-module::tools lsp and an LSP server (e.g. Lake). There no LSP support for Lean 3.
+v3
Include Lean 3 support, powered by doom-package:lean-mode.

TODO Hacks

󱌣 This module's hacks haven't been documented yet. Document them?

TODO Changelog

This module does not have a changelog yet.

TODO Installation

Enable this module in your doom! block.

󱌣 This module's prerequisites are not documented. Document them?

  • Lean 4 requires the lean4 executable (and lake if LSP support is wanted) in your $PATH.
  • Lean 3 requires the lean3 and leanpkg executables.
  • For LSP support,

TODO Usage

󱌣 This module has no usage documentation yet. Write some?

TODO Configuration

󱌣 This module has no configuration documentation yet. Write some?

Troubleshooting

There are no known problems with this module. Report one?

Frequently asked questions

This module has no FAQs yet. Ask one?

TODO Appendix

󱌣 This module has no appendix yet. Write one?