Layout graph from proof

[nomeata]

With the new Schieblehre blocks, it is possible to lay out proofs so that all edges go from left to right. With this in mind, is it realistic to automatically layout a proof? Doesn’t have to be perfect, but would be useful to clean up completely messy proofs, or to be able to load proofs into the UI.

So the task here would be to turn a proof object into a graph, assigning position to the cells, and for those Schieblehre blocks, the width. I guess the code would be realtively hackish, as it would have to “know” what proof elements can be shown as a Schieblehre etc..

[nomeata]

This would solve the ITP reviewers suggestion:

You can do a better job of displaying the proofs. I know it requires a lot of engineering, but it is easy when playing the game for connections to overlap, which makes it harder to understand how blocks are connected.

[mikeshulman]

I would really like it if all edges always went from left to right. In fact, I would like it if the UI only allowed you to draw edges that go from left to right. This is particularly true for "hypothesis" edges coming from →I and ∨E: I worry that when my students pull those edges back to go into some other block way to the left, they haven't fully internalized the idea that the hypothesis is only available "within" the sub-proof. In line with that, it would also be really nice if the stretchy →I and ∨E blocks automatically resized to include everything "inside" them.

[nomeata]

If the underlying JointJS library might allow that somehow, then it's plausible?

Back then I intentionally didn't forbid all bad wirings, to allow experimentation. But I'm not saying that that was the right didactic choice :-)