Links to code snippets

Stream: Zulip meta

[Mario Carneiro]

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]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Kevin Buzzard]

That'll do for now!

[Bryan Gin-ge Chen]

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]

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

[Rob Lewis]

[Bhavik Mehta]

wait zulip has a dark mode!

[Johan Commelin]

been usin' it for ages (-;

[Floris van Doorn]

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]

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]

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]

I guess I was slightly exaggerating...

[Floris van Doorn]

:)

[Adam Topaz]

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

[Adam Topaz]

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

[Bhavik Mehta]

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

[Adam Topaz]

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

[Johan Commelin]

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]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Johan Commelin]

mupdf also has this, I use both

[Rob Lewis]

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]

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]

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]

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]

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)