lecture notes

Stream: new members

[Thorsten Altenkirch]

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]

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]

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

[Mario Carneiro]

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

[Thorsten Altenkirch]

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

[Thorsten Altenkirch]

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

[Rob Lewis]

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]

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]

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]

@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]

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. ;)

[Gihan Marasingha]

I'm trying to do that for my latest lecture notes. How do I find the official vscode colors? Is your modified lstlean.tex publicly available @Jasmin Blanchette ?

[Jasmin Blanchette]

It's a crude hack. I hope you enjoy it.
lstleanx.sty](/user_uploads/3121/wBYFFbLVdxoOB8MQlVE-YwPs/lstleanx.sty)

[Jasmin Blanchette]

In LaTeX:

\definecolor{keywordcolor}{rgb}{0,0,1}          % blue
\definecolor{sortcolor}{rgb}{0,0,1}             % blue
\definecolor{commentcolor}{rgb}{0,0.5,0}        % darkish green
\definecolor{stringcolor}{rgb}{.65,.07,.04}     % reddish
\definecolor{symbolcolor}{rgb}{.18,.49,.72}     % blueish
\definecolor{sorrycolor}{rgb}{0.91,0,0}         % fairly hot red
\definecolor{numeralcolor}{rgb}{0,0.53,0.34}    % greenish
\definecolor{modifiercolor}{rgb}{.69,0,.87}     % magentaish
\definecolor{procnamecolor}{rgb}{.55,.37,.13}   % brownish
\definecolor{ctxtcolor}{rgb}{.85,.46,0}         % orange
\definecolor{preprocessorcolor}{rgb}{0,0,1}     % blue

[Gihan Marasingha]

Thanks @Jasmin Blanchette ! Were there changes other than the colors? The upload link for lstleanx.sty isn't working for me.

[Eric Wieser]

Gihan Marasingha said:

I'm trying to do that for my latest lecture notes. How do I find the official vscode colors? Is your modified lstlean.tex publicly available Jasmin Blanchette ?

The vscode default themes are here: https://github.com/microsoft/vscode/tree/main/extensions/theme-defaults/themes

[Eric Wieser]

If you run the "Developer: Inspect Editor Tokens and Scope" command (via Ctrl + Shift + P) in vscode, you can also just ask for the color of the text under the cursor:

image.png

[Jasmin Blanchette]

Let me try again:
lstleanx.sty

[Jasmin Blanchette]

I got the colors using a color picker.