6

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?

Improve this question
3
  • 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? 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. Commented Apr 3, 2019 at 15:55

1 Answer 1

Reset to default
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" #+end_src #+begin_src lean4 :noweb strip-export <<define-foo>> #eval foo #+end_src
Improve this answer
1
  • Your examples work but when I try to import mathlib then I run into problems. I will raise an issue. Commented Dec 27, 2024 at 7:09

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.