Feature requests for more types of nodes and their behavior

utensil commented 7 months ago

Red node 🟥

Requested by @kbuzzard .

I would like to be able to make red nodes, which in the old days would show up as blue but were actually huge projects all disguised as one node. A red node means that LaTeX needs to be written and the node needs to be broken up into smaller nodes, and I want blue to mean "this node is ready to be tackled as a reasonable project, there is a either a clear citation or a good explanation in the LaTeX".

For the legend: I think I want red border to mean "the statement of this result needs to be broken down into smaller formalizable pieces; prerequisites may or may not be ready.

I want (theorems stated in Lean) to be green border and red "not ready to be worked on; waiting for Kevin" interior (as their proofs are not sorted out in blueprint).

This is now partially implemented by a maker named \tangled (for now) in my prototype.

More green node 🟢

Requested by @teorth on Zulip.

I wonder if there is a way to add an additional coloring to the dependency graph (maybe some sort of "really green") that indicates not only that a node has been locally formalized, but that all of the nodes it depends on transitively are also formalized? Right now for instance we are adding a few extensions to the PFR project, which has temporarily uglified our dependency graph, but it would be nice to tell at a glance that the original result PFR is still completely proven (or at least, that blueprint thinks that it is).

Not implemented yet, just filed this issue for follow up.

Feature requests that can be fulfilled using current implementation

Requested by @kbuzzard .

These are subtle details, documenting them in the hope that they will still be there:

A definition and a theorem together in one node, with different prerequisites of the statement and the proof.

An example is that the definition and the theorem are stated in Lean, so

I want it to be green border 🟢 and blue interior 🟦 . All prerequisites are done, data in definition is done, we just need some proofs filled in.

The solution is:

a. put the definition and the theorem in \begin{theorem} block, mark it with \leanok b. put the proof sketch or an empty one in \begin{proof} block, mark it with some \uses, note that:

no \uses means not ready (white interior) ⚪
empty \uses{} means all ready (green interior) 🟢
\uses{A,B,C} depends on the readiness of A, B, and C (could be blue interior). 🟦
arrows of (prerequisites) of a node is the union of \uses in theorem and in proof, but the colors are determined separately, when all proof \uses are ready (at least stated), its interior turns blue, when all statement \uses are ready, its border turns blue.

utensil commented 7 months ago

Here comes reason 2 of the feature request:

I want definitions to be the same as theorems: green means done, blue means "there's an issue about this and it's possible for someone to do it" and red means "read the issue but basically it's not possible to work on this now"

To describe this more clearly, for the following LaTeX:

\begin{definition}[wait]
    \label{wait}
    \tangled
    \uses{welcome, not_done}
\end{definition}

\begin{definition}[welcome]
    \label{welcome}
    \uses{done, not_done}
\end{definition}

\begin{definition}[done]
    \label{done}
    \leanok
\end{definition}

\begin{definition}[not done]
    \label{not_done}
\end{definition}

\begin{theorem}[wait]
    \label{wait'}
    \tangled
    \uses{welcome', not_done'}
\end{theorem}
\begin{proof}
\end{proof}

\begin{theorem}[welcome]
    \label{welcome'}
    \uses{done'}
\end{theorem}
\begin{proof}
    \uses{done'}
\end{proof}

\begin{theorem}[not ready]
    \label{not_ready'}
    \uses{done', not_done'}
\end{theorem}
\begin{proof}
\end{proof}

\begin{theorem}[done]
    \label{done'}
    \leanok
\end{theorem}
\begin{proof}
    \leanok
\end{proof}

\begin{theorem}[not done]
    \label{not_done'}
\end{theorem}
\begin{proof}
\end{proof}

The dep graph would look like this:

The means for the convenience of the readers, they can see what actions they could take just by the color of the background. Also, the legend can be improved to use similar example dep graph and simple words instead of long descriptions like now.

A prototype is hacked in latest commits of https://github.com/utensil/leanblueprint/commits/lean4-only-dev/ and was used to generate the dep graph above.

PatrickMassot commented 2 months ago

Sorry I forgot about the existence of this issue. Almost all of this was completed a long time ago (and was already planned before this issue was opened). Let’s open separate issues for the little remaining bits if needed.

PatrickMassot / leanblueprint