indentation

Stream: Emacs

[Clément Blaudeau]

Hi everyone, I'm new to lean. I installed the latest version of lean (Lean (version 4.20.0, x86_64-unknown-linux-gnu, commit b02228b03f65, Release), and setup lean4-mode as described in the installation instruction. I use lean with lsp-mode. Most things work well (type annotations, errors, etc.), but the indentation is broken. M-x indent-region simply removes all space from the beginning of the lines. Is it normal (i.e. unsupported) or a problem in my configuration ?
Thank you for your help, and sorry if it is already answered somewhere

[Malvin Gattinger]

Not sure if we even have automatic indentation in vs code :thinking:

[Julian Berman]

This is what I implemented for lean.nvim for autoindent in case it's helpful for reference, with test cases here.

It seems to work pretty well (in the sense that no one has complained to me about it!)

[Clément Blaudeau]

Malvin Gattinger said:

Not sure if we even have automatic indentation in vs code :thinking:

When you hit enter at the end of a line, what happens ? does the next line starts always start at column 0 ? You do all the indentation manually ?

[Malvin Gattinger]

Ah, no, in VS code I think it usually stays in the same indentation level as the line you were on before hitting enter. But besides that there is no "smart" indentation function I think, so nothing like what Mx indent-region does for me in a $\LaTeX$ document for example.

[Lua Viana Reis]

Do you have haskell-mode installed? You can try using haskell-indent-mode, which is a minor mode (I'm not sure if it conflicts with lean4-indent.el, though :/ )

[Clément Blaudeau]

haskell-indent-mode does not help (neither electric-indent-mode), each newline is still thrown at column 0... Could someone share a minimal emacs config where the indentation is, at least, the same as the previous line ? It has been the main roadblock for trying Lean so far for me

[Clément Blaudeau]

More investigation revealed that all the indent infrastructure is there in the lean4-mode (in lean4-eri.el), so the problem is more of getting it activated properly...

[Abdullah Uyu]

I am using doom emacs. For me, "gg=G" (or C-x h M-x indent-region) just flattens all the buffer, no indentation at all. but when "o" (or RET), it continues from the indentation of the line RET is pressed. Thus, second RET continues at column 0, for example. I think this is very open to enhance.

For example, I always keep pressing SPC two times after going to new line from a line starting with dot. Here, see the demo:
2025-07-05 11-29-47.mkv

[Abdullah Uyu]

I think for a line starting with a dot, the default indentation for the second line should be +2.

[George McNinch]

Clément Blaudeau said:

More investigation revealed that all the indent infrastructure is there in the lean4-mode (in lean4-eri.el), so the problem is more of getting it activated properly...

Hi-- It seems that I've just been putting up with the indentation behavior you describe (!) but spurred by your question I arrived at the following which is maybe the behavior you want?

• For lean4-mode, redefine the newline behavior to have new lines indented to (current-indentation) of the preceding line. In the code below, this is accomplished by defining lean4-newline-and-indent and having some code in the lean4-mode-hook assign this function to the return key.
• For good measure, I also set <backtab> (i.e. "shift-tab") to lean4-eri-indent-reverse so that you can easily back up indentation levels .

Here is the code I (now) use to initialize lean4-mode in my emacs initialization:

(use-package lean4-mode
  :defer t
  :commands (lean4-mode)
  :vc (:url "https://github.com/leanprover-community/lean4-mode.git"
       :rev :last-release
      )
  :config
  (defun lean4-newline-and-indent ()
    "Insert a newline and indent according to the previous line."
    (interactive)
    (let ((indentation (current-indentation)))
      (newline)
      (indent-line-to indentation)))

  (add-hook 'lean4-mode-hook
          (lambda ()
            (local-set-key (kbd "RET") 'lean4-newline-and-indent)
            (local-set-key (kbd "<backtab>") 'lean4-eri-indent-reverse)))
  :custom
  (lean4-keybinding-auto-complete (kbd "C-c C-SPC")))

(I think there is some way to give use-package a :keys argument which probably avoids some of the boilerplate in the add-hook call, but I was feeling lazy and didn't dig into it)

best,
George

[Clément Blaudeau]

Thank you ! I'll add it to my config and see how it feels over the coming Lean sessions