dark mode

Stream: general

[Sahan Wijetunga]

is there a way to get theorem proving in lean in dark mode

[Martin Dvořák]

If you are in VS Code, you can switch it in:
File -> Preferences -> Themes

[Martin Dvořák]

Also this is an opportunity for me to advertise my own color scheme highly optimized for Lean 4 in VS Code with dark mode:
https://github.com/madvorak/vscode-lean4-colors

[Sahan Wijetunga]

As in the textbook "Theorem Proving in Lean 4"

(I'm accessing it through https://leanprover.github.io/theorem_proving_in_lean4 but I don't see a way to change theme to dark mode. It was previously in dark mode automatically I think but they updated things today)

[Niels Voss]

It seems that it was updated to use verso instead of what they were using previously (mdbook I think). I don't know if verso has dark mode yet

[Arthur Paulino]

I know it's been requested before

[Alex Sweeney]

Bumping this because it's important to me :cry:

[Snir Broshi]

Are any of these sufficient?
image.png
image.png
image.png

https://darkreader.org/ it's a general algorithm and isn't customized per website, but it usually works good enough.

[Niklas Halonen]

This issue is tracked here: https://github.com/leanprover/verso/issues/641 and there is active work ongoing in a PR: https://github.com/leanprover/verso/pull/676