org-mode

Stream: Emacs

[Dominic Steinitz]

I am writing a blog but would like the code in the blog to be executed. Does anyone have any views on this: https://github.com/Maverobot/ob-lean4? See also https://emacs.stackexchange.com/questions/48732/live-literate-lean-programming-with-org-mode

[Yury G. Kudryashov]

I haven't tried this yet.

[Mauricio Collares]

Part of the problem is that you have to define what "to be executed" means. Org is nice, but it doesn't have infoview support. If you're talking about the code you posted in the other thread, it produces no output at all when viewed as a traditional program (you don't run #eval, #check or the like). That's why verso is probably the best option for your blog.

[Mauricio Collares]

Ah, do you mean you would like the infoview to work while the org buffer is open? That would be amazing, but I don't think ob-lean4 provides this feature.

[Dominic Steinitz]

Mauricio Collares said:

That's why verso is probably the best option for your blog.

Hmmm I am not sure how I get latex into verso

image.png

[Dominic Steinitz]

Mauricio Collares said:

Ah, do you mean you would like the infoview to work while the org buffer is open? That would be amazing, but I don't think ob-lean4 provides this feature.

That's what I would like - verso is a whole new package to learn

[Dominic Steinitz]

Well neither ob-lean4 nor verso are working for me yet.

[Dominic Steinitz]

So the best I can do at the moment is to write the blog post in org mode and export just the code to check the lean and compile to latex / pdf to check the formatting. Ultimately I will convert to markdown and then GitHub pages will render it correctly (pause for laughter).

[Malvin Gattinger]

I also got curious about getting org-mode with working InfoView, and I think mmm-mode can do it! However, I am currently using the eglot-compatible fork by bustercopley so this may not work with the current normal / lsp-mode version.

Screenshot_20241227_203230.png

/-
Annoyingly, stuff outside of BEGIN_SRC lean4 is
seen by lean4 via eglot, so we need to comment it.

** The Example

#+BEGIN_SRC lean4
-/
def hello := "hallo" ++ sorry

#print hello
/-
#+END_SRC

Here could be other text.

** The Setup of mmm-mode

The following is adapted from https://emacs.stackexchange.com/a/28269.
Select it, then ~M-x eval-region~, then re-open this file.

#+BEGIN_SRC emacs-lisp
(require 'mmm-mode)
(setq mmm-global-mode 'maybe)
(mmm-add-mode-ext-class 'org-mode nil 'org-lean4)
(mmm-add-mode-ext-class 'org-mode nil 'org-elisp)

(mmm-add-group
 'org-lean4
 '((lean-src-block
    :submode lean4-mode
    :face org-block
    :front "#\\+BEGIN_SRC lean4.*\n"
    :back "#\\+END_SRC")))

(mmm-add-group
 'org-elisp
 '((elisp-src-block
    :submode emacs-lisp-mode
    :face org-block
    :front "#\\+BEGIN_SRC emacs-lisp.*\n"
    :back "#\\+END_SRC")))
#+END_SRC

Again, we are still "inside" a Lean comment.
-/

[Mauricio Collares]

Dominic Steinitz said:

Hmmm I am not sure how I get latex into verso

mathjax or katex, maybe? You can take inspiration from the reference manual: https://github.com/leanprover/reference-manual/blob/main/Main.lean

[Dominic Steinitz]

Mauricio Collares said:

Dominic Steinitz said:

Hmmm I am not sure how I get latex into verso

mathjax or katex, maybe? You can take inspiration from the reference manual: https://github.com/leanprover/reference-manual/blob/main/Main.lean

Thanks very much but I didn't see anything in your link. There is this issue https://github.com/leanprover/verso/issues/54 but I am still not clear on how one should write latex formulae.