Stream: new members

Topic: lecture notes

Thorsten Altenkirch (Sep 03 2020 at 16:58):

Hi everybody,

I am using Agda and have been using coq in the past. I am going to get back my formal verification course this autumn and I am planning to switch from Coq to Lean.

What is the best way to write lecture notes including lean code. I have been using literate programming for Agda in the past with latex in the past.
I like the style of the "Theorem proving in Lean", especially being able to include workable examples via the web interface.

Cheers,
Thorsten

Patrick Massot (Sep 03 2020 at 17:07):

You can copy the setup of "Theorem proving in Lean", the source code is on GitHub. If you prefer to read things in VSCode and do the exercises in VSCode directly (using a local Lean install, you can look at how "Mathematics in Lean" is setup). For a non-interactive version there is format_lean.

Kenny Lau (Sep 03 2020 at 17:22):

is there a way to have Lean syntax highlighter in LaTeX?

Mario Carneiro (Sep 03 2020 at 17:28):

https://github.com/leanprover-community/lean/blob/master/extras/latex/lstlean.md

Thorsten Altenkirch (Sep 03 2020 at 17:48):

Thank you, Patrick. Actually I prefer using emacs but can move to VSCode if that's better.

Thorsten Altenkirch (Sep 03 2020 at 17:49):

Actually where on GitHub do I find the source code for the book?

Rob Lewis (Sep 03 2020 at 18:22):

Thorsten Altenkirch said:

Actually where on GitHub do I find the source code for the book?

https://github.com/leanprover/theorem_proving_in_lean

Rob Lewis (Sep 03 2020 at 18:24):

https://github.com/avigad/mathematics_in_lean_source is the source for MiL, based on similar technology but with a mathlib dependency and more designed for in-editor use.

Rob Lewis (Sep 03 2020 at 18:28):

I don't think there's been any work done on integrating the textbook display with emacs. In VSCode you get a Lean window side by side with the text, and the "try it" links open in that Lean window.

Jeremy Avigad (Sep 04 2020 at 11:29):

@Thorsten Altenkirch, Gabriel Ebner did most of the Sphinx customization for the tutorials, and it works great. As has been suggested, one option is to copy an existing tutorial (Mathematics in Lean is the most recent) and modify it. If you like to have the feeling of knowing what is going on under the hood, another option is to do a standard Sphinx setup, compare it to an existing tutorial, and then modify the Sphinx setup to match. IIRC, the key additions are these:

• Gabriel wrote lean_sphinx.py to make it possible to test all the Lean snippets with make leantest.
• He modified make.bat to add a procedure to install python and pygments. He also changed the SPHINXBUILD = sphinx-build to SPHINXBUILD = python -msphinx. (At one point I thought I figured out why, but now I don't remember.)
• You have to go through the conf.py file and get the settings right. Again, you can do this by comparing line-by-line to e.g. the one in Mathematics in Lean. For example, we use xelatex and the unixode.sty package to handle unicode, and I added some things to the latex preamble. I also tinkered with the fonts and font sizes.
• We use the alabaster Sphinx theme, but I made a small modification to the sidebar, in source/_templates. It is just cosmetic.
• Gabriel wrote a deploy.sh script to deploy the html. The one in Mathematics in Lean is more complicated than the others, since it also sets up the user version of the repository with copies of all the exercises, so that when they open up an exercise, they can modify it and save it in a local folder. For example, formathematics_in_lean, the source repository is mathematics_in_lean_source, and we deploy to mathematics_in_lean for both the github.io pages and the user version of the repository. (The arrangement is currently imperfect: if users pull a new version of the repository, it overwrites any work they have done.)
• We make the source repository a Lean project (see the leanproject documentation) and install mathlib locally. That way, we can control the versions of Lean and mathlib that users have when they install it on their machine, and we can test the snippets against that version.

Use make html to build / test the html, make latexpdf to build / test the latex, and make leantest to test all the snippets. You can deploy it anywhere: deploy foo bar puts it at foo.github.io/bar (assuming you have set that repository to show pages on github.io. The version for mathematics_in_lean also set github/foo/bar to be the user template. (For example, in mathematics_in_lean, the source repository is mathematics_in_lean_source, and we deploy to mathematics_in_lean) I often deploy pages to a separate test repository (like avigad/mathematics_in_lean) just to check them online and make sure everything looks o.k. before deploying again to the official one (leanprover-community/mathematics_in_lean).

Like I said, the system works great. You have to get used to restructured text conventions, but writing, testing, and deploying goes very smoothly.

We can imagine some improvements. For mathematics_in_lean, it would be nice to have longer examples stored in the local repository (and in a github repository for the online version) so that we can quote from them in the text and users can click to jump to the corresponding place in a longer file. So we may be playing around with that over the next few months. But for short, self-contained examples, the snippets work great. You can limit what is displayed in the textbook (for example, to suppress repeated import statements and definitions) by putting them between -- BEGIN and -- END comments, as you'll see frequently done in our tutorials.

One more thing: when users are running VS Code with Lean, they can type Ctrl-Shift P (or Cmd-Shift P on a Mac, I think) to get the menu and then type Lean: Open Documentation View, and that gives them a list of tutorials they can run in the browser. If you want to add yours to the list, you have to add it to the Lean VS Code interface: https://github.com/leanprover/vscode-lean/blob/master/src/docview.ts#L108-L114. I think @Gabriel Ebner doesn't mind merging a pull request, and I am sure Lean users will be happy to have another tutorial to play with.

Jasmin Blanchette (Sep 04 2020 at 11:38):

Nobody has mentioned the "wrong way" of doing it, so I'll do so for the record. For the Hitchhiker's Guide, I used a modified version of Jeremy's lstlean.sty setup, even with the official VSCode colors for syntax highlighting. It's a great setup if you love LaTeX and hate all things web. ;)

Last updated: May 13 2021 at 23:16 UTC