Preparing HTML slides

Stream: Lean for teaching

[Graham Leach-Krouse]

Does anyone have a technique they like for embedding lean snippets into HTML slides (for example, reveal.js or similar)? :ToHTML in vim is an option, I guess, but it would be nice to have something cleaner.

[Britt Anderson]

If all you want to do is get some typesetting, and not the interactive evaluation I think any markdown dialect could do that . I use emacs and orgmode. Since you can also use emacs instead of vscode you might find that option worth exploring. You can use "evil" mode to emulate vim key bindings in emacs and there is a lean4 mode for emacs.

[Graham Leach-Krouse]

Yes, I was hoping for something beyond just typesetting - I'm not sure if there's some way of using LeanInk (which I guess is no longer active) or verso for making slides...

[Anand Rao Tadipatri]

This isn't quite what you're looking for, but Lean Slides allows Reveal JS slides to be displayed from within the Lean editor.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Here are some slides also running in the Lean editor, where the Lean code appearing therein is interactive (using the same JS components as the tactic state display). I'm actually not sure this is preferrable for presentations, because there you may prefer syntax highlighting (which the tactic state still doesn't have :cry:), but might be worth considering.

[Eric Wieser]

There is a highlight.js plugin for Lean that works just fine with reveal.js

[Graham Leach-Krouse]

@Anand Rao Tadipatri Not quite what I was looking for, but very interesting nonetheless, thanks! @Eric Wieser Thanks, I'll check that out.

[Utensil Song]

You might want to check out Eric's beautifully highlighted and animated Lean slides using highlightjs and revealjs, e.g. https://eric-wieser.github.io/cicm-2023/

[Andrés Goens]

Utensil Song said:

You might want to check out Eric's beautifully highlighted and animated Lean slides using highlightjs and revealjs, e.g. https://eric-wieser.github.io/cicm-2023/

wow, this looks really nice! @Eric Wieser is there a recording of that presentation somewhere?

[Eric Wieser]

Yes! https://www.youtube.com/watch?v=p7nQX0nQsCA