Blueprint colors

Stream: PrimeNumberTheorem+

[Ian Jauslin]

Hi all!
@Alex Kontorovich and I have been discussing changing the color scheme for the dependency graph, to make the 'todo's a more different color from the 'done's. I through something together on a fork of PNT+: https://ianjauslin-rutgers.github.io/PrimeNumberTheoremAnd/web/dep_graph_document.html
Does anyone have any suggestions?

[Ian Jauslin]

I also made another change: definitions that are yet to be formalized have the 'todo' background, instead of the 'todo' border with the 'done' background.

[Yaël Dillies]

What do you mean by "todo border and done background"? That should never happen

[Ian Jauslin]

It does happen. My understanding of the philosophy, is that blueprint considers that definitions always have correct proofs, because there is no need for a proof. It can get confusing though, so I think it would be best to only color a proof as 'done' if it's been formalized.

[Yaël Dillies]

:thinking: I maintain that if this happens you have done something wrong. See in eg my blueprint that it never happens that you have a green background and a blue border.

[Alex Kontorovich]

No no, we're talking about changing the color scheme. The idea is that Green looks like something is done, and it's hard to see the border without squinting (especially blue to green!). So definitions that aren't formalized look like they are. So we're discussing changing the convention.

[Ian Jauslin]

I think @Yaël Dillies is talking about the change that I made so that definitions don't show with a background of 'done' when they haven't been formalized yet.

[Ian Jauslin]

That does happen though. Here's an example:

\documentclass{report}

\usepackage[showmore, dep_graph, coverage, project=../../]{blueprint}

\usepackage{amsmath, amsthm}

\theoremstyle{definition}
\newtheorem{definition}{Definition}

\begin{document}

\begin{definition}
test
\end{definition}

\end{document}

[Alex Kontorovich]

Oh I think I'm starting to see. Do we have \leanoks on definitions that aren't formalized, is that what's wrong...?

[Alex Kontorovich]

Ah

[Ian Jauslin]

In @Yaël Dillies 's blueprint, all the definitions have been formalized, so there's no problem.

[Yaël Dillies]

You must have changed something to the blueprint, because I swear definitions always have the same background and border in my blueprints.

[Ian Jauslin]

I am running the code that I pasted above with the latest commit of blueprint. No modifications.

[Ian Jauslin]

If I run the following, (I just added a label to the definition):

\documentclass{report}

\usepackage[showmore, dep_graph, coverage, project=../../]{blueprint}

\usepackage{amsmath, amsthm}

\theoremstyle{definition}
\newtheorem{definition}{Definition}

\begin{document}

\begin{definition}
\label{test}\lean{test}
test
\end{definition}

\end{document}

I get this:
test.png

edit: without adding the label, I get the same thing, but with a random name instead of 'test'

[Yaël Dillies]

That definitely didn't happen before. @Patrick Massot, did you accidentally change the background of definitions to always be green?

[Alex Kontorovich]

regardless of how it used to work, what do people think of our proposal for how it could look in the future?

[Ian Jauslin]

Specifically, I am interested in what you think of the colors.

[Yaël Dillies]

They are a bit confusable for deuteranomals like me

[Ian Jauslin]

That's exactly what I was worried about. How about switching orange to purple (which has some blue in it)

[Alex Kontorovich]

Exactly! We're trying to make it more colorblind friendly!...

[Alex Kontorovich]

But Ian, how come, e.g., RectangleIntegral, which is a definition marked with \leanok, showing up light green instead of dark green...?

[Yaël Dillies]

A trick to make things colorblind-friendly is to have different fillings. cf the Discord status badges.

[Ian Jauslin]

Let me have a look at this. This'll have to be a graphviz feature to integrate easily into blueprint.

[Alex Kontorovich]

I notice that zulip's colors for active vs idle users is green and orange!...

[Yaël Dillies]

With different fillings!
image.png

[Alex Kontorovich]

Indeed... might be too hard to change that in blueprint...?

[Ian Jauslin]

I don't think it will be hard. graphviz has a "striped" feature for filling. I think I can spin this up quickly.

[Ian Jauslin]

@Alex Kontorovich : Do you have a preference between stripes or a color gradient?

[Alex Kontorovich]

hmm can we do an AB test?

[Ian Jauslin]

