Zulip Chat Archive

Stream: Zulip meta

Topic: Links to code snippets


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rob Lewis (Sep 10 2020 at 13:11):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 13:29):

That'll do for now!

view this post on Zulip 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...

view this post on Zulip Rob Lewis (Sep 29 2020 at 12:31):

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

view this post on Zulip Rob Lewis (Sep 29 2020 at 12:32):

view this post on Zulip Bhavik Mehta (Sep 29 2020 at 17:56):

wait zulip has a dark mode!

view this post on Zulip Johan Commelin (Sep 29 2020 at 18:01):

been usin' it for ages (-;

view this post on Zulip 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 :)

view this post on Zulip 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}

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Sep 29 2020 at 22:16):

I guess I was slightly exaggerating...

view this post on Zulip Floris van Doorn (Sep 29 2020 at 22:16):

:)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Sep 30 2020 at 01:53):

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

view this post on Zulip 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...

view this post on Zulip Adam Topaz (Sep 30 2020 at 04:35):

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

view this post on Zulip Adam Topaz (Sep 30 2020 at 04:37):

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

view this post on Zulip Johan Commelin (Sep 30 2020 at 06:03):

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

view this post on Zulip Johan Commelin (Sep 30 2020 at 06:03):

mupdf also has this, I use both

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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