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.

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 windows into 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?

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.

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?

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.

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 

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.

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 windows into 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?