Skip to content

feat: deeply compare diagnostics and simplify build orchestration#786

Open
Vtec234 wants to merge 3 commits into
masterfrom
diag-deps
Open

feat: deeply compare diagnostics and simplify build orchestration#786
Vtec234 wants to merge 3 commits into
masterfrom
diag-deps

Conversation

@Vtec234

@Vtec234 Vtec234 commented Jun 12, 2026

Copy link
Copy Markdown
Member

This PR reduces infoview re-renders (1.) and simplifies the build setup (2.) Fixes leanprover-community/ProofWidgets4#176.

  1. InfoAux fetches goals and widgets whenever the Object.is-identity of lspDiagsHere changes. The React effect that sets lspDiagsHere tries to maintain its identity, but it used to do so by comparing LeanDiagnostics for ===-identity. We now use react-fast-compare-identity. We do not try to memoize earlier in the data flow (e.g. when setting LspDiagnosticsContext) in any principled way.

    The ===-comparison was never correct - fresh diagnostic objects are created on every publishDiagnostics - but the issue was primarily exposed by feat: 'unsolved goals' & 'goals accomplished' diagnostics lean4#7366 which produces a hidden diagnostic on every declaration, so that lspDiagsHere is recomputed at most positions.

  2. We remove Lerna, leaving only Nx (which Lerna uses under the hood). This unbreaks building in a worktree folder nested within the main repo folder (vscode-lean4/worktree-my-branch/). This also drops ~400 transitive dependencies and should otherwise be functionally equivalent.

@Vtec234 Vtec234 requested a review from mhuisi June 12, 2026 20:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Panel widgets are refreshed when the orange bar progresses

1 participant