readable (literate) proofs

Stream: general

[Matthew Pocock]

Is there a tutorial or style guide for writing proof documents that are human-reader oriented? I have a file full of theorems and code comments, but would prefer something more like a literate programming document that can be viewed as pdf/html.

[Arthur Paulino]

Check out the infra that's set for https://github.com/leanprover-community/lean4-metaprogramming-book
The core trick is using lean2md
Once you turn your file into markdown, you're free to do much more with whatever tools exist out there

Edit: note that lean2md won't handle comments with /- ... -/ inside Lean code blocks because it's a very simple tool that was created for the specific purpose of writing the metaprogramming book

[Sebastian Ullrich]

We have a tool for producing interactive proof documents though it's not as nicely integrated as it could be: https://github.com/leanprover/LeanInk
Examples: https://leanprover.github.io/lean4/doc/examples.html

[Martin Dvořák]

Am I the only one who prefers reading Lean over reading PDFs?

[Arthur Paulino]

It clearly depends on the target audience and the context

[Eric Wieser]

but would prefer something more like a literate programming document that can be viewed as pdf/html.

doc-gen can do this in some sense; every /-! comment is rendered as markdown between declarations

[Matthew Pocock]

Thanks. I will have a play with these. Is there any support for live-preview of the formatted document within vs code?

[Arthur Paulino]

Not yet (bait attempt!)

[Arthur Paulino]

I'd say LeanInk is arguably the one that deserves further support/integration/simplification

[Jujian Zhang]

EEF9C729-1038-4B94-A451-9E3F9711CA7B.png

DB79F1B3-2FE3-484A-BF9A-FF0C4C46AE31.png

By using poly mode and emacs, one can set up a mixed mode to write Lean code as normal and org-style comments including rendering of maths equations and commutative diagram and displaying images.

[Tomas Skrivan]

Did you try to convert the org file into html using LeanInk? I would be quite interested in that.

[Jujian Zhang]

(deleted)

[Jujian Zhang]

(deleted)

[Jujian Zhang]

(deleted)

[Jujian Zhang]

I added rst-mode supported in emacs:
Screenshot-2023-09-26-at-12.23.02.png

exporting it via alectryon and leanink, it looks like this:
Screenshot-2023-09-26-at-12.23.15.png

[Jujian Zhang]

emacs setup:

1. download polymode
2. add the following into emacs config file

(require 'polymode)

(defun pm--lean4org-head-matcher (ahead)
  (when (re-search-forward "^[ \t]*\/-*Org" nil t ahead)
    (cons (match-beginning 0) (match-end 0))))

(defun pm--lean4org-tail-matcher (ahead)
  (when (< ahead 0)
    (error "Backwards tail match not implemented"))
  ;; may be rely on syntactic lookup ?
  (when (re-search-forward "^[ \t]*-*\/[ \t]*")
    (cons (match-beginning 0) (match-end 0))))

(define-innermode poly-lean4-org-innermode
  :mode 'org-mode
  :head-matcher 'pm--lean4org-head-matcher
  :tail-matcher 'pm--lean4org-tail-matcher
  :head-mode 'host
  :tail-mode 'host)

(defun pm--lean4rst-head-matcher (ahead)
  (when (re-search-forward "\/-!" nil t ahead)
    (cons (match-beginning 0) (match-end 0))))

(defun pm--lean4rst-tail-matcher (ahead)
  (when (< ahead 0)
    (error "Backwards tail match not implemented"))
  (when (re-search-forward "^[ \t]*-*\/[ \t]*")
    (cons (match-beginning 0) (match-end 0))))

(define-innermode poly-lean4-rst-innermode
  :mode 'rst-mode
  :head-matcher 'pm--lean4rst-head-matcher
  :tail-matcher 'pm--lean4rst-tail-matcher
  :head-mode 'host
  :tail-mode 'host)

(define-hostmode poly-lean4-hostmode
  :mode 'lean4-mode)

(define-polymode poly-lean4-mode
  :hostmode 'poly-lean4-hostmode
  :innermodes
  '(poly-lean4-org-innermode poly-lean4-rst-innermode))

3. use poly-lean4-mode in a lean file buffer