Zulip Chat Archive
Stream: new members
Topic: Literate programming
Pedro Minicz (Oct 05 2020 at 17:47):
Does Lean support literate programming? I couldn't find anything, so I assume it doesn't. How hard should it be to implement it?
I assume some Markdown or TeX preprocesser able to extract code (which then could be checked by Lean) should exist, but I am not aware of any.
Eric Wieser (Oct 05 2020 at 18:36):
https://leanprover-community.github.io/format_lean/
Adam Topaz (Oct 05 2020 at 18:38):
It would be really cool to also have something like this:
https://agda.github.io/agda-stdlib/
Adam Topaz (Oct 05 2020 at 18:39):
I guess the API docs are an approximation of this.
Adam Topaz (Oct 05 2020 at 18:42):
If you're an emacs person, there is surely some way to embed lean code in an org-mode file, which you can then (presumably) extract to whatever you want.
Adam Topaz (Oct 05 2020 at 18:42):
Of course this is not ideal.
Bryan Gin-ge Chen (Oct 05 2020 at 18:47):
I think the first step for a literate programming implementation for Lean would be to collect proposals for a "literate Lean" file format (.llean?). Once the design / bikeshedding is done I'd be happy to help out with the vscode-lean side of things.
Adam Topaz (Oct 05 2020 at 18:48):
foo.lean.tex?
Kyle Miller (Oct 05 2020 at 18:49):
Pedro Minicz said:
Does Lean support literate programming?
Do you mean Knuth-style literate programming (like the TeX source code and WEB), or do you mean Haskell-style where everything is a comment unless otherwise specified? (I can't answer either way, but there's a spectrum of what "literate programming" even means.)
Adam Topaz (Oct 05 2020 at 18:55):
Just trying it out with org-mode
* Introduction
Here is some text
#+BEGIN_SRC lean
inductive mynat
| zero : mynat
| succ : mynat → mynat
#+END_SRC
At least things are highlighted correctly and editing lets me put in unicode as expected from lean-mode.
Adam Topaz (Oct 05 2020 at 18:55):
I'll try converting to PDF to see what happens. Still not sure about code execution either.
Adam Topaz (Oct 05 2020 at 18:56):
This was the pdf output:
test.pdf
Adam Topaz (Oct 05 2020 at 18:57):
Someone who knows elisp and/or pandoc better than I do can probably arrange for the latex extraction to use the correct style files for lean code.
Adam Topaz (Oct 05 2020 at 19:05):
Okay, code execution doesn't work out of the box, but it shouldn't be hard to modify this elisp file
https://code.orgmode.org/bzg/worg/raw/master/org-contrib/babel/ob-template.el
to work with lean.
Yury G. Kudryashov (Oct 05 2020 at 20:07):
The downside of this solution is that it's editor specific.
Yury G. Kudryashov (Oct 05 2020 at 20:07):
Though as an Emacs user I like it.
Adam Topaz (Oct 05 2020 at 20:13):
I'm not suggesting this is a realistic solution :) I was just experimenting with what I have on hand.
Yury G. Kudryashov (Oct 05 2020 at 20:16):
It's easy to write a plug-in for https://asciidoctor.org/ that will write code to external files.
Adam Topaz (Oct 05 2020 at 20:18):
I feel like asciidoc is even more obscure than org-mode.
Yury G. Kudryashov (Oct 05 2020 at 20:19):
Why?
Adam Topaz (Oct 05 2020 at 20:19):
I could be wrong.
Adam Topaz (Oct 05 2020 at 20:20):
Personally I have only heard of it in passing.
Yury G. Kudryashov (Oct 05 2020 at 20:24):
I like callouts in quoted source Screenshot
Pedro Minicz (Oct 05 2020 at 20:33):
Well, as a mostly terminal-only programmer I have to say, I've heard of AsciiDoc, never used nor heard of Asciidoctor.
Pedro Minicz (Oct 05 2020 at 20:33):
But it does look pretty cool.
Pedro Minicz (Oct 05 2020 at 20:34):
Kyle Miller said:
Pedro Minicz said:
Does Lean support literate programming?
Do you mean Knuth-style literate programming (like the TeX source code and WEB), or do you mean Haskell-style where everything is a comment unless otherwise specified? (I can't answer either way, but there's a spectrum of what "literate programming" even means.)
Well, I've never used literate programming in C or Haskell, but I have used it in Agda, which I am willing to bet is more Haskell like.
Bryan Gin-ge Chen (Nov 21 2020 at 22:20):
I happened to see this today on Hacker News: "Alectryon (named after the Greek god of chicken) is a collection of tools for writing technical documents that mix Coq code and prose, in a style sometimes called literate programming."
Andreu Cotanda (Aug 16 2023 at 15:56):
Hi! Are there any updates on literate programming with Lean apart from LeanInk? I've been looking to use lean in emacs org-mode files but I cannot find any documentation for that (if it is even possible).
Henrik Böving (Aug 16 2023 at 17:41):
No not really. I guess you can count the docs renderer a bit? But nothing dedicated
Jujian Zhang (Sep 24 2023 at 15:16):
If you are open to use emacs, polymode allows you to mix two major mode together so that you can write Lean code normally and write comment in org mode so that you can render equations, commutative diagram and images.
Jujian Zhang (Sep 24 2023 at 15:16):
D6DAC4B6-BAC7-4874-8137-D7E58337CC11.png
3ACC1867-B685-4E55-BF19-A371E20A856A.png
Kyle Miller (Sep 24 2023 at 18:25):
Last updated: Dec 20 2023 at 11:08 UTC