[backport v4.33.0] perf: compact generated Blueprint payloads

lakefile.lean

@@ -75,6 +75,7 @@ lean_lib VersoBlueprintTests where
     `VersoBlueprintTests.BlueprintExternalMarkup,
     `VersoBlueprintTests.ExternalDeclRender,
     `VersoBlueprintTests.RuntimeCache,
+    `VersoBlueprintTests.SerializedExtension,
     `VersoBlueprintTests.TestBlueprintRegistryMeta,
     `VersoBlueprintTests.TestBlueprintRegistryChecks,
     `VersoBlueprintTests.TestBlueprintRegistryCoverage,

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
 

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

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
 

src/VersoBlueprint/Commands/Summary/Data.lean

@@ -18,43 +18,43 @@ 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
   kind : String
   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
 
 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,15 +129,15 @@ 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
   totalEntries : Nat := 0
   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

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