## Stream: Zulip meta

### Topic: Links to code snippets

#### Mario Carneiro (Sep 10 2020 at 13:06):

Zulip is requesting user feedback on a planned feature to allow executing inline snippets: https://github.com/zulip/zulip/issues/11618#issuecomment-689870496 . I wonder if there is a way to get lean in on the action

#### Rob Lewis (Sep 10 2020 at 13:11):

It sounds like Lean is in on the action already: https://github.com/zulip/zulip/pull/16308

#### Rob Lewis (Sep 10 2020 at 13:11):

The five major programming languages: Rust, Python2, Python3, Julia, and Lean

#### Rob Lewis (Sep 10 2020 at 13:20):

For the record, "executing inline snippets" means "opening the web editor with text inserted," which is still very cool.

#### Kevin Buzzard (Sep 10 2020 at 13:29):

That'll do for now!

#### Bryan Gin-ge Chen (Sep 10 2020 at 15:03):

That's great! I wonder if we should start thinking about hosting different versions of Lean + mathlib on the web editor at some point...

edit: Maybe something to think about after Lean 4 comes out...

#### Rob Lewis (Sep 29 2020 at 12:31):

This was merged, dunno how long it takes to go live though

#### Bhavik Mehta (Sep 29 2020 at 17:56):

wait zulip has a dark mode!

#### Johan Commelin (Sep 29 2020 at 18:01):

been usin' it for ages (-;

#### Floris van Doorn (Sep 29 2020 at 21:57):

Bhavik Mehta said:

wait zulip has a dark mode!

Zulip has light mode? I always forget which websites I had to manually set to dark mode, and which come like that by default :)

#### Adam Topaz (Sep 29 2020 at 21:59):

At this point in my life, if it doesn't have dark mode, I don't use it.
For example, put this at the preamble of your latex files:

\usepackage{xcolor}
\pagecolor[rgb]{0.0,0.0,0.0}
\color[rgb]{0.2,1.0,0.2}


#### Floris van Doorn (Sep 29 2020 at 22:14):

I just noticed that Wikipedia has dark mode, but formulas are still written in black font: https://wikidark.org/wiki/Cauchy_condensation_test. Does Wikipedia have a better dark mode?

#### Adam Topaz (Sep 29 2020 at 22:16):

I guess I was slightly exaggerating...

:)

#### Adam Topaz (Sep 29 2020 at 22:18):

I remember seeing some chrome and/or firefox extensions that change the CSS to make everything dark mode. Never used them though.

#### Adam Topaz (Sep 29 2020 at 22:18):

And of course this doesn't help with the formulas on wikipedia, since they use images as opposed to something like mathjax.

#### Bhavik Mehta (Sep 30 2020 at 00:43):

Yeah I'm usually dark-mode-only (including latex) but for some reason I never thought to change it for zulip

#### Adam Topaz (Sep 30 2020 at 01:53):

That latex code will make your PDF dark-mode :wink:

#### Johan Commelin (Sep 30 2020 at 04:21):

I typically invert colors in my PDF reader, so that my LaTeX code also works for people that have joined the light side...

#### Adam Topaz (Sep 30 2020 at 04:35):

Oh, what PDF reader is this? I typically use zathura, does it have such an option?

#### Adam Topaz (Sep 30 2020 at 04:37):

Whoa, zathura does have this! And it's just a matter of pressing C-r

#### Johan Commelin (Sep 30 2020 at 06:03):

@Adam Topaz It's the little things, right? :grinning_face_with_smiling_eyes:

#### Johan Commelin (Sep 30 2020 at 06:03):

mupdf also has this, I use both

#### Rob Lewis (Oct 01 2020 at 18:55):

Rob Lewis said:

The five major programming languages: Rust, Python2, Python3, Julia, and Lean

The two major research topics: Category Theory and the Lean Theorem Prover

#### Kevin Buzzard (Oct 01 2020 at 19:55):

Oh that's wonderful that they mention us on their site. I want "Lean" to be this cool weird thing that people have heard of and even if they don't really know what it is, they know it's there.

#### Bryan Gin-ge Chen (Oct 11 2020 at 00:57):

Rob Lewis said:

This was merged, dunno how long it takes to go live though
https://user-images.githubusercontent.com/30312566/94343448-efb7d100-0035-11eb-96dd-f1b7844f35a6.gif

Just noticed that this is live now, try hovering over the snippet below and looking at the icon in the top-right corner:

import data.set.finite
example : ({1,2,3} : set ℕ).to_finset.card = 3 := rfl


#### Kevin Buzzard (Oct 15 2020 at 10:36):

I am offered two links -- one to playground (leanprover.github.io, the old MS site) and one to community playground. The former doesn't work for me -- it ends up mangled as

import data.set.finite
example %3A ({1%2C2%2C3} %3A set ℕ).to_finset.card %3D 3 %3A%3D rfl


#### Kevin Buzzard (Oct 15 2020 at 10:37):

Suggested fix: just remove the link to the 3.4.2 playground completely? We'll only get people clicking on it and complaining that ring doesn't work (or any other tactic added in the last two years)

Last updated: May 08 2021 at 22:13 UTC