1

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
#+end_src

Now I want to use that information:

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

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 Apr 3 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. – Joe Corneli Apr 3 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 Apr 3 at 15:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.