add dark theme

[cuppajoeman]

Aside from the dark theme this commit adds a button which lets you toggle the color scheme which saves your setting between sessions.

[eric-wieser]

deploy

[eric-wieser]

Hmm, that crashed...

[eric-wieser]

deploy

[eric-wieser]

@gebner, any idea what's causing deployment failures? Is this the "runner is too puny" problem that motivated self-hosted runners elsewhere?

[ericrbg]

hmm, I doubt this is what it is, but you need to tell the main .py to copy stuff over for it to work, see my changes to print_docs.py here

[gebner]

any idea what's causing deployment failures? Is this the "runner is too puny" problem that motivated self-hosted runners elsewhere?

Yes, I only moved the regular CI over to the self-hosted runners but forgot about #deploy since that's a separate workflow.

deploy

[github-actions[bot]]

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

[eric-wieser]

deploy

[github-actions[bot]]

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

[ericrbg]

I think the main background is a bit too light, which makes all the other colours look a bit washed out. maybe something like #171717? I'm no good at colour though.

[gebner]

deploy

[github-actions[bot]]

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

[gebner]

deploy

[github-actions[bot]]

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

[gebner]

deploy

[github-actions[bot]]

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

[digama0]

There is a black text header at https://leanprover-community.github.io/mathlib_docs_demo/commands.html##explode%20/%20#explode_widget, and the red color of Prop in the code block is too dark. I suggest using an actual dark-mode theme as a base for modification, because the color choices all seem not that great and it's probably hard to get a coordinated look otherwise.

[gebner]

Does the newest commit solve this for you?

Not really. Changing the system style doesn't take effect immediately on the docs website. Sometimes I also have to press the toggle twice before it takes effect.

Two other things:

• The toggle button is not visible on portrait (less than 700px wide)
• The hamburger button only has light colors (also for portrait mode).
• Between ~700-800px window width, the toggle button overflows into a second line (because it is too wide).
• The toggle button is inside the search form (that might get sent to google)

What I would suggest for the portrait styling issues is to 1) put the toggle button after the form, 2) remove the header-side-padding, and 3) put an empty <div></div> at the beginning of the header. I would also change the button text to something shorter and more descriptive, that is, "dark" or "🌓" instead of "toggle theme".

[cuppajoeman]

I've added some more changes today to add more variables with respect to Eric's post.

I see that @gebner still has the issue with his operating system color scheme changes not affecting the site, to that end I don't really know why that window.matchMedia doesn't work, so if anyone wants to take a look at that please do.

As for the other styling issues that gebner mentioned, I can try to do that as well, but it probably wouldn't get to it until the end of the day today or in the next day, so if anyone wants to take that on today then there wouldn't be any conflicts.

[eric-wieser]

deploy

[github-actions[bot]]

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

[cuppajoeman]

Does the newest commit solve this for you?

Not really. Changing the system style doesn't take effect immediately on the docs website. Sometimes I also have to press the toggle twice before it takes effect.

Two other things:

* The toggle button is not visible on portrait (less than 700px wide)

* The hamburger button only has light colors (also for portrait mode).

* Between ~700-800px window width, the toggle button overflows into a second line (because it is too wide).

* The toggle button is inside the search form (that might get sent to google)

What I would suggest for the portrait styling issues is to 1) put the toggle button after the form, 2) remove the header-side-padding, and 3) put an empty <div></div> at the beginning of the header. I would also change the button text to something shorter and more descriptive, that is, "dark" or "first_quarter_moon" instead of "toggle theme".

I've added these changes

[eric-wieser]

deploy

[github-actions[bot]]

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

[robertylewis]

Some weird-looking spots, on a spotcheck:

(same on all the "general documentation" pages)

This appears everywhere except the index page, and clicking it does nothing:

[robertylewis]

I would also prefer the toggle to be more subtle than a big button at the top. As someone who doesn't use dark themes, I may be blind to this. But it isn't common web design to put this kind of toggle so prominently on a page, is it?

[cuppajoeman]

Some weird-looking spots, on a spotcheck:

(same on all the "general documentation" pages)

This appears everywhere except the index page, and clicking it does nothing:

Thanks for catching these - I'll fix up these things tonight.

As for your other comment - I'm not really sure whether it's good practice or not to put the button up there, but I've definitely seen websites which do that.

[cuppajoeman]

When I load up the tactics page it looks like this:

which is unlike what @robertylewis was reporting, so probably they just need to refresh the page to get the new css (ctrl-shift-r) usually works for that. Besides that I've updated the button so it should actually toggle the theme and removed the old toggle button, can we rebuild and see how it looks?

[bryangingechen]

deploy

[github-actions[bot]]

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

[cuppajoeman]

I think with the newest changes this seems almost good to go!

[eric-wieser]

There are still a handful of uncorrected colors. For instance, .decl.sorried is likely to be way too pastel, and the hamburger goes while when clicked.