understanding blueprint colourscheme

[kbuzzard]

This code

\begin{lemma}
    \label{ZHat.e_not_in_Int}
    \lean{ZHat.e_not_in_Int}
    \uses{ZHat.e}
    \leanok
    The element $(e_N)_N$ of $\Zhat$ is not in $\Z$.
\end{lemma}
\begin{proof}\notready
    I don't have a proof of this but it doesn't look too bad; maybe I'm wrong
    and it's hard? We will not need it later on.
\end{proof}

produces (on FLT) an oval with a green border (fine) but a blue interior. I want that interior to be orange or red or something.

In fact there seem to be two kinds of \notready proofs -- one is "I didn't write the LaTeX yet, feel free to write it for me" and the other is "this is a multi-year project, please see the discussion link".
Maybe I want \needsLaTeX to be orange, and \noplans to be grey?

Can I also edit the legend to explain my personal colour system?

[pitmonticone]

Hi @kbuzzard,

I want that interior to be orange or red or something.

This is the current (default) colour scheme:

1. Statement Status
   • Blue border: The statement of the result is ready to be formalized; all prerequisites are complete.
   • Orange border: The statement of the result is not ready to be formalised; additional work is required on the blueprint.
   • Green border: The statement of the result has been formalised.
2. Proof Status
   • Blue background: The proof of the result is ready to be formalised; all prerequisites are complete.
   • Green background: The proof of the result has been formalised.
   • Dark green background: The proof of the result and all its ancestors have been formalized.

We can change this scheme very easily. If I understand you correctly, you want to change the Blue background into an Orange / Red background, right? Please notice that this choice might be a bit unfortunate since Orange is associated with \notready when placed in the statement environment.

In fact there seem to be two kinds of \notready proofs -- one is "I didn't write the LaTeX yet, feel free to write it for me" and the other is "this is a multi-year project, please see the discussion link". Maybe I want \needsLaTeX to be orange, and \noplans to be grey?

First of all, \notready is not supposed to be inserted in the proof environment, but in the statement one: \notready claims that the surrounding statement environment is not ready to be formalized, typically because it requires more blueprint work. For more details you can see the implementation here.

If you want to change this, it's going to be a bit trickier because it requires changes upstream (i.e. in the LeanBlueprint library).

Can I also edit the legend to explain my personal colour system?

I can make it explicit in the web.tex preamble so that you can change the colours as you like, but to add new status commands and change the legend we need to modify the implementation upstream (here and here).

[pitmonticone]

claim

[pitmonticone]

propose #261