Alright! I've switched the 'todo' background color to a gradient, and the 'todo' boundary to a dashed line. How does this look: https://ianjauslin-rutgers.github.io/PrimeNumberTheoremAnd/web/dep_graph_document.html

[Yaël Dillies]

It's a bit jarring. How does it look if you replace the gradient by stripes or by half-filling (in the style of the Zulip AFK badge)?

[Yaël Dillies]

Also worth making sure that the dashes are different between arrows and borders since they mean different things

[Ian Jauslin]

I can easily do a horizontal half filling, but then the text is not so easy to read. So I think a vertical half-filling would be best, but that takes a little more work.

Ah yes, I forgot about the dashes on the arrows. I will dot the boundaries instead of dashing them

[Ian Jauslin]

Well, it seems like rotating the stripes is annoying. Si here are my two options: gradient:
gradient.png
or stripes:
hard.png

[Yaël Dillies]

I like the vertical halves best, followed by the horizontal halves

[Terence Tao]

Gradient looks better, though tbh I would also be happy with a solid color. Dotted line looks good (though I don't really understand the distinction between a dotted line boundary and a black boundary, but presumably whatever legend one has for the blueprint will clarify this).

[Ian Jauslin]

The black boundary occurs when the blueprint has no links to lean code. Ideally, the blueprint should be written in such a way to avoid this.

[Patrick Massot]

Yaël Dillies said:

That definitely didn't happen before. Patrick Massot, did you accidentally change the background of definitions to always be green?

There was no recent change to colors. However it may be broken since January 5th when I did change some color stuff. In that case you can open an issue with a mwe.

[Ian Jauslin]

I have a fix on my fork, I will make a usable PR when I have some time tomorrow.

[Patrick Massot]

Why do you have a fork?

[Ian Jauslin]

So I can modify the code to suit my purposes. (I'm not sure I understand the question.)

[Patrick Massot]

I don't understand why you do that instead of contributing to the upstream version so that everyone can benefit from improvements.

[Yaël Dillies]

because it's work in progress?

[Patrick Massot]

If your modifications are unlikely to be wanted by anyone else then you can ask for more options.

[Johan Commelin]

I think Ian Jauslin meant "fork" in the Github sense, so basically "personal clone". And not "fork" in the traditional, I'm going my way and not yours and the community will have to choose between two versions.

[Alex Kontorovich]

Terence Tao said:

Gradient looks better, though tbh I would also be happy with a solid color. Dotted line looks good (though I don't really understand the distinction between a dotted line boundary and a black boundary, but presumably whatever legend one has for the blueprint will clarify this).

I agree, I like the left to right gradient better than horizontal line down the middle of the lemma name. I would also be perfectly happy with a solid color, but see the benefit of giving it a gradient if it'll help the colorblind...

[Ian Jauslin]

Yes, I meant a github fork of the repo where I can play around with the code. I'm not trying to spin off leanblueprint, just figuring out the best way for me to contribute.

At the moment, I modified the hardcoded colorscheme, which I don't think is something I want to distribute to the community. When I have a bit of time, I would like to set things up so the colors can be adjusted from the configuration file. When I do that, I'll PR it to the main repo.

[Ian Jauslin]

Incidentally, @Patrick Massot , leanblueprint still doesn't have a license. I think this could become a problem in the long run. (I would feel much more comfortable contributing to a project which is clearly marked as Free Software.)

[Patrick Massot]

Ian Jauslin said:

Yes, I meant a github fork of the repo where I can play around with the code. I'm not trying to spin off leanblueprint, just figuring out the best way for me to contribute.

At the moment, I modified the hardcoded colorscheme, which I don't think is something I want to distribute to the community. When I have a bit of time, I would like to set things up so the colors can be adjusted from the configuration file. When I do that, I'll PR it to the main repo.

What do you mean by “harcoded colorscheme”? Nothing is hardcoded here. You can modify colors from the TeX file.

[Ian Jauslin]

Ah, good. How does one do this?

[Patrick Massot]

Or maybe I stopped halfway through this refactor because of Christmas...

[Patrick Massot]

Indeed in the code I see everything is ready but the LaTeX macros don’t exist. This will be very easy to fix.

[Ian Jauslin]

Great! Looking forward to it being done.

[Patrick Massot]

I added license files (in the client branch that will hopefully soon be merged to master).