[backport v4.32.0] feat: use ProofWidgets graphviz widget

[Vtec234]

Summary

Backport #425 to v4.32.0.

Primary Review

• Primary review: feat: use ProofWidgets graphviz widget #425
• Keep review comments on feat: use ProofWidgets graphviz widget #425 unless this backport diverges materially.

Scope

• Backport the already-reviewed default-development change onto v4.32.0.
• Keep this PR limited to release-line-specific conflict resolution.
• Preserve one-to-one commit provenance with cherry-pick -x.

Backport Delta

• No intentional release-specific changes.
• If conflict resolution requires deviations from the default-development PR, describe them here.

[ejgallego]

Thanks a lot!

I am still consolidating some relevant code, I think we should be able to land this hopefully in the next couple of days.

[ejgallego]

Hi @Vtec234, thanks for the PR. I played around with it a little. A few comments:

• It seems to me that the PR needs to be rebased onto a 4.32 branch, as the upstream ProofWidgets code will force the 4.32 toolchain. I have now added a 4.32 branch to Verso Blueprint, and the dependent PR has been merged, so maybe it would be good to rebase?
• I think the ForceWidget.lean file is stale, right?

My main question is about how to store the info-tree data for Blueprint- and Verso-specific information.

Before this commit deactivated it, I was using Widget.savePanelWidgetInfo during elaboration to signal: “here is a blueprint syntax piece; activate a preview.”

This was used, for example, to allow previews when clicking on pieces of data such as {uses "foo"}[...].

I see you are indeed using a custom Verso Blueprint infotree data. What should be the way forward here? Should we keep the Blueprint-specific Data.NodeInfo and extend it to cover other cases?

Second: now that the widget has seen some much-needed love, I would like to reactivate the preview. How should we approach the UI aspect? Do you have any ideas or suggestions? Thanks!

[Vtec234]

maybe it would be good to rebase?

Done!

I think the ForceWidget.lean file is stale, right?

Yes, the PR description had a note about this before you (or AI) removed it :P I deleted the file.

Should we keep the Blueprint-specific Data.NodeInfo and extend it to cover other cases?

Using info nodes for blueprint nodes and info nodes for the widget itself has different purposes. The latter tells the system 'display this widget at this position', whereas the former is something we can use internally to recognize where the blueprint nodes are. I removed the latter in favor of a widget that is always shown, with the idea that to navigate around you do want it to always show up. What other cases do you have in mind?

I would like to reactivate the preview. How should we approach the UI aspect?

Do you mean the theorem/statement content preview? If so, I intentionally didn't add that for now in order not to overload the UI with information. One thing we could have is another widget that previews the current node (i.e., the one the cursor is on). This wouldn't help preview other nodes, but maybe that's fine? If we do want to preview other nodes, a decent UI might be to show the preview below the graph always. This is because the infoview is quite vertical, so there tends to be available space there.

[ejgallego]

Yes, the PR description had a note about this before you (or AI) removed it :P I deleted the file.

Indeed; sorry for the churn here. It was interesting what happened: the harness went sideways because of a corner case that I hadn't anticipated.

My order to Codex was "rebase and build PR#193 locally with full artifacts", which I often do for testing with the large reference blueprints interactively.

However, the PR was pulling a recent proofwidgets version, which bumped the global toolchain to 4.32. This won't work in our setting, the reference blueprints at the time required 4.31. Codex went into a hole backporting the widget code to 4.31, etc... It was way too eager, and created a mess.

When I realized, I restored PR state manually, but forgot to fully revert the PR description.

Of course, Codex wanted to add more harness code to detect this situation in the future (lake bumps effective toolchain via a dep), but I refused, enough harness inflation already! :D

Should we keep the Blueprint-specific Data.NodeInfo and extend it to cover other cases?

Using info nodes for blueprint nodes and info nodes for the widget itself has different purposes. The latter tells the system 'display this widget at this position', whereas the former is something we can use internally to recognize where the blueprint nodes are. I removed the latter in favor of a widget that is always shown, with the idea that to navigate around you do want it to always show up. What other cases do you have in mind?

The main case I was thinking of is showing a preview of a lemma when you are around {uses "foo"}[].

Do you mean the theorem/statement content preview? If so, I intentionally didn't add that for now in order not to overload the UI with information. One thing we could have is another widget that previews the current node (i.e., the one the cursor is on). This wouldn't help preview other nodes, but maybe that's fine? If we do want to preview other nodes, a decent UI might be to show the preview below the graph always. This is because the infoview is quite vertical, so there tends to be available space there.

Indeed, this is exactly what I was thinking. I'll try to cook a vertical space below the widget. Do we have all the required web components already in ProofWidgets, or do you think we should add some more for this use case.

[ejgallego]

Great stuff, thanks a lot!

I'll rebase on top of 4.33 branch, backport (using Codex, which should be the identity) and merge.