literate lean

Stream: general

[Thorsten Altenkirch]

What is the best way to write a document including lean proofs using latex or markup? I only want to have one source as in literate programming, and I don't want to repeat Lean code (which is what happens when I use the sphinx markup I use for my lecture notes, because the lean code blocks cannot depend on each other.

[Eric Wieser]

Thorsten Altenkirch said:

What is the best way to write a document including lean proofs using latex or markup? I only want to have one source as in literate programming, and I don't want to repeat Lean code (which is what happens when I use the sphinx markup I use for my lecture notes, because the lean code blocks cannot depend on each other.

If you want to stick to sphinx, it shouldn't be too hard to write a plugin that makes this work; there are already such plugins for things like ipython

[Eric Wieser]

How are you using sphinx with lean at the moment? It sounds like you have it set up so that it can run individual blocks already?

[Johan Commelin]

@Thorsten Altenkirch Two examples are: https://www.ma.imperial.ac.uk/~buzzard/docs/lean/sandwich.html
https://leanprover-community.github.io/mathematics_in_lean/introduction.html

[Johan Commelin]

@Gabriel Ebner knows how to setup the second. I think it uses sphinx

[Thorsten Altenkirch]

I co
Eric Wieser said:

Thorsten Altenkirch said:

What is the best way to write a document including lean proofs using latex or markup? I only want to have one source as in literate programming, and I don't want to repeat Lean code (which is what happens when I use the sphinx markup I use for my lecture notes, because the lean code blocks cannot depend on each other.

If you want to stick to sphinx, it shouldn't be too hard to write a plugin that makes this work; there are already such plugins for things like ipython

I copied Jeremy et al's setup for the lean tutorial but as I said it doesn't use the contents of previous code boxes.

[Eric Wieser]

Presumably you're referring to the "try it" links that open the web editor?

[Gabriel Ebner]

That's somewhat by design. You can add extra Lean code that doesn't show up in the rendered document by placing it outside of the -- BEGIN and -- END markers like here: https://github.com/leanprover/theorem_proving_in_lean/blame/6cd7dd5d5c225a46a29bedd0081468c5b097c424/axioms_and_computation.rst#L133-L148

[Thorsten Altenkirch]

Johan Commelin said:

Gabriel Ebner knows how to setup the second. I think it uses sphinx

Yes, I am using this setup. Now I have a student who is writing his project report about a Lean project. The disadavnatgae is that code blocks can't depend on each other.

[Thorsten Altenkirch]

Gabriel Ebner said:

That's somewhat by design. You can add extra Lean code that doesn't show up in the rendered document by placing it outside of the -- BEGIN and -- END markers like here: https://github.com/leanprover/theorem_proving_in_lean/blame/6cd7dd5d5c225a46a29bedd0081468c5b097c424/axioms_and_computation.rst#L133-L148

Yes, I know and I am using this. However, the point of literate programming is that you don't have to repeat code because when you change something you only want to change it in one place.

[Gabriel Ebner]

The code that extracts the Lean code from the document is super simple, you can probably change it to concatenate the previous snippets: https://github.com/leanprover/theorem_proving_in_lean/blob/6cd7dd5d5c225a46a29bedd0081468c5b097c424/lean_sphinx.py#L28-L44

[Eric Wieser]

You could probably even use the existing :names: mechanic to concatenate code if it shares the same name

[Eric Wieser]

Ah, that's only present in https://github.com/avigad/mathematics_in_lean_source/blob/master/lean_sphinx.py#L29-L51

[Eric Wieser]

I guess we should probably make a new repo to contain the sphinx extension so that we don't have these diverging duplicates?

[Gabriel Ebner]

The "mathematics in lean" version of the script is definitely the odd one out here. The names feature is really specific to that one book, it's also the only book that distributes a git repository with the extracted snippets.