From 1275017cad316cdd3ec98afec4cc94e89c0f2a7d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 17 Jul 2026 10:31:31 +0200 Subject: [PATCH 1/2] feat: distinguish original-source identities (cherry picked from commit 9eedaa522c8df4bf89918c0f648c07b95b4086a3) --- README.md | 7 ++- doc/API.md | 4 +- doc/DESIGN_RATIONALE.md | 18 +++++- doc/MANUAL.md | 50 ++++++++++++++-- src/VersoBlueprint/Informal/Block/Render.lean | 58 +++++++++++++++---- src/VersoBlueprint/Source/Data.lean | 21 +++++-- src/VersoBlueprint/blueprint-api-types.mjs | 4 +- .../BlueprintExternalMarkup.lean | 2 +- .../BlueprintPreviewSchema.lean | 53 +++++++++++++---- .../VersoBlueprintTests/BlueprintSource.lean | 58 +++++++++++++++---- .../test_preview_runtime_regressions.py | 6 +- .../Chapters/CustomRenderClient.lean | 2 + 12 files changed, 238 insertions(+), 45 deletions(-) diff --git a/README.md b/README.md index 09cd42be..dbb307a2 100644 --- a/README.md +++ b/README.md @@ -258,6 +258,8 @@ source := { spans := #[ { page := "12" + anchor := "lem:addition-right-identity" + citation := "Lemma 2.1(1)" pdf := some { path := "source/pages/page-12.pdf" } } ] @@ -269,7 +271,10 @@ For every natural number $`n`, $`n + 0 = n`. ```` Current behavior: source provenance is exported in the Blueprint manifest as -`sourceDocuments` and per-entry `sources`, and kept hidden in rendered pages. +`sourceDocuments` and per-entry `sources`. A sourced node shows a compact chip; +when one source citation is available, the chip says, for example, +`source: Lemma 2.1(1)` rather than presenting the citation as Blueprint's own +generated number. Browser clients can resolve source-document ids with `loadSourceDocument`, load the complete catalog with `loadSourceDocuments`, or join entry source refs with declared documents using `resolveSourceMetadata` from `api/data.mjs` or diff --git a/doc/API.md b/doc/API.md index 829f9a82..082f15c1 100644 --- a/doc/API.md +++ b/doc/API.md @@ -1215,7 +1215,9 @@ a `reason` and `diagnosticHtml` suitable for insertion into the page. `resolveSourceMetadata` is data-only: it returns source metadata and failure reasons, but no rendered HTML. It also does not load source PDFs, extracted text, or page images; callers use the returned paths and spans in the source UI -they own. +they own. Each span may carry a source-native `anchor` (for example a TeX +`\label`) and a human-readable `citation` (for example `Lemma 2.1(1)`) in +addition to its optional page, text range, and PDF location. | Helper | Success shape | Failure shape | | --- | --- | --- | diff --git a/doc/DESIGN_RATIONALE.md b/doc/DESIGN_RATIONALE.md index 3411899e..7ecf6b32 100644 --- a/doc/DESIGN_RATIONALE.md +++ b/doc/DESIGN_RATIONALE.md @@ -1,6 +1,6 @@ # Blueprint Design Rationale -Last updated: 2026-06-20 +Last updated: 2026-07-17 This document records the current architecture boundaries and the reasons the Blueprint implementation is shaped the way it is. @@ -46,6 +46,22 @@ traversal/rendering pass answers "how do these objects sit inside this rendered site?" Rendering and UI layers are expected to project from those two stages rather than invent parallel sources of truth. +### Blueprint Identity and Original-Source Identity + +Blueprint labels and traversal-generated heading numbers identify nodes inside +the Blueprint site. They must remain independent of identities inherited from +an original TeX, PDF, or text source. A source span therefore records a stable +source-native `anchor` and a human-facing `citation` alongside physical page, +text, or PDF locations. For example, a node generated as `Lemma 2.2` can point +to `itm: ib-first` and display `source: Lemma 2.1(1)` without changing its graph +key, cross-references, or intrinsic numbering. + +The source anchor is machine identity; the citation is presentation. Neither is +reconstructed from visible prose, and neither is used as a substitute for the +Blueprint node label. This is particularly important for Blueprints generated +from TeX, where definitions or split list items may consume different +Blueprint counters than the source theorem environment. + ### Command Split Command modules are split by concern: diff --git a/doc/MANUAL.md b/doc/MANUAL.md index f49585db..a3d31f8d 100644 --- a/doc/MANUAL.md +++ b/doc/MANUAL.md @@ -646,6 +646,8 @@ source := { spans := #[ { page := "12" + anchor := "lem:addition-right-identity" + citation := "Lemma 2.1(1)" text := some { path := "source/pages/page-12.md" startLine := 41 @@ -667,8 +669,48 @@ For every natural number $`n`, $`n + 0 = n`. The generated manifest exports declared documents in `sourceDocuments` and each manifest entry's original-source refs in `entry.sources`. Normal generated node shells also show a compact source chip when source provenance is present; open -it to inspect the source document id, page summary, and recorded text/PDF span -details. +it to inspect the source document id, source-native anchor and citation, page +summary, and recorded text/PDF span details. + +`anchor` is a stable identifier in the original source, such as a TeX +`\label`; `citation` is the corresponding human-readable source identity, such +as `Lemma 2.1(1)` or `Equation (2.4)`. These fields do not replace the +Blueprint node's label or generated heading number. A node may therefore remain +`Lemma 2.2` in the Blueprint while its source chip explicitly reads +`source: Lemma 2.1(1)`. Keeping the identities separate avoids silently +changing graph keys, Blueprint references, or site-local numbering to imitate +the source document. + +For a text source such as the TeX input itself, omit `page` and use a source +anchor, a text line range, or both: + +````md +:::source_document "paper-tex" +%%% +title := "Representation Theory (TeX source)" +kind := .text +%%% +::: + +:::lemma_ "addition_right_identity" +%%% +source := { + document := "paper-tex" + spans := #[{ + anchor := "itm:addition-right-identity" + citation := "Lemma 2.1(1)" + text := some { + path := "paper.tex" + startLine := 439 + endLine := 440 + } + }] +} +%%% + +For every natural number $`n`, $`n + 0 = n`. +::: +```` Manifest clients should read `entry.sources`; there is no singular `entry.source` field. Lean code preview entries may contain multiple refs when @@ -684,8 +726,8 @@ read the complete catalog with `loadSourceDocuments`. Browser clients can call `resolveSourceMetadata` from `api/data.mjs` or `api/preview.mjs` to resolve source refs for a preview key, manifest entry, or -render result. The API returns structured source-document metadata and recorded -text/PDF spans. +render result. The API returns structured source-document metadata, source +identities, and text/PDF spans. Manifest entries also include `sourceLocation`, a lookup result for the authored Blueprint label/facet location or Lean declaration source. Browser clients that start from semantic names can call `resolveLabel`, or `resolveDeclaration` for diff --git a/src/VersoBlueprint/Informal/Block/Render.lean b/src/VersoBlueprint/Informal/Block/Render.lean index 4d4ccc1d..2b2b3590 100644 --- a/src/VersoBlueprint/Informal/Block/Render.lean +++ b/src/VersoBlueprint/Informal/Block/Render.lean @@ -372,8 +372,11 @@ private def sourceSpanPages (spans : Array Source.Span) : Array String := spans.foldl (init := #[]) fun pages span => - let page := span.page.trimAscii.toString - if page.isEmpty then pages else pushUniqueString pages page + match span.page with + | none => pages + | some rawPage => + let page := rawPage.trimAscii.toString + if page.isEmpty then pages else pushUniqueString pages page private def sourcePagesSummary (pages : Array String) : String := match pages.toList with @@ -395,9 +398,25 @@ private def sourcePdfSpanSummary (span : Source.PdfSpan) : String := | Option.none => s!"pdf {span.path}" private def sourceSpanSummary (span : Source.Span) : String := - let page := span.page.trimAscii.toString - let parts : Array String := - if page.isEmpty then #[] else #[s!"page {page}"] + let parts : Array String := #[] + let parts := + match span.citation with + | Option.some citation => + let citation := citation.trimAscii.toString + if citation.isEmpty then parts else parts.push s!"citation {citation}" + | Option.none => parts + let parts := + match span.anchor with + | Option.some anchor => + let anchor := anchor.trimAscii.toString + if anchor.isEmpty then parts else parts.push s!"anchor {anchor}" + | Option.none => parts + let parts := + match span.page with + | Option.some rawPage => + let page := rawPage.trimAscii.toString + if page.isEmpty then parts else parts.push s!"page {page}" + | Option.none => parts let parts := match span.text with | Option.some textRange => parts.push (sourceTextRangeSummary textRange) @@ -408,6 +427,22 @@ private def sourceSpanSummary (span : Source.Span) : String := | Option.none => parts String.intercalate "; " parts.toList +private def sourceSpanCitations (spans : Array Source.Span) : Array String := + spans.foldl + (init := #[]) + fun citations span => + match span.citation with + | none => citations + | some rawCitation => + let citation := rawCitation.trimAscii.toString + if citation.isEmpty then citations else pushUniqueString citations citation + +private def sourceRefsCitations (sourceRefs : Array Source.Ref) : Array String := + sourceRefs.foldl + (init := #[]) + fun citations sourceRef => + (sourceSpanCitations sourceRef.spans).foldl pushUniqueString citations + private def sourceRefSummary (sourceRef : Source.Ref) : String := let pages := sourceSpanPages sourceRef.spans let pageSummary := sourcePagesSummary pages @@ -425,10 +460,13 @@ private def sourceRefTitle (sourceRef : Source.Ref) : String := s!"Original source document {sourceRef.document}: {String.intercalate " | " spanSummary}" private def sourceRefsChipText (sourceRefs : Array Source.Ref) : String := - if sourceRefs.size == 1 then - "source 1" - else - s!"sources {sourceRefs.size}" + match sourceRefsCitations sourceRefs |>.toList with + | [citation] => s!"source: {citation}" + | _ => + if sourceRefs.size == 1 then + "source 1" + else + s!"sources {sourceRefs.size}" private def sourceRefsPanelTitle (sourceRefs : Array Source.Ref) : String := if sourceRefs.size == 1 then @@ -452,7 +490,7 @@ private def sourceRefsChipTitle (sourceRefs : Array Source.Ref) : String := private def sourceSpanPreviewText (span : Source.Span) : String := let summary := sourceSpanSummary span if summary.isEmpty then - "Source span recorded without page, text, or PDF location" + "Source span recorded without page, anchor, text, or PDF location" else summary diff --git a/src/VersoBlueprint/Source/Data.lean b/src/VersoBlueprint/Source/Data.lean index 69960207..6e43230b 100644 --- a/src/VersoBlueprint/Source/Data.lean +++ b/src/VersoBlueprint/Source/Data.lean @@ -70,7 +70,8 @@ def ValidationError.message : ValidationError → String | .pdfBoxInvalidYRange => "source PDF box yMin must be less than yMax" | .pdfBoxXMaxBeyondPageWidth => "source PDF box xMax must be within pageWidth" | .pdfBoxYMaxBeyondPageHeight => "source PDF box yMax must be within pageHeight" - | .spanMissingLocation => "source spans require text or PDF location data" + | .spanMissingLocation => + "source spans require a page, source anchor, text range, or PDF location" | .refMissingSpan => "source metadata must include at least one source span" instance : ToString ValidationError where @@ -160,14 +161,26 @@ def PdfSpan.validationErrors (span : PdfSpan) : Array ValidationError := /-- One source span attached to a Blueprint node. -/ structure Span where - page : String + /-- Optional source-local page identifier. Text sources do not need one. -/ + page : Option String := none + /-- Stable source-native identifier, such as a TeX `\label`. -/ + anchor : Option String := none + /-- Human-readable source-native reference, such as `Lemma 2.1(1)`. -/ + citation : Option String := none text : Option TextRange := none pdf : Option PdfSpan := none deriving Inhabited, Repr, BEq, DecidableEq, FromJson, ToJson, Quote def Span.validationErrors (span : Span) : Array ValidationError := - let errors := nonEmptyField "source span page" span.page - let errors := addIf errors (span.text.isNone && span.pdf.isNone) .spanMissingLocation + let errors : Array ValidationError := #[] + let errors := addOptional errors span.page (nonEmptyField "source span page") + let errors := addOptional errors span.anchor (nonEmptyField "source span anchor") + let errors := addOptional errors span.citation (nonEmptyField "source span citation") + let hasPage := span.page.any fun page => !page.trimAscii.isEmpty + let hasAnchor := span.anchor.any fun anchor => !anchor.trimAscii.isEmpty + let errors := addIf errors + (!hasPage && !hasAnchor && span.text.isNone && span.pdf.isNone) + .spanMissingLocation let errors := addOptional errors span.text TextRange.validationErrors addOptional errors span.pdf PdfSpan.validationErrors diff --git a/src/VersoBlueprint/blueprint-api-types.mjs b/src/VersoBlueprint/blueprint-api-types.mjs index a296450c..cf78f072 100644 --- a/src/VersoBlueprint/blueprint-api-types.mjs +++ b/src/VersoBlueprint/blueprint-api-types.mjs @@ -215,7 +215,9 @@ * One original source span attached to a Blueprint node. * * @typedef {Object} BlueprintSourceSpan - * @property {string} page Source-local page identifier. + * @property {string} [page] Optional source-local page identifier. + * @property {string} [anchor] Stable source-native identifier, such as a TeX `\\label`. + * @property {string} [citation] Human-readable source-native reference, such as `Lemma 2.1(1)`. * @property {BlueprintSourceTextRange} [text] Text location for this span. * @property {BlueprintSourcePdfSpan} [pdf] PDF/page-image location for this span. */ diff --git a/tests/VersoBlueprintTests/BlueprintExternalMarkup.lean b/tests/VersoBlueprintTests/BlueprintExternalMarkup.lean index 0c692f37..ede7e878 100644 --- a/tests/VersoBlueprintTests/BlueprintExternalMarkup.lean +++ b/tests/VersoBlueprintTests/BlueprintExternalMarkup.lean @@ -48,7 +48,7 @@ private def entryHasSourcePage (entry : Informal.PreviewManifest.Entry) (document page : String) : Bool := entry.sources.any fun sourceRef => sourceRef.document == document && - sourceRef.spans.any (fun span => span.page == page) + sourceRef.spans.any (fun span => span.page == some page) private def htmlHasSourcePreview (html document pageText : String) : Bool := hasSubstr html "bp_extra_slot_source" && diff --git a/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean b/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean index ef2e9efb..d82d43ad 100644 --- a/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean +++ b/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean @@ -31,10 +31,38 @@ open Informal.PreviewManifest fromJson? (α := Array String) requiredJson |>.toOption let some relatedEntrySchema := defs.get? "Informal.PreviewManifest.RelatedEntry" | return false let some graphNodeSchema := defs.get? "Informal.Graph.NodeData" | return false + let some sourceSpanSchema := defs.get? "Informal.Source.Span" | return false + let Except.ok sourceSpanPropsJson := Json.getObjVal? sourceSpanSchema "properties" | return false + let Except.ok sourceSpanProps := sourceSpanPropsJson.getObj? | return false + let sourceSpanRequired? := do + let requiredJson ← sourceSpanSchema.getObjVal? "required" |>.toOption + fromJson? (α := Array String) requiredJson |>.toOption let schemaText := schema.compress let stringSchemaHasMinLengthOne (schema : Json) : Bool := (schema.getObjValAs? String "type" |>.toOption) == some "string" && (schema.getObjValAs? Nat "minLength" |>.toOption) == some 1 + let stringSchema (schema : Json) : Bool := + (schema.getObjValAs? String "type" |>.toOption) == some "string" + let schemaHasStringNull (schema : Json) : Bool := + match Json.getObjVal? schema "anyOf" with + | Except.error _ => false + | Except.ok anyOfJson => + match anyOfJson.getArr? with + | Except.error _ => false + | Except.ok schemas => + schemas.any stringSchema && + schemas.any (fun (schema : Json) => + (schema.getObjValAs? String "type" |>.toOption) == some "null") + let schemaHasNonEmptyStringNull (schema : Json) : Bool := + match Json.getObjVal? schema "anyOf" with + | Except.error _ => false + | Except.ok anyOfJson => + match anyOfJson.getArr? with + | Except.error _ => false + | Except.ok schemas => + schemas.any stringSchemaHasMinLengthOne && + schemas.any (fun (schema : Json) => + (schema.getObjValAs? String "type" |>.toOption) == some "null") let previewKeySchemaHasNonEmptyStringNull (schema : Json) : Bool := match Json.getObjVal? schema "properties" with | Except.error _ => false @@ -44,16 +72,7 @@ open Informal.PreviewManifest | Except.ok props => match props.get? "previewKey" with | none => false - | some previewKeyJson => - match Json.getObjVal? previewKeyJson "anyOf" with - | Except.error _ => false - | Except.ok anyOfJson => - match anyOfJson.getArr? with - | Except.error _ => false - | Except.ok schemas => - schemas.any stringSchemaHasMinLengthOne && - schemas.any (fun (schema : Json) => - (schema.getObjValAs? String "type" |>.toOption) == some "null") + | some previewKeyJson => schemaHasNonEmptyStringNull previewKeyJson let internalSchemaDesc? := do let internalSchemaJson ← fileProps.get? "vbpInternalSchemaVersion" internalSchemaJson.getObjValAs? String "description" |>.toOption @@ -81,6 +100,7 @@ open Informal.PreviewManifest authoredLabelJson.getObjValAs? String "description" |>.toOption let some fileRequired := fileRequired? | return false let some entryRequired := entryRequired? | return false + let some sourceSpanRequired := sourceSpanRequired? | return false let some useRefProps := useRefProps? | return false let displayCaptionDesc? := do let displayCaptionJson ← entryProps.get? "displayCaption" @@ -159,6 +179,19 @@ open Informal.PreviewManifest defs.contains "Informal.Source.DocumentKind" && defs.contains "Informal.Source.Ref" && defs.contains "Informal.Source.Span" && + sourceSpanProps.contains "page" && + sourceSpanProps.contains "anchor" && + sourceSpanProps.contains "citation" && + sourceSpanProps.contains "text" && + sourceSpanProps.contains "pdf" && + sourceSpanRequired.contains "page" && + sourceSpanRequired.contains "anchor" && + sourceSpanRequired.contains "citation" && + sourceSpanRequired.contains "text" && + sourceSpanRequired.contains "pdf" && + (sourceSpanProps.get? "page").any schemaHasStringNull && + (sourceSpanProps.get? "anchor").any schemaHasStringNull && + (sourceSpanProps.get? "citation").any schemaHasStringNull && defs.contains "Informal.Source.TextRange" && defs.contains "Informal.Source.PdfSpan" && defs.contains "Informal.Source.PdfBox" && diff --git a/tests/VersoBlueprintTests/BlueprintSource.lean b/tests/VersoBlueprintTests/BlueprintSource.lean index be1516f9..a9514e33 100644 --- a/tests/VersoBlueprintTests/BlueprintSource.lean +++ b/tests/VersoBlueprintTests/BlueprintSource.lean @@ -20,7 +20,10 @@ private def sourcedLabel : Name := Name.mkSimple "source.lemma" private def secondSourcedLabel : Name := Name.mkSimple "source.second" private def sourceRefHasPage (document page : String) (sourceRef : Informal.Source.Ref) : Bool := - sourceRef.document == document && sourceRef.spans.any (fun span => span.page == page) + sourceRef.document == document && sourceRef.spans.any (fun span => span.page == some page) + +private def sourceRefHasAnchor (document anchor : String) (sourceRef : Informal.Source.Ref) : Bool := + sourceRef.document == document && sourceRef.spans.any (fun span => span.anchor == some anchor) private def entryHasSourcePage (document page : String) (entry : Informal.PreviewManifest.Entry) : Bool := @@ -30,11 +33,21 @@ private def entryOptionHasSourcePage (document page : String) (entry? : Option Informal.PreviewManifest.Entry) : Bool := entry?.any fun entry => entryHasSourcePage document page entry +private def entryHasSourceAnchor + (document anchor : String) (entry : Informal.PreviewManifest.Entry) : Bool := + entry.hasSourceDocument document && entry.sources.any (sourceRefHasAnchor document anchor) + +private def entryOptionHasSourceAnchor + (document anchor : String) (entry? : Option Informal.PreviewManifest.Entry) : Bool := + entry?.any fun entry => entryHasSourceAnchor document anchor entry + private def sourceRefHasRepresentationTheorySpan (sourceRef : Informal.Source.Ref) : Bool := sourceRef.document == "paper" && sourceRef.spans.any fun span => let boxXMax := (span.pdf.bind (·.box)).map (·.xMax) - span.page == "12" && + span.page == some "12" && + span.anchor == some "lem:representation" && + span.citation == some "Lemma 4.2" && span.text.map (·.path) == some "source/pages/page-12.md" && span.text.map (·.startLine) == some 41 && span.text.map (·.endLine) == some 45 && @@ -69,6 +82,8 @@ source := { spans := #[ { page := "12" + anchor := "lem:representation" + citation := "Lemma 4.2" text := some { path := "source/pages/page-12.md" startLine := 41 @@ -101,9 +116,10 @@ source := { document := "notes" spans := #[ { - page := "A" + anchor := "itm:addition-right-identity" + citation := "Lemma 2.1(1)" text := some { - path := "source/notes/addition.md" + path := "source/notes/addition.tex" startLine := 1 endLine := 3 } @@ -250,13 +266,29 @@ Invalid source metadata. let refErrors := Informal.Source.Ref.validationErrors ({ document := "paper" } : Informal.Source.Ref) + let citationOnlySpanErrors := + Informal.Source.Span.validationErrors + ({ citation := "Lemma 2.1(1)" } : Informal.Source.Span) + let anchorOnlySpanErrors := + Informal.Source.Span.validationErrors + ({ anchor := "itm:addition-right-identity" } : Informal.Source.Span) + let anchoredTextSpanErrors := + Informal.Source.Span.validationErrors + ({ + anchor := "itm:addition-right-identity" + citation := "Lemma 2.1(1)" + text := some { path := "source.tex", startLine := 1, endLine := 3 } + } : Informal.Source.Span) let expectedDocumentErrors : Array Informal.Source.ValidationError := #[ .emptyField "source document id", .pdfDocumentMissingPath ] let expectedRefErrors : Array Informal.Source.ValidationError := #[.refMissingSpan] documentErrors == expectedDocumentErrors && - refErrors == expectedRefErrors + refErrors == expectedRefErrors && + citationOnlySpanErrors == #[.spanMissingLocation] && + anchorOnlySpanErrors.isEmpty && + anchoredTextSpanErrors.isEmpty /-- info: true -/ #guard_msgs in @@ -265,17 +297,21 @@ Invalid source metadata. let (html, st) ← renderManualDocHtmlStringAndState extension_impls% sourceProvenanceDoc let sourceDocument? := Informal.TraversalIndex.SourceDocuments.data? st "paper" let sourceRef? := Informal.TraversalIndex.SourceRefs.data? st sourcedLabel + let secondSourceRef? := Informal.TraversalIndex.SourceRefs.data? st secondSourcedLabel let storageOk := - match sourceDocument?, sourceRef? with - | some sourceDocument, some sourceRef => + match sourceDocument?, sourceRef?, secondSourceRef? with + | some sourceDocument, some sourceRef, some secondSourceRef => sourceDocument.id == "paper" && sourceDocument.title == "Representation Theory" && sourceDocument.kind == .pdf && sourceDocument.pdf == some "source/paper.pdf" && sourceDocument.pageRoot == some "source/pages" && sourceDocument.imageRoot == some "source/pages/images" && - sourceRefHasRepresentationTheorySpan sourceRef - | _, _ => false + sourceRefHasRepresentationTheorySpan sourceRef && + sourceRefHasAnchor "notes" "itm:addition-right-identity" secondSourceRef && + secondSourceRef.spans.any (fun span => + span.page.isNone && span.citation == some "Lemma 2.1(1)") + | _, _, _ => false pure <| hasSubstr html "A sourced statement." && !hasSubstr html "source/paper.pdf" && @@ -312,9 +348,9 @@ Invalid source metadata. entry.targetKind == .leanDecl && entry.sources.size == 2 && entryHasSourcePage "paper" "12" entry && - entryHasSourcePage "notes" "A" entry) && + entryHasSourceAnchor "notes" "itm:addition-right-identity" entry) && entryOptionHasSourcePage "paper" "12" entry? && - entryOptionHasSourcePage "notes" "A" secondEntry? + entryOptionHasSourceAnchor "notes" "itm:addition-right-identity" secondEntry? /-- info: true -/ #guard_msgs in diff --git a/tests/browser/test_preview_runtime_regressions.py b/tests/browser/test_preview_runtime_regressions.py index 83d5694a..7a69603f 100644 --- a/tests/browser/test_preview_runtime_regressions.py +++ b/tests/browser/test_preview_runtime_regressions.py @@ -1513,6 +1513,8 @@ def test_generated_manifest_carries_source_metadata_for_external_markup(self, se assert entry["label"] == "custom_client_external_markdown_metadata" assert source_ref["document"] == "custom-client-paper" assert span["page"] == "42" + assert span["anchor"] == "thm:custom-client" + assert span["citation"] == "Theorem 4.2" assert span["text"]["path"] == "source/pages/page-42.md" assert span["text"]["startLine"] == 10 assert span["text"]["endLine"] == 12 @@ -2168,7 +2170,7 @@ def test_source_header_chip_opens_source_preview(self, server: str, page: Page): ).first source_slot = statement.locator(".bp_extra_slot_source").first chip = source_slot.locator(".bp_source_ref_chip").first - expect(chip).to_have_text("source 1") + expect(chip).to_have_text("source: Theorem 4.2") uses_chip = statement.locator(".bp_extra_slot_uses .bp_relation_chip").first source_box = require_box(chip) @@ -2190,6 +2192,8 @@ def test_source_header_chip_opens_source_preview(self, server: str, page: Page): body = preview.locator(".bp_source_ref_preview_body").first expect(body).to_contain_text("custom-client-paper") expect(body).to_contain_text("custom-client-paper p. 42") + expect(body).to_contain_text("citation Theorem 4.2") + expect(body).to_contain_text("anchor thm:custom-client") expect(body).to_contain_text("source/pages/page-42.md:10-12") expect(body).to_contain_text("source/pages/page-42.pdf") diff --git a/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CustomRenderClient.lean b/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CustomRenderClient.lean index e91c8caa..d670b139 100644 --- a/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CustomRenderClient.lean +++ b/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CustomRenderClient.lean @@ -498,6 +498,8 @@ source := { spans := #[ { page := "42" + anchor := "thm:custom-client" + citation := "Theorem 4.2" text := some { path := "source/pages/page-42.md" startLine := 10 From 1ec8d5556eb33182a7b09c316cfc0e85ff1d54ae Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 5 Aug 2026 03:40:23 +0200 Subject: [PATCH 2/2] fix: tighten source provenance contracts (cherry picked from commit a4ce0e04d7993818fb323c7b800be090b3fcf5ac) --- README.md | 8 +- doc/API.md | 5 ++ doc/DESIGN_RATIONALE.md | 11 +-- doc/MANUAL.md | 5 ++ src/VersoBlueprint/Informal/Block/Render.lean | 79 ++++++++----------- src/VersoBlueprint/PreviewManifest.lean | 39 ++++++--- src/VersoBlueprint/blueprint-api-types.mjs | 24 +++--- .../BlueprintExternalMarkup.lean | 2 +- .../BlueprintPreviewSchema.lean | 71 ++++++++++++++--- .../VersoBlueprintTests/BlueprintSource.lean | 40 ++++++++++ tests/VersoBlueprintTests/Vbp.lean | 24 ++++++ .../test_preview_runtime_regressions.py | 16 ++++ .../Chapters/CustomRenderClient.lean | 9 +++ 13 files changed, 240 insertions(+), 93 deletions(-) diff --git a/README.md b/README.md index dbb307a2..e322d668 100644 --- a/README.md +++ b/README.md @@ -272,9 +272,11 @@ For every natural number $`n`, $`n + 0 = n`. Current behavior: source provenance is exported in the Blueprint manifest as `sourceDocuments` and per-entry `sources`. A sourced node shows a compact chip; -when one source citation is available, the chip says, for example, -`source: Lemma 2.1(1)` rather than presenting the citation as Blueprint's own -generated number. +when an entry has exactly one source ref and that ref has one unique citation, +the chip says, for example, `source: Lemma 2.1(1)` rather than presenting the +citation as Blueprint's own generated number. Entries with multiple source refs +retain the `sources N` summary so that the chip does not hide aggregated +provenance. Browser clients can resolve source-document ids with `loadSourceDocument`, load the complete catalog with `loadSourceDocuments`, or join entry source refs with declared documents using `resolveSourceMetadata` from `api/data.mjs` or diff --git a/doc/API.md b/doc/API.md index 082f15c1..22fb8b62 100644 --- a/doc/API.md +++ b/doc/API.md @@ -1219,6 +1219,11 @@ they own. Each span may carry a source-native `anchor` (for example a TeX `\label`) and a human-readable `citation` (for example `Lemma 2.1(1)`) in addition to its optional page, text range, and PDF location. +Generated JSON includes every source-provenance field. Fields backed by Lean +`Option` values are encoded as either their documented value or `null`, rather +than being omitted. In particular, clients must handle page-less spans as +`page: null` and use their anchor, text range, or PDF location instead. + | Helper | Success shape | Failure shape | | --- | --- | --- | | `resolveLabel(label, options)` | `{ ok: true, label, facet, key, manifestEntry, href, sourceLocation }` | `{ ok: false, label, facet, key, reason, manifestEntry, href, sourceLocation }` | diff --git a/doc/DESIGN_RATIONALE.md b/doc/DESIGN_RATIONALE.md index 7ecf6b32..3d3ba529 100644 --- a/doc/DESIGN_RATIONALE.md +++ b/doc/DESIGN_RATIONALE.md @@ -50,11 +50,12 @@ rather than invent parallel sources of truth. Blueprint labels and traversal-generated heading numbers identify nodes inside the Blueprint site. They must remain independent of identities inherited from -an original TeX, PDF, or text source. A source span therefore records a stable -source-native `anchor` and a human-facing `citation` alongside physical page, -text, or PDF locations. For example, a node generated as `Lemma 2.2` can point -to `itm: ib-first` and display `source: Lemma 2.1(1)` without changing its graph -key, cross-references, or intrinsic numbering. +an original TeX, PDF, or text source. A source span may therefore record a +stable source-native `anchor` and a human-facing `citation` either alongside +physical page, text, or PDF locations or, for an anchor-only span, instead of +them. For example, a node generated as `Lemma 2.2` can point to `itm:ib-first` +and display `source: Lemma 2.1(1)` without changing its graph key, +cross-references, or intrinsic numbering. The source anchor is machine identity; the citation is presentation. Neither is reconstructed from visible prose, and neither is used as a substitute for the diff --git a/doc/MANUAL.md b/doc/MANUAL.md index a3d31f8d..46b659d5 100644 --- a/doc/MANUAL.md +++ b/doc/MANUAL.md @@ -672,6 +672,11 @@ shells also show a compact source chip when source provenance is present; open it to inspect the source document id, source-native anchor and citation, page summary, and recorded text/PDF span details. +When an entry has exactly one source ref with one unique citation, the chip +displays that citation as `source: ...`. A single ref without a unique citation +uses `source 1`; entries that aggregate several refs use `sources N` so the +compact label does not hide additional provenance. + `anchor` is a stable identifier in the original source, such as a TeX `\label`; `citation` is the corresponding human-readable source identity, such as `Lemma 2.1(1)` or `Equation (2.4)`. These fields do not replace the diff --git a/src/VersoBlueprint/Informal/Block/Render.lean b/src/VersoBlueprint/Informal/Block/Render.lean index 2b2b3590..286756e1 100644 --- a/src/VersoBlueprint/Informal/Block/Render.lean +++ b/src/VersoBlueprint/Informal/Block/Render.lean @@ -270,6 +270,20 @@ private def externalMarkupBadgeText : Data.ExternalMarkupLanguage → String private def pushUniqueString (values : Array String) (value : String) : Array String := if values.contains value then values else values.push value +private def trimmedOptionalString (value? : Option String) : Option String := do + let rawValue ← value? + let value := rawValue.trimAscii.toString + if value.isEmpty then none else some value + +private def collectTrimmedUniqueBy {α : Type} (values : Array α) + (value? : α → Option String) : Array String := + values.foldl + (init := #[]) + fun collected item => + match trimmedOptionalString (value? item) with + | some value => pushUniqueString collected value + | none => collected + private def externalMarkupLanguages (markup : Array Data.ExternalMarkup) : Array Data.ExternalMarkupLanguage := markup.foldl @@ -369,14 +383,7 @@ private def renderMetadataCodeLinkValue (href : String) (value : Data.AuthorId) {{s!"{value}"}} private def sourceSpanPages (spans : Array Source.Span) : Array String := - spans.foldl - (init := #[]) - fun pages span => - match span.page with - | none => pages - | some rawPage => - let page := rawPage.trimAscii.toString - if page.isEmpty then pages else pushUniqueString pages page + collectTrimmedUniqueBy spans (·.page) private def sourcePagesSummary (pages : Array String) : String := match pages.toList with @@ -397,26 +404,16 @@ private def sourcePdfSpanSummary (span : Source.PdfSpan) : String := | Option.some image => s!"pdf {span.path}; image {image}" | Option.none => s!"pdf {span.path}" +private def pushOptionalSourceSummary (parts : Array String) (key : String) + (value? : Option String) : Array String := + match trimmedOptionalString value? with + | some value => parts.push s!"{key} {value}" + | none => parts + private def sourceSpanSummary (span : Source.Span) : String := - let parts : Array String := #[] - let parts := - match span.citation with - | Option.some citation => - let citation := citation.trimAscii.toString - if citation.isEmpty then parts else parts.push s!"citation {citation}" - | Option.none => parts - let parts := - match span.anchor with - | Option.some anchor => - let anchor := anchor.trimAscii.toString - if anchor.isEmpty then parts else parts.push s!"anchor {anchor}" - | Option.none => parts - let parts := - match span.page with - | Option.some rawPage => - let page := rawPage.trimAscii.toString - if page.isEmpty then parts else parts.push s!"page {page}" - | Option.none => parts + let parts := pushOptionalSourceSummary #[] "citation" span.citation + let parts := pushOptionalSourceSummary parts "anchor" span.anchor + let parts := pushOptionalSourceSummary parts "page" span.page let parts := match span.text with | Option.some textRange => parts.push (sourceTextRangeSummary textRange) @@ -428,20 +425,7 @@ private def sourceSpanSummary (span : Source.Span) : String := String.intercalate "; " parts.toList private def sourceSpanCitations (spans : Array Source.Span) : Array String := - spans.foldl - (init := #[]) - fun citations span => - match span.citation with - | none => citations - | some rawCitation => - let citation := rawCitation.trimAscii.toString - if citation.isEmpty then citations else pushUniqueString citations citation - -private def sourceRefsCitations (sourceRefs : Array Source.Ref) : Array String := - sourceRefs.foldl - (init := #[]) - fun citations sourceRef => - (sourceSpanCitations sourceRef.spans).foldl pushUniqueString citations + collectTrimmedUniqueBy spans (·.citation) private def sourceRefSummary (sourceRef : Source.Ref) : String := let pages := sourceSpanPages sourceRef.spans @@ -460,13 +444,12 @@ private def sourceRefTitle (sourceRef : Source.Ref) : String := s!"Original source document {sourceRef.document}: {String.intercalate " | " spanSummary}" private def sourceRefsChipText (sourceRefs : Array Source.Ref) : String := - match sourceRefsCitations sourceRefs |>.toList with - | [citation] => s!"source: {citation}" - | _ => - if sourceRefs.size == 1 then - "source 1" - else - s!"sources {sourceRefs.size}" + match sourceRefs.toList with + | [sourceRef] => + match sourceSpanCitations sourceRef.spans |>.toList with + | [citation] => s!"source: {citation}" + | _ => "source 1" + | _ => s!"sources {sourceRefs.size}" private def sourceRefsPanelTitle (sourceRefs : Array Source.Ref) : String := if sourceRefs.size == 1 then diff --git a/src/VersoBlueprint/PreviewManifest.lean b/src/VersoBlueprint/PreviewManifest.lean index 13b9dcbd..f902e4c5 100644 --- a/src/VersoBlueprint/PreviewManifest.lean +++ b/src/VersoBlueprint/PreviewManifest.lean @@ -694,7 +694,7 @@ This is a VBP stale-artifact diagnostic marker, not a public interchange version. It may change whenever the generated-data reader needs a clean validation boundary. -/ -def manifestInternalSchemaVersion : Nat := 3 +def manifestInternalSchemaVersion : Nat := 4 def manifestInternalSchemaVersionField : String := "vbpInternalSchemaVersion" @@ -1697,18 +1697,31 @@ private partial def schemaForType (ty : Expr) : StateT SchemaState MetaM Json := modify fun st => { st with seen := st.seen.insert name } let env ← getEnv if let some info := getStructureInfo? env name then - let mut properties : List (String × Json) := [] - let mut required : Array Json := #[] - for fieldInfo in info.fieldInfo do - let schema ← schemaForType (← fieldType fieldInfo.projFn) - let docs? ← findDocString? env fieldInfo.projFn - let schema := - match docs? with - | some docs => schemaWithDescription schema docs - | none => schema - let key := fieldKey fieldInfo.fieldName - properties := properties.concat (key, schema) - required := required.push (Json.str key) + let rec collectFields (info : StructureInfo) : + StateT SchemaState MetaM (List (String × Json) × Array Json) := do + let mut properties : List (String × Json) := [] + let mut required : Array Json := #[] + for fieldInfo in info.fieldInfo do + match fieldInfo.subobject? with + | some parentName => + -- Derived JSON flattens embedded parent structures into the child object. + let some parentInfo := getStructureInfo? env parentName + | throwError "Unsupported schema parent structure: {parentName}" + let (parentProperties, parentRequired) ← collectFields parentInfo + properties := properties ++ parentProperties + required := required ++ parentRequired + | none => + let schema ← schemaForType (← fieldType fieldInfo.projFn) + let docs? ← findDocString? env fieldInfo.projFn + let schema := + match docs? with + | some docs => schemaWithDescription schema docs + | none => schema + let key := fieldKey fieldInfo.fieldName + properties := properties.concat (key, schema) + required := required.push (Json.str key) + pure (properties, required) + let (properties, required) ← collectFields info let schema := Json.mkObj [ ("type", Json.str "object"), ("properties", Json.mkObj properties), diff --git a/src/VersoBlueprint/blueprint-api-types.mjs b/src/VersoBlueprint/blueprint-api-types.mjs index cf78f072..c688a25c 100644 --- a/src/VersoBlueprint/blueprint-api-types.mjs +++ b/src/VersoBlueprint/blueprint-api-types.mjs @@ -173,9 +173,9 @@ * @property {string} id Canonical source-document id. * @property {string} title Human-readable source title. * @property {"pdf" | "text" | string} kind Broad source-document kind. - * @property {string} [pdf] Source PDF path, when the document is PDF-backed. - * @property {string} [pageRoot] Optional root for extracted source pages. - * @property {string} [imageRoot] Optional root for extracted page images. + * @property {string | null} pdf Source PDF path, or `null` when the document is not PDF-backed. + * @property {string | null} pageRoot Root for extracted source pages, or `null` when unavailable. + * @property {string | null} imageRoot Root for extracted page images, or `null` when unavailable. */ /** @@ -185,8 +185,8 @@ * @property {string} path Source text path. * @property {number} startLine One-based inclusive start line. * @property {number} endLine One-based inclusive end line. - * @property {number} [startCharacter] Optional start character. - * @property {number} [endCharacter] Optional end character. + * @property {number | null} startCharacter Start character, or `null` when the span covers whole lines. + * @property {number | null} endCharacter End character, or `null` when the span covers whole lines. */ /** @@ -207,19 +207,19 @@ * * @typedef {Object} BlueprintSourcePdfSpan * @property {string} path Source PDF page path. - * @property {string} [image] Optional rendered page image path. - * @property {BlueprintSourcePdfBox} [box] Optional crop box. + * @property {string | null} image Rendered page image path, or `null` when unavailable. + * @property {BlueprintSourcePdfBox | null} box Crop box, or `null` when the span covers the page. */ /** * One original source span attached to a Blueprint node. * * @typedef {Object} BlueprintSourceSpan - * @property {string} [page] Optional source-local page identifier. - * @property {string} [anchor] Stable source-native identifier, such as a TeX `\\label`. - * @property {string} [citation] Human-readable source-native reference, such as `Lemma 2.1(1)`. - * @property {BlueprintSourceTextRange} [text] Text location for this span. - * @property {BlueprintSourcePdfSpan} [pdf] PDF/page-image location for this span. + * @property {string | null} page Source-local page identifier, or `null` for a page-less span. + * @property {string | null} anchor Stable source-native identifier, such as a TeX `\\label`, or `null` when unavailable. + * @property {string | null} citation Human-readable source-native reference, such as `Lemma 2.1(1)`, or `null` when unavailable. + * @property {BlueprintSourceTextRange | null} text Text location, or `null` when unavailable. + * @property {BlueprintSourcePdfSpan | null} pdf PDF/page-image location, or `null` when unavailable. */ /** diff --git a/tests/VersoBlueprintTests/BlueprintExternalMarkup.lean b/tests/VersoBlueprintTests/BlueprintExternalMarkup.lean index ede7e878..edcaa498 100644 --- a/tests/VersoBlueprintTests/BlueprintExternalMarkup.lean +++ b/tests/VersoBlueprintTests/BlueprintExternalMarkup.lean @@ -951,7 +951,7 @@ external markup. sourcedWitnessEntry.sources.any (fun sourceRef => sourceRef.document == "external-paper" && sourceRef.spans.size == 1 && - sourceRef.spans[0]!.page == "7") && + sourceRef.spans[0]!.page == some "7") && htmlHasSourcePreview sourcedWitnessHtml "external-paper" "p. 7" && hasSubstr externalOut "bp_extra_slot_markup" && hasSubstr externalOut "bp_external_markup_badge_markdown" && diff --git a/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean b/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean index d82d43ad..0ef73dee 100644 --- a/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean +++ b/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean @@ -31,38 +31,61 @@ open Informal.PreviewManifest fromJson? (α := Array String) requiredJson |>.toOption let some relatedEntrySchema := defs.get? "Informal.PreviewManifest.RelatedEntry" | return false let some graphNodeSchema := defs.get? "Informal.Graph.NodeData" | return false + let some sourceDocumentSchema := defs.get? "Informal.Source.Document" | return false + let Except.ok sourceDocumentPropsJson := + Json.getObjVal? sourceDocumentSchema "properties" | return false + let Except.ok sourceDocumentProps := sourceDocumentPropsJson.getObj? | return false + let sourceDocumentRequired? := do + let requiredJson ← sourceDocumentSchema.getObjVal? "required" |>.toOption + fromJson? (α := Array String) requiredJson |>.toOption let some sourceSpanSchema := defs.get? "Informal.Source.Span" | return false let Except.ok sourceSpanPropsJson := Json.getObjVal? sourceSpanSchema "properties" | return false let Except.ok sourceSpanProps := sourceSpanPropsJson.getObj? | return false let sourceSpanRequired? := do let requiredJson ← sourceSpanSchema.getObjVal? "required" |>.toOption fromJson? (α := Array String) requiredJson |>.toOption + let some sourceTextRangeSchema := defs.get? "Informal.Source.TextRange" | return false + let Except.ok sourceTextRangePropsJson := + Json.getObjVal? sourceTextRangeSchema "properties" | return false + let Except.ok sourceTextRangeProps := sourceTextRangePropsJson.getObj? | return false + let sourceTextRangeRequired? := do + let requiredJson ← sourceTextRangeSchema.getObjVal? "required" |>.toOption + fromJson? (α := Array String) requiredJson |>.toOption + let some sourcePdfSpanSchema := defs.get? "Informal.Source.PdfSpan" | return false + let Except.ok sourcePdfSpanPropsJson := + Json.getObjVal? sourcePdfSpanSchema "properties" | return false + let Except.ok sourcePdfSpanProps := sourcePdfSpanPropsJson.getObj? | return false + let sourcePdfSpanRequired? := do + let requiredJson ← sourcePdfSpanSchema.getObjVal? "required" |>.toOption + fromJson? (α := Array String) requiredJson |>.toOption let schemaText := schema.compress let stringSchemaHasMinLengthOne (schema : Json) : Bool := (schema.getObjValAs? String "type" |>.toOption) == some "string" && (schema.getObjValAs? Nat "minLength" |>.toOption) == some 1 let stringSchema (schema : Json) : Bool := (schema.getObjValAs? String "type" |>.toOption) == some "string" - let schemaHasStringNull (schema : Json) : Bool := + let integerSchema (schema : Json) : Bool := + (schema.getObjValAs? String "type" |>.toOption) == some "integer" + let refSchema (expected : String) (schema : Json) : Bool := + (schema.getObjValAs? String "$ref" |>.toOption) == some expected + let schemaHasValueNull (valueSchema : Json → Bool) (schema : Json) : Bool := match Json.getObjVal? schema "anyOf" with | Except.error _ => false | Except.ok anyOfJson => match anyOfJson.getArr? with | Except.error _ => false | Except.ok schemas => - schemas.any stringSchema && + schemas.any valueSchema && schemas.any (fun (schema : Json) => (schema.getObjValAs? String "type" |>.toOption) == some "null") + let schemaHasStringNull (schema : Json) : Bool := + schemaHasValueNull stringSchema schema let schemaHasNonEmptyStringNull (schema : Json) : Bool := - match Json.getObjVal? schema "anyOf" with - | Except.error _ => false - | Except.ok anyOfJson => - match anyOfJson.getArr? with - | Except.error _ => false - | Except.ok schemas => - schemas.any stringSchemaHasMinLengthOne && - schemas.any (fun (schema : Json) => - (schema.getObjValAs? String "type" |>.toOption) == some "null") + schemaHasValueNull stringSchemaHasMinLengthOne schema + let schemaHasIntegerNull (schema : Json) : Bool := + schemaHasValueNull integerSchema schema + let schemaHasRefNull (expected : String) (schema : Json) : Bool := + schemaHasValueNull (refSchema expected) schema let previewKeySchemaHasNonEmptyStringNull (schema : Json) : Bool := match Json.getObjVal? schema "properties" with | Except.error _ => false @@ -100,7 +123,10 @@ open Informal.PreviewManifest authoredLabelJson.getObjValAs? String "description" |>.toOption let some fileRequired := fileRequired? | return false let some entryRequired := entryRequired? | return false + let some sourceDocumentRequired := sourceDocumentRequired? | return false let some sourceSpanRequired := sourceSpanRequired? | return false + let some sourceTextRangeRequired := sourceTextRangeRequired? | return false + let some sourcePdfSpanRequired := sourcePdfSpanRequired? | return false let some useRefProps := useRefProps? | return false let displayCaptionDesc? := do let displayCaptionJson ← entryProps.get? "displayCaption" @@ -177,6 +203,16 @@ open Informal.PreviewManifest defs.contains "Informal.Data.ExternalMarkupLocation" && defs.contains "Informal.Source.Document" && defs.contains "Informal.Source.DocumentKind" && + !sourceDocumentProps.contains "toDocumentMetadata" && + sourceDocumentRequired.contains "id" && + sourceDocumentRequired.contains "title" && + sourceDocumentRequired.contains "kind" && + sourceDocumentRequired.contains "pdf" && + sourceDocumentRequired.contains "pageRoot" && + sourceDocumentRequired.contains "imageRoot" && + (sourceDocumentProps.get? "pdf").any schemaHasStringNull && + (sourceDocumentProps.get? "pageRoot").any schemaHasStringNull && + (sourceDocumentProps.get? "imageRoot").any schemaHasStringNull && defs.contains "Informal.Source.Ref" && defs.contains "Informal.Source.Span" && sourceSpanProps.contains "page" && @@ -192,8 +228,21 @@ open Informal.PreviewManifest (sourceSpanProps.get? "page").any schemaHasStringNull && (sourceSpanProps.get? "anchor").any schemaHasStringNull && (sourceSpanProps.get? "citation").any schemaHasStringNull && + (sourceSpanProps.get? "text").any + (schemaHasRefNull "#/$defs/Informal.Source.TextRange") && + (sourceSpanProps.get? "pdf").any + (schemaHasRefNull "#/$defs/Informal.Source.PdfSpan") && defs.contains "Informal.Source.TextRange" && + sourceTextRangeRequired.contains "startCharacter" && + sourceTextRangeRequired.contains "endCharacter" && + (sourceTextRangeProps.get? "startCharacter").any schemaHasIntegerNull && + (sourceTextRangeProps.get? "endCharacter").any schemaHasIntegerNull && defs.contains "Informal.Source.PdfSpan" && + sourcePdfSpanRequired.contains "image" && + sourcePdfSpanRequired.contains "box" && + (sourcePdfSpanProps.get? "image").any schemaHasStringNull && + (sourcePdfSpanProps.get? "box").any + (schemaHasRefNull "#/$defs/Informal.Source.PdfBox") && defs.contains "Informal.Source.PdfBox" && defs.contains "Informal.Data.SourceLocation" && defs.contains "Informal.Data.SourceLocationResult" && diff --git a/tests/VersoBlueprintTests/BlueprintSource.lean b/tests/VersoBlueprintTests/BlueprintSource.lean index a9514e33..df17cf27 100644 --- a/tests/VersoBlueprintTests/BlueprintSource.lean +++ b/tests/VersoBlueprintTests/BlueprintSource.lean @@ -290,6 +290,46 @@ Invalid source metadata. anchorOnlySpanErrors.isEmpty && anchoredTextSpanErrors.isEmpty +/-- info: true -/ +#guard_msgs in +#eval + show Bool from + let sharedCitation := "Lemma 2.1(1)" + let paperSource : Informal.Source.Ref := { + document := "paper" + spans := #[{ page := "12", citation := sharedCitation }] + } + let notesSource : Informal.Source.Ref := { + document := "notes" + spans := #[{ anchor := "itm:addition-right-identity", citation := sharedCitation }] + } + let uncitedSource : Informal.Source.Ref := { + document := "paper" + spans := #[{ page := "12" }] + } + let ambiguousSource : Informal.Source.Ref := { + document := "paper" + spans := #[ + { page := "12", citation := sharedCitation }, + { page := "13", citation := "Lemma 2.1(2)" } + ] + } + let singleHtml? := + (Informal.renderSourceHeaderExtra? #[paperSource]).map (·.html.asString) + let multipleHtml? := + (Informal.renderSourceHeaderExtra? #[paperSource, notesSource]).map (·.html.asString) + let uncitedHtml? := + (Informal.renderSourceHeaderExtra? #[uncitedSource]).map (·.html.asString) + let ambiguousHtml? := + (Informal.renderSourceHeaderExtra? #[ambiguousSource]).map (·.html.asString) + singleHtml?.any (hasSubstr · s!"source: {sharedCitation}") && + multipleHtml?.any (hasSubstr · "sources 2") && + !multipleHtml?.any (hasSubstr · s!"source: {sharedCitation}") && + uncitedHtml?.any (hasSubstr · "source 1") && + !uncitedHtml?.any (hasSubstr · "source:") && + ambiguousHtml?.any (hasSubstr · "source 1") && + !ambiguousHtml?.any (hasSubstr · "source:") + /-- info: true -/ #guard_msgs in #eval diff --git a/tests/VersoBlueprintTests/Vbp.lean b/tests/VersoBlueprintTests/Vbp.lean index e73d04a2..0d0aa8e0 100644 --- a/tests/VersoBlueprintTests/Vbp.lean +++ b/tests/VersoBlueprintTests/Vbp.lean @@ -1032,6 +1032,30 @@ private def writeRawManifestOnlySite (site : System.FilePath) (manifestJson : Js message.contains Informal.PreviewManifest.manifestInternalSchemaVersionField && message.contains "lake exe vbp build" +/-- info: true -/ +#guard_msgs in +#eval do + let site ← freshVbpFixtureRoot + let staleManifestJson := Json.mkObj [ + (Informal.PreviewManifest.manifestInternalSchemaVersionField, + toJson (Informal.PreviewManifest.manifestInternalSchemaVersion - 1)), + ("previews", Json.arr #[]), + ("groups", Json.arr #[]), + ("graphs", Json.arr #[]), + ("sourceDocuments", Json.arr #[]) + ] + writeRawManifestOnlySite site staleManifestJson + try + let _ ← VersoBlueprint.Vbp.readManifestForSite site + pure false + catch err => + let message := IO.Error.toString err + pure <| + message.contains "unsupported internal Blueprint manifest schema" && + message.contains "found" && + message.contains "expected" && + message.contains "lake exe vbp build" + /-- info: true -/ #guard_msgs in #eval diff --git a/tests/browser/test_preview_runtime_regressions.py b/tests/browser/test_preview_runtime_regressions.py index 7a69603f..11f7e3ad 100644 --- a/tests/browser/test_preview_runtime_regressions.py +++ b/tests/browser/test_preview_runtime_regressions.py @@ -1500,6 +1500,7 @@ def test_generated_manifest_carries_source_metadata_for_external_markup(self, se ) source_ref = entry["sources"][0] span = source_ref["spans"][0] + page_less_span = source_ref["spans"][1] assert source_document == { "id": "custom-client-paper", @@ -1529,6 +1530,19 @@ def test_generated_manifest_carries_source_metadata_for_external_markup(self, se "yMax": 520, "yMin": 240, } + assert page_less_span == { + "anchor": "itm:custom-client", + "citation": "Theorem 4.2", + "page": None, + "pdf": None, + "text": { + "endCharacter": None, + "endLine": 82, + "path": "source/custom-client.tex", + "startCharacter": None, + "startLine": 80, + }, + } def test_public_apis_resolve_source_documents_from_manifest(self, server: str, page: Page): errors = record_runtime_errors(page) @@ -2196,6 +2210,8 @@ def test_source_header_chip_opens_source_preview(self, server: str, page: Page): expect(body).to_contain_text("anchor thm:custom-client") expect(body).to_contain_text("source/pages/page-42.md:10-12") expect(body).to_contain_text("source/pages/page-42.pdf") + expect(body).to_contain_text("anchor itm:custom-client") + expect(body).to_contain_text("source/custom-client.tex:80-82") assert_no_runtime_errors(errors) diff --git a/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CustomRenderClient.lean b/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CustomRenderClient.lean index d670b139..78defc04 100644 --- a/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CustomRenderClient.lean +++ b/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CustomRenderClient.lean @@ -518,6 +518,15 @@ source := { yMax := 520 } } + }, + { + anchor := "itm:custom-client" + citation := "Theorem 4.2" + text := some { + path := "source/custom-client.tex" + startLine := 80 + endLine := 82 + } } ] }