Zulip Chat Archive

Stream: new members

Topic: Literate programming


view this post on Zulip 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.

view this post on Zulip Eric Wieser (Oct 05 2020 at 18:36):

https://leanprover-community.github.io/format_lean/

view this post on Zulip 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/

view this post on Zulip Adam Topaz (Oct 05 2020 at 18:39):

I guess the API docs are an approximation of this.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 05 2020 at 18:42):

Of course this is not ideal.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 05 2020 at 18:48):

foo.lean.tex?

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 05 2020 at 18:56):

This was the pdf output:
test.pdf

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 20:07):

The downside of this solution is that it's editor specific.

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 20:07):

Though as an Emacs user I like it.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 05 2020 at 20:18):

I feel like asciidoc is even more obscure than org-mode.

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 20:19):

Why?

view this post on Zulip Adam Topaz (Oct 05 2020 at 20:19):

I could be wrong.

view this post on Zulip Adam Topaz (Oct 05 2020 at 20:20):

Personally I have only heard of it in passing.

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 20:24):

I like callouts in quoted source Screenshot

view this post on Zulip 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.

view this post on Zulip Pedro Minicz (Oct 05 2020 at 20:33):

But it does look pretty cool.

view this post on Zulip 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.

view this post on Zulip 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."


Last updated: May 13 2021 at 23:16 UTC