dark theme mathlib docs

Stream: general

[ccn]

Hi there,

I've started working on making a version of the mathlib docs which has a darker theme. You can find the docs here:

https://cuppajoeman.github.io/mathlib_docs/

the source is here:

https://github.com/cuppajoeman/mathlib_docs

if you want to experiment with different colors feel free to tweak them using the inspector like this: https://cdn.discordapp.com/attachments/940035706556932197/940268593118085190/simplescreenrecorder-2022-02-07_10.29.08.mp4 . The customized version of the css is in the above repo in the custom.css file. Most of the changes are just variable names in the :root selector.

In the original docs we had the following color scheme for these types (in order):

def, theorem, axiom&constant, structure&inductive, background

image.png

to go with the dark theme I've changed them to be :

image.png

Julian from discord was hinting at being able to have the browser choose which colorscheme to use:

Julian: This is great -- just in case you don't already know, you could also follow what the browser requests here too (i.e. dark if the browser requests a dark theme, original light if it requests a light one)
Julian: I don't know what the media query looks like for that but I know of things that do so, so you could crib their CSS (notably furo from Python: https://github.com/pradyunsg/furo)

But I also think it would be nice to have a switch on the docs page if possible.

Once we have a method to switch between them I think we should make a PR onto the doc-gen repo.

[Eric Wieser]

https://developer.mozilla.org/en-US/docs/Web/CSS/@media/prefers-color-scheme is the feature @Julian Berman is referring to

[ccn]

@Rob Lewis I managed to get this all to work, so there's a button which lets you toggle, and also it saves your color preferences when you reload the site, the one thing is that I don't really know how doc-gen works. The modifications required are to modify the style.css file (which I know how to do), but to also include a link to https://leanprover-community.github.io/mathlib_docs/detect_color_scheme.js and another script at in specific locations in each file. Do you know where I can find code that includes this?

[ccn]

Sorry if you're the wrong person to ping, I just saw that you have contributed to the repo before and that you were online.

[Rob Lewis]

https://github.com/leanprover-community/doc-gen/blob/master/templates/base.j2

[ccn]

Thanks!

[Rob Lewis]

I don't use dark themes, so my opinion might not be worth anything here, but the choice of yellow for links in your demo pretty much blinds me -- it's all I can see when I look at the page. Would it be better to soften that a bit?

[ccn]

Yeah I'm going to test out a different color right now actually.

[ccn]

What do you think about this blue? image.png

[Rob Lewis]

I'm probably the wrong person to ask here. I don't use dark themes so I don't really have a point of comparison

[Rob Lewis]

It's less blinding than the yellow for sure!

[ccn]

Eric also requested for links to be blue, so I'll do this change for now. It's easily changeable if people don't like it in the future.

[ccn]

Ok, I made a PR on the doc-gen github repo: https://github.com/leanprover-community/doc-gen/pull/158

[ccn]

It should work, but apparently my 16gb of ram is isn't enough to build the docs, so hopefully someone who can build the docs can try it out...

[Arthur Paulino]

@ccn You could try the palette from Lean syntax highlight in VS code. I think it would feel like home for many people

[Bhavik Mehta]

I like this idea, but I worry it might feel a bit odd (uncanny valley, perhaps), as the syntax highlighting will be on different tokens but with the usual colours

[Kevin Buzzard]

I certainly will never be going back to light mode whatever colour decisions are made. Thanks ccn!

[Eric Wieser]

For some reason the normal #deploy comment thing on doc-gen isn't working - does anyone know why?

[Eric Wieser]

It's failed twice now with no diagnostics

[Callum Cassidy-Nolan]

Can someone do a #deploy on the PR ? If that looks good it should be ready to merge.

[Callum Cassidy-Nolan]

Can we try another #deploy I've removed the old toggle button and the new should work now.

[Callum Cassidy-Nolan]

Thanks, I think it looks pretty good!

[Callum Cassidy-Nolan]

@Eric Wieser I feel like the PR is ready, is there anything else I should do here?

[Eric Wieser]

I don't feel like the final call is mine to make here. Perhaps @Gabriel Ebner or @Bryan Gin-ge Chen are happy to pull the trigger on this.

[Eric Wieser]

I would maybe lean towards hiding the dark theme toggle at the bottom of the left sidebar

[Gabriel Ebner]

Apparently I pressed the merge button right when you commented Eric. Please make a new PR for the color fixes.

[Eric Rodriguez]

The button doesn't work for me on Firefox Nightly on mobile :(

[Eric Wieser]

Eric Wieser said:

I would maybe lean towards hiding the dark theme toggle at the bottom of the left sidebar

To elaborate on that idea, something like

image.png

[Eric Wieser]

Uglyier, but hidden away rather than in plain view where it isn't needed. Gives a home for things like "show only definitions" or "I don't care about computability" options too

[Gabriel Ebner]

I like it that there is a dedicated system button.

[Gabriel Ebner]

Can you reduce the font size and add a fat margin between the file tree and the settings so that they're visually distinct?

[Eric Wieser]

Let's wait till it deploys then you can fiddle in-browser. Likely I screwed up the JS anyway.

[Gabriel Ebner]

It also needs some space between the three settings. The dark moon looks like another radio button.

[Gabriel Ebner]

https://github.com/leanprover-community/doc-gen/pull/160

[Eric Wieser]

Initially I was after some kind of toggle button group, but eventually I decided I didn't care enough and if we want that type of thing we should just use bootstrap like the main site does

[Eric Wieser]

Eric Wieser said:

Let's wait till it deploys then you can fiddle in-browser. Likely I screwed up the JS anyway.

Alright, it's deployed

[Eric Wieser]

Gabriel Ebner said:

It also needs some space between the three settings. The dark moon looks like another radio button.

Now looks like:

image.png

[Mario Carneiro]

I think the moons should just be dropped. They made more sense when it was an icon button, now it's just confusing

[Eric Wieser]

How about

image.png

image.png