From 6ed55785c94e15fa953d93aff513d4600eaa3cd5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 30 Aug 2026 17:46:02 +0200 Subject: [PATCH] perf: compact generated Blueprint payloads (cherry picked from commit a67330a36dfc42b53aeaa4401251bdbbf40220dd) --- lakefile.lean | 1 + src/VersoBlueprint/Commands/Graph.lean | 5 ++- .../Commands/SerializedExtension.lean | 39 +++++++++++++++++++ src/VersoBlueprint/Commands/Summary.lean | 3 +- src/VersoBlueprint/Commands/Summary/Data.lean | 32 +++++++-------- .../SerializedExtension.lean | 30 ++++++++++++++ 6 files changed, 91 insertions(+), 19 deletions(-) create mode 100644 src/VersoBlueprint/Commands/SerializedExtension.lean create mode 100644 tests/VersoBlueprintTests/SerializedExtension.lean diff --git a/lakefile.lean b/lakefile.lean index a394de17..3c0e07b9 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -75,6 +75,7 @@ lean_lib VersoBlueprintTests where `VersoBlueprintTests.BlueprintExternalMarkup, `VersoBlueprintTests.ExternalDeclRender, `VersoBlueprintTests.RuntimeCache, + `VersoBlueprintTests.SerializedExtension, `VersoBlueprintTests.TestBlueprintRegistryMeta, `VersoBlueprintTests.TestBlueprintRegistryChecks, `VersoBlueprintTests.TestBlueprintRegistryCoverage, diff --git a/src/VersoBlueprint/Commands/Graph.lean b/src/VersoBlueprint/Commands/Graph.lean index 1ae49971..a767d18d 100644 --- a/src/VersoBlueprint/Commands/Graph.lean +++ b/src/VersoBlueprint/Commands/Graph.lean @@ -8,6 +8,7 @@ import Lean import Verso import VersoManual import VersoBlueprint.Commands.Common +import VersoBlueprint.Commands.SerializedExtension import VersoBlueprint.Environment import VersoBlueprint.Graph import VersoBlueprint.GraphApi @@ -51,7 +52,7 @@ structure GraphBlockData where options : GraphOptions := {} previewMode : Informal.HoverRender.PreviewMode := .pinned previewPlacement : Informal.HoverRender.PreviewPlacement := .docked -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson def parseGraphPreviewMode? (s : String) : Option Informal.HoverRender.PreviewMode := match s.trimAscii.toString.toLower with @@ -474,7 +475,7 @@ def mkGraphPart (stx : Syntax) (endPos : String.Pos.Raw) (options : GraphOptions if verso.blueprint.debug.commands.get (← Lean.getOptions) then logInfo m!"Adding {graphModel.nodes.size} graph nodes" let graphData : GraphBlockData := { graphModel, options, previewMode, previewPlacement } - let block ← ``(Verso.Doc.Block.other (Informal.Commands.Block.graph $(quote graphData)) #[]) + let block ← serializedBlockTerm `Informal.Commands.Block.graph graphData let subParts := #[] pure <| FinishedPart.mk stx stx expandedTitle titlePreview metadata #[block] subParts endPos diff --git a/src/VersoBlueprint/Commands/SerializedExtension.lean b/src/VersoBlueprint/Commands/SerializedExtension.lean new file mode 100644 index 00000000..f7c0e54f --- /dev/null +++ b/src/VersoBlueprint/Commands/SerializedExtension.lean @@ -0,0 +1,39 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import Lean.Data.Json.Parser +import Verso.Doc.Elab +import VersoManual.Basic + +namespace Informal.Commands + +open Lean + +/-- +Construct a Manual block from extension data serialized while elaborating a document command. + +Keeping a large computed payload in a string literal avoids generating and then re-elaborating an +equivalent constructor-sized Lean term. This is an internal document-construction helper, not a +persisted VBP artifact format. +-/ +def blockFromJsonString! (name : Name) (serialized : String) : Verso.Genre.Manual.Block := + let data := + match Json.parse serialized with + | .ok data => data + | .error error => panic! s!"invalid serialized Blueprint extension data: {error}" + { name, data } + +/-- +Serialize extension data into a compact string literal and reconstruct its Manual block when the +generated document term is evaluated. +-/ +def serializedBlockTerm [ToJson α] (name : Name) (data : α) : + Verso.Doc.Elab.PartElabM (TSyntax `term) := do + let serialized := (toJson data).compress + ``(Verso.Doc.Block.other + (Informal.Commands.blockFromJsonString! $(quote name) $(quote serialized)) #[]) + +end Informal.Commands diff --git a/src/VersoBlueprint/Commands/Summary.lean b/src/VersoBlueprint/Commands/Summary.lean index 4821c35b..8396132b 100644 --- a/src/VersoBlueprint/Commands/Summary.lean +++ b/src/VersoBlueprint/Commands/Summary.lean @@ -9,6 +9,7 @@ import Lean.Elab.Command import Verso import VersoManual import VersoBlueprint.Commands.Common +import VersoBlueprint.Commands.SerializedExtension import VersoBlueprint.Commands.Summary.Collect import VersoBlueprint.Commands.Summary.Render @@ -26,7 +27,7 @@ def mkSummaryPart (stx : Syntax) (endPos : String.Pos.Raw) : PartElabM FinishedP let summary ← buildSummary if verso.blueprint.debug.commands.get (← Lean.getOptions) then logInfo m!"Blueprint summary for {summary.totalEntries} entries" - let block ← ``(Verso.Doc.Block.other (Informal.Commands.Block.summary $(quote summary)) #[]) + let block ← serializedBlockTerm `Informal.Commands.Block.summary summary let subParts := #[] pure <| FinishedPart.mk stx stx expandedTitle titlePreview metadata #[block] subParts endPos diff --git a/src/VersoBlueprint/Commands/Summary/Data.lean b/src/VersoBlueprint/Commands/Summary/Data.lean index e2b37051..76012077 100644 --- a/src/VersoBlueprint/Commands/Summary/Data.lean +++ b/src/VersoBlueprint/Commands/Summary/Data.lean @@ -18,14 +18,14 @@ structure SorryItem where decl : Name isTheorem : Bool := false status : Data.ProvedStatus := .proved -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure MissingLeanDeclItem where label : Name kind : String written : Name canonical : Name -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure RenderFailureItem where label : Name @@ -33,13 +33,13 @@ structure RenderFailureItem where written : Name canonical : Name message : String -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure IndexItem where label : Name kind : String leanObjects : List Name := [] -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson abbrev PendingInformalItem := IndexItem @@ -47,14 +47,14 @@ structure ParentTheoremGroup where parent : Name header : String := "" entries : List IndexItem := [] -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure EntryStatusCounts where completed : Nat := 0 completedDepsNo : Nat := 0 withSorries : Nat := 0 noProof : Nat := 0 -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure PriorityItem where label : Name @@ -70,7 +70,7 @@ structure PriorityItem where directUses : Nat := 0 downstreamUses : Nat := 0 leanObjects : List Name := [] -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure UsageItem where label : Name @@ -80,7 +80,7 @@ structure UsageItem where directUses : Nat := 0 downstreamUses : Nat := 0 leanObjects : List Name := [] -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure GroupHealthItem where parent : Name @@ -93,14 +93,14 @@ structure GroupHealthItem where incompleteLeanEntries : Nat := 0 unlockScore : Nat := 0 nextPriority? : Option PriorityItem := none -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure CoverageSplit where readyToFormalize : Nat := 0 formalizedWithoutAncestors : Nat := 0 fullyClosed : Nat := 0 blockedOrIncomplete : Nat := 0 -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure DependencyLoadItem where label : Name @@ -111,7 +111,7 @@ structure DependencyLoadItem where directUses : Nat := 0 downstreamUses : Nat := 0 leanObjects : List Name := [] -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure DebtHotspotItem where parent : Name @@ -120,7 +120,7 @@ structure DebtHotspotItem where incompleteDecls : Nat := 0 missingDecls : Nat := 0 totalDebt : Nat := 0 -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure OwnerRollupItem where owner : Name @@ -129,7 +129,7 @@ structure OwnerRollupItem where actionableEntries : Nat := 0 quickWins : Nat := 0 linkedPrs : Nat := 0 -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure TagRollupItem where tag : String @@ -137,7 +137,7 @@ structure TagRollupItem where actionableEntries : Nat := 0 quickWins : Nat := 0 linkedPrs : Nat := 0 -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure MetadataEntryItem where label : Name @@ -148,7 +148,7 @@ structure MetadataEntryItem where prUrl : Option String := none tags : List String := [] leanObjects : List Name := [] -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson structure Summary where showDebugDiagnostics : Bool := false @@ -193,6 +193,6 @@ structure Summary where missingOwners : List MetadataEntryItem := [] missingEffort : List MetadataEntryItem := [] untaggedEntries : List MetadataEntryItem := [] -deriving Inhabited, FromJson, ToJson, Quote +deriving Inhabited, FromJson, ToJson end Informal.Commands diff --git a/tests/VersoBlueprintTests/SerializedExtension.lean b/tests/VersoBlueprintTests/SerializedExtension.lean new file mode 100644 index 00000000..379369d4 --- /dev/null +++ b/tests/VersoBlueprintTests/SerializedExtension.lean @@ -0,0 +1,30 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import VersoBlueprint.Commands.Graph +import VersoBlueprint.Commands.Summary + +namespace Verso.VersoBlueprintTests.SerializedExtension + +/-- info: true -/ +#guard_msgs in +#eval + let graphData : Informal.Commands.GraphBlockData := default + let direct := Informal.Commands.Block.graph graphData + let serialized := Informal.Commands.blockFromJsonString! + `Informal.Commands.Block.graph (Lean.toJson graphData).compress + direct.name == serialized.name && direct.data.compress == serialized.data.compress + +/-- info: true -/ +#guard_msgs in +#eval + let summary : Informal.Commands.Summary := { totalEntries := 3, theorems := 2 } + let direct := Informal.Commands.Block.summary summary + let serialized := Informal.Commands.blockFromJsonString! + `Informal.Commands.Block.summary (Lean.toJson summary).compress + direct.name == serialized.name && direct.data.compress == serialized.data.compress + +end Verso.VersoBlueprintTests.SerializedExtension