I would like to use lean-mode and org-mode together to write literate code that is also being parsed by the Lean server.

lean-mode (available on melpa) supports a live-coding style of interaction, illustrated here with flycheck-inline output.

enter image description here

I'm aware of Org Mode's sessions, which support a literate style for scripting languages. Any suggestions about what would be involved in setting this up for Lean?

Here's a currently-not-working example, save as lll.org, notice that cursor-over on the #check line does nothing at present.

#+Title: Can I do literate live coding with lean?
Here I set up some imports.

#+begin_src lean
import topology.basic data.set.intervals
open real set

Now I want to use that information:

#+begin_src lean
#check (Icc (0:ℝ) 1)

Summary of the challenge

I would like the collection of lean source code blocks within one org-mode file to operate as if they were different transcluded portions of one buffer in lean-mode. The Lean server should be active on all of these blocks, and the contents of the blocks should interoperate, e.g., so that import in an earlier block will make the imported definitions available in later blocks. How could this be arranged?

  • What's the question? What's not "working" about the example - what do you expect/want it to do, and what does it do instead?
    – Drew
    Commented Apr 3, 2019 at 15:19
  • The desired behavior is: cursor-over the #check and have Lean print a result, via flycheck, as in the screenshot of from the lean-mode buffer above. In the Org mode sample, my lean source code blocks use lean-mode for highlighting, but the Lean server is not invoked. Commented Apr 3, 2019 at 15:29
  • 1
    @JoeCorneli Org-mode puts the source blocks in a temporary buffer, selects the required major mode, and lets font-lock do its work. The text properties are then put onto the corresponding regions in the source block (see definition of org-src-font-lock-fontify-block). Flycheck uses overlays. I doubt that overlays survive the procedure of Org mode in any way. To get what you want you would have to define a org-babel-execute:lean for non-nil :session argument. Looks like there is currently no such thing.
    – Tobias
    Commented Apr 3, 2019 at 15:55

1 Answer 1


I've put together a package ob-lean4 that aims to assist in evaluating lean4 source blocks within org files. It's a simple tool meant to facilitate the execution of lean4 code within the context of org documents.

At present, the package doesn't offer support for :session. However, you can still engage in a form of literate programming to some extent using :noweb:

#+name: define-foo
#+begin_src lean4
  def foo : String := "Lean"

#+begin_src lean4 :noweb strip-export
  #eval foo

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.