From 7d0e7443ce2334ec3d4934bebb0b746ca54d4a23 Mon Sep 17 00:00:00 2001 From: WaylandYang Date: Thu, 3 Sep 2026 11:28:29 +0800 Subject: [PATCH] A contradiction is visible where it sits (B2b) Co-Authored-By: Claude Fable 5.1 --- crates/utopia-core/src/models.rs | 35 ++ crates/utopia-server/src/api/graph_routes.rs | 17 +- crates/utopia-server/src/api/mod.rs | 5 + crates/utopia-store/src/graph.rs | 63 ++- crates/utopia-store/src/reasoning.rs | 93 ++++- .../tests/a_contradiction_points_upstream.rs | 43 +++ ...-the-open-seams-before-cutting-new-ones.md | 6 +- .../0017-a-contradiction-points-upstream.md | 2 +- docs/decisions/README.md | 4 +- web/src/api.ts | 37 ++ web/src/i18n/en.ts | 13 + web/src/i18n/zh.ts | 11 + web/src/pages/Graph.tsx | 363 +++++++++++++++--- web/src/pages/Review.tsx | 18 +- web/src/router.tsx | 7 + web/src/styles.css | 5 + 16 files changed, 635 insertions(+), 87 deletions(-) diff --git a/crates/utopia-core/src/models.rs b/crates/utopia-core/src/models.rs index ab05c1848..091a5cf84 100644 --- a/crates/utopia-core/src/models.rs +++ b/crates/utopia-core/src/models.rs @@ -513,6 +513,13 @@ pub struct GraphEdge { pub valid_from: Option>, pub valid_to: Option>, pub confidence: f32, + /// 有争议（0017 §3）：有一条 open 的公理违规或时态冲突指着它。整条边画成 + /// 警戒色——环在节点上、边还是灰的，余光分不出来 + pub contested: bool, + /// 幽灵边（0017 §3）：一条**没有落地**的派生——推出来了却撞上断言。`id` 是那条 + /// `derived_contradiction` 违规的 id，不是任何事实；`derived` 同时为 true， + /// 所以它跟着派生开关走 + pub blocked: bool, } /// 实体详情页的事实行（时间线）。 @@ -549,6 +556,10 @@ pub struct EntityFact { pub corrected: bool, /// 证据集合里最新的文档时间——开放事实的"最后确认时间"（时效性透明化） pub last_evidence_time: Option>, + /// 有争议（0017 §3）：`{ kind, ref_id, derived? }`——哪一种（违规的 kind，或 + /// `temporal_conflict`）、Review 里那一项的 id、派生撞断言时推出来的那句话。 + /// 一条只报最新的一处；行**不压暗**，断言仍然活着 + pub contested: Option, } /// 实体的一次认知变更（记录时间轴上的事件，与 EntityFact 的有效时间轴正交）。 @@ -933,6 +944,30 @@ pub struct DerivedFactView { pub premises: Vec, } +/// 一条**没有落地**的派生（0017 §3）：推出来了，撞上一条断言，拦在图外。 +/// +/// 它没有 id——落库的才有。这里用那条 `derived_contradiction` 违规的 id 指它， +/// 面板上的「没落地的」一档与图上的幽灵边都靠这个 id 对上 Review 里的卡片。 +#[derive(Debug, Clone, Serialize, sqlx::FromRow)] +pub struct BlockedDerivation { + pub violation_id: Uuid, + pub subject_id: Uuid, + pub subject: String, + pub object_id: Uuid, + pub object: String, + pub predicate: String, + pub rule: String, + /// 声明所在的谓词 + pub via_label: String, + pub valid_from: Option>, + pub valid_to: Option>, + /// 挡住它的那条断言，与它的三元组文本 + pub against_fact: Uuid, + pub against_text: String, + /// 前提事实 id，按推导顺序——证明链从这里展开 + pub premises: Vec, +} + /// 证明的一步：一条断言前提，连同它的证据（0002 R2）。 /// /// 前提一律是断言（`fact_derivations` 不记派生），所以证明是一条链而不是一棵树： diff --git a/crates/utopia-server/src/api/graph_routes.rs b/crates/utopia-server/src/api/graph_routes.rs index d693382d9..8962ac278 100644 --- a/crates/utopia-server/src/api/graph_routes.rs +++ b/crates/utopia-server/src/api/graph_routes.rs @@ -145,9 +145,12 @@ pub async fn entity_detail( // 只有先改一次名才够得着——而两个张伟并存是「宁分勿合」的正当产物，不是 // 改名改出来的。合并入口该长在能看见同名的地方。 let same_name = utopia_store::graph::same_name_peers(&state.pool, kb_id, entity_id).await?; + // 没落地的派生（0017 §3）也单独一个键：它们连 `derived_facts` 都不在 + let blocked = + utopia_store::reasoning::blocked_for_entity(&state.pool, kb_id, entity_id).await?; Ok(Json(json!({ "entity": entity, "facts": facts, - "derived": derived, "same_name": same_name, + "derived": derived, "blocked": blocked, "same_name": same_name, }))) } @@ -240,6 +243,18 @@ pub async fn derived_proof( Ok(Json(json!({ "proof": proof }))) } +/// 没落地的派生的证明链（0017 §3）：前提在那条 `derived_contradiction` 违规的 +/// `path` 里，展开方式与落了地的一样。违规不存在时 `steps` 为 null +pub async fn blocked_proof( + State(state): State, + AuthUser(user): AuthUser, + Path((kb_id, violation_id)): Path<(Uuid, Uuid)>, +) -> ApiResult> { + require_kb(&state, &user, kb_id, Role::Viewer).await?; + let steps = utopia_store::reasoning::blocked_proof(&state.pool, kb_id, violation_id).await?; + Ok(Json(json!({ "steps": steps }))) +} + /// 手动触发抽取（failed 重试 / 补配模型后补抽）。 pub async fn extract( State(state): State, diff --git a/crates/utopia-server/src/api/mod.rs b/crates/utopia-server/src/api/mod.rs index bb646e08c..aa5ff7622 100644 --- a/crates/utopia-server/src/api/mod.rs +++ b/crates/utopia-server/src/api/mod.rs @@ -295,6 +295,11 @@ pub fn router(state: AppState, cfg: &AppConfig) -> Router { "/kbs/{id}/derived/{derived_id}/proof", get(graph_routes::derived_proof), ) + // 没落地的派生的证明（0017 §3）：前提在违规的 path 里 + .route( + "/kbs/{id}/violations/{violation_id}/proof", + get(graph_routes::blocked_proof), + ) .route("/kbs/{id}/events", get(events_routes::kb_events)) .route( "/kbs/{id}/sources", diff --git a/crates/utopia-store/src/graph.rs b/crates/utopia-store/src/graph.rs index 741e93f90..fe7689ad2 100644 --- a/crates/utopia-store/src/graph.rs +++ b/crates/utopia-store/src/graph.rs @@ -418,13 +418,29 @@ async fn edges_among( // // 图要它们，因为「这条边是推出来的」正是用户该看见的信息之一；`derived` // 那一位让界面画得出区别，也让人整体过滤掉。 + // + // 第三段是**幽灵边**（0017 §3）：推出来却没落地的派生，住在 `axiom_violations` + // 的 `detail` 里。它的 id 是违规的 id；`derived` 与 `blocked` 同时为 true， + // 界面据此让它跟着派生开关走、画成争议色往背景混的那一档。 + // + // 断言那一段多算一位 `contested`：有 open 的违规或时态冲突指着它。派生撞断言 + // 时被撞的是 left；right 只是最后一条前提，它本身没有争议 let edges: Vec = sqlx::query_as( "SELECT f.id, f.subject_id AS source, f.object_id AS target, COALESCE(r.key, fact_surface_predicate(f.id)) AS predicate, COALESCE(r.label, fact_surface_predicate(f.id)) AS label, r.id IS NULL AS inferred, FALSE AS derived, NULL::text AS rule, ARRAY[]::uuid[] AS premises, - f.valid_from, f.valid_to, f.confidence + f.valid_from, f.valid_to, f.confidence, + (EXISTS (SELECT 1 FROM axiom_violations v + WHERE v.status = 'open' + AND (v.left_fact = f.id + OR (v.right_fact = f.id AND v.kind <> 'derived_contradiction'))) + OR EXISTS (SELECT 1 FROM fact_conflicts c + WHERE c.status = 'open' + AND (c.old_fact_id = f.id OR c.new_fact_id = f.id)) + ) AS contested, + FALSE AS blocked FROM facts f LEFT JOIN relation_types r ON r.id = f.predicate_id WHERE f.kb_id = $1 AND f.invalidated_at IS NULL AND f.object_id IS NOT NULL AND f.subject_id = ANY($2) AND f.object_id = ANY($2) @@ -437,14 +453,35 @@ async fn edges_among( FALSE AS inferred, TRUE AS derived, ru.kind AS rule, ARRAY(SELECT fd.premise_fact_id FROM fact_derivations fd WHERE fd.derived_fact_id = d.id ORDER BY fd.seq) AS premises, - d.valid_from, d.valid_to, d.confidence + d.valid_from, d.valid_to, d.confidence, + FALSE AS contested, FALSE AS blocked FROM derived_facts d JOIN relation_types r ON r.id = d.predicate_id JOIN rules ru ON ru.id = d.rule_id WHERE d.kb_id = $1 AND d.invalidated_at IS NULL AND d.subject_id = ANY($2) AND d.object_id = ANY($2) AND ($3::timestamptz IS NULL OR ((d.valid_from IS NULL OR d.valid_from <= $3) - AND (d.valid_to IS NULL OR d.valid_to > $3)))", + AND (d.valid_to IS NULL OR d.valid_to > $3))) + UNION ALL + SELECT v.id, + (v.detail->>'subject_id')::uuid AS source, + (v.detail->>'object_id')::uuid AS target, + v.detail->>'predicate' AS predicate, v.detail->>'predicate' AS label, + FALSE AS inferred, TRUE AS derived, v.detail->>'rule' AS rule, + v.path AS premises, + (v.detail->>'valid_from')::timestamptz AS valid_from, + (v.detail->>'valid_to')::timestamptz AS valid_to, + 0::real AS confidence, + TRUE AS contested, TRUE AS blocked + FROM axiom_violations v + WHERE v.kb_id = $1 AND v.kind = 'derived_contradiction' AND v.status = 'open' + AND (v.detail->>'subject_id')::uuid = ANY($2) + AND (v.detail->>'object_id')::uuid = ANY($2) + AND ($3::timestamptz IS NULL + OR (((v.detail->>'valid_from')::timestamptz IS NULL + OR (v.detail->>'valid_from')::timestamptz <= $3) + AND ((v.detail->>'valid_to')::timestamptz IS NULL + OR (v.detail->>'valid_to')::timestamptz > $3)))", ) .bind(kb_id) .bind(ids) @@ -568,7 +605,25 @@ pub async fn entity_detail( (f.supersedes IS NOT NULL) AS corrected, (SELECT MAX(COALESCE(d.doc_time, d.created_at)) FROM fact_evidence fe JOIN documents d ON d.id = fe.document_id - WHERE fe.fact_id = f.id) AS last_evidence_time + WHERE fe.fact_id = f.id) AS last_evidence_time, + COALESCE( + (SELECT jsonb_build_object( + 'kind', v.kind, 'ref_id', v.id, + 'derived', CASE WHEN v.kind = 'derived_contradiction' + THEN (v.detail->>'subject') || ' · ' + || (v.detail->>'predicate') || ' · ' + || (v.detail->>'object') END) + FROM axiom_violations v + WHERE v.status = 'open' + AND (v.left_fact = f.id + OR (v.right_fact = f.id AND v.kind <> 'derived_contradiction')) + ORDER BY v.detected_at DESC LIMIT 1), + (SELECT jsonb_build_object('kind', 'temporal_conflict', 'ref_id', c.id) + FROM fact_conflicts c + WHERE c.status = 'open' + AND (c.old_fact_id = f.id OR c.new_fact_id = f.id) + ORDER BY c.created_at DESC LIMIT 1) + ) AS contested FROM facts f LEFT JOIN relation_types r ON r.id = f.predicate_id LEFT JOIN entities o diff --git a/crates/utopia-store/src/reasoning.rs b/crates/utopia-store/src/reasoning.rs index 1b9764aac..1e7b799cd 100644 --- a/crates/utopia-store/src/reasoning.rs +++ b/crates/utopia-store/src/reasoning.rs @@ -1178,9 +1178,27 @@ pub async fn proof( let Some(derived) = derived_one(pool, kb_id, derived_id).await? else { return Ok(None); }; + let premises: Vec = sqlx::query_scalar( + "SELECT premise_fact_id FROM fact_derivations WHERE derived_fact_id = $1 ORDER BY seq", + ) + .bind(derived_id) + .fetch_all(pool) + .await?; + let steps = steps_for(pool, &premises).await?; + Ok(Some(utopia_core::models::Proof { derived, steps })) +} + +/// 一串前提展开成证明的步：三元组、区间、撤没撤、证据。 +/// +/// 落了地的派生（`fact_derivations`）与没落地的（`axiom_violations.path`）都从这里 +/// 走——前提是同一种东西，证明链没有理由长两个样 +async fn steps_for( + pool: &PgPool, + premises: &[Uuid], +) -> AppResult> { #[allow(clippy::type_complexity)] let rows: Vec<( - i32, + i64, Uuid, Uuid, String, @@ -1193,19 +1211,18 @@ pub async fn proof( f32, bool, )> = sqlx::query_as( - "SELECT fd.seq, f.id, f.subject_id, s.canonical_name, + "SELECT x.ord - 1, f.id, f.subject_id, s.canonical_name, f.predicate_id, r.label, f.object_id, o.canonical_name, f.valid_from, f.valid_to, f.confidence, f.invalidated_at IS NOT NULL - FROM fact_derivations fd - JOIN facts f ON f.id = fd.premise_fact_id + FROM unnest($1::uuid[]) WITH ORDINALITY AS x(id, ord) + JOIN facts f ON f.id = x.id JOIN entities s ON s.id = f.subject_id LEFT JOIN relation_types r ON r.id = f.predicate_id LEFT JOIN entities o ON o.id = f.object_id - WHERE fd.derived_fact_id = $1 - ORDER BY fd.seq", + ORDER BY x.ord", ) - .bind(derived_id) + .bind(premises) .fetch_all(pool) .await?; let mut steps = Vec::with_capacity(rows.len()); @@ -1227,7 +1244,7 @@ pub async fn proof( // 一条链最多 MAX_DEPTH 步，逐条取证据是可数的几次往返 let evidence = crate::graph::fact_evidence(pool, fact_id).await?; steps.push(utopia_core::models::ProofStep { - seq, + seq: seq as i32, fact_id, subject_id, subject, @@ -1242,7 +1259,65 @@ pub async fn proof( evidence, }); } - Ok(Some(utopia_core::models::Proof { derived, steps })) + Ok(steps) +} + +/// 没落地的派生里，与这个实体有关的那些（0017 §3）——面板「推出来的」一档的 +/// 「没落地的」小节。 +pub async fn blocked_for_entity( + pool: &PgPool, + kb_id: Uuid, + entity_id: Uuid, +) -> AppResult> { + Ok(sqlx::query_as( + "SELECT v.id AS violation_id, + (v.detail->>'subject_id')::uuid AS subject_id, + COALESCE(v.detail->>'subject', '?') AS subject, + (v.detail->>'object_id')::uuid AS object_id, + COALESCE(v.detail->>'object', '?') AS object, + COALESCE(v.detail->>'predicate', '?') AS predicate, + COALESCE(v.detail->>'rule', '?') AS rule, + COALESCE(v.detail->>'via_label', '?') AS via_label, + (v.detail->>'valid_from')::timestamptz AS valid_from, + (v.detail->>'valid_to')::timestamptz AS valid_to, + v.left_fact AS against_fact, + s.canonical_name || ' · ' + || COALESCE(r.label, fact_surface_predicate(f.id), '?') || ' · ' + || COALESCE(o.canonical_name, '?') AS against_text, + v.path AS premises + FROM axiom_violations v + JOIN facts f ON f.id = v.left_fact + JOIN entities s ON s.id = f.subject_id + LEFT JOIN relation_types r ON r.id = f.predicate_id + LEFT JOIN entities o ON o.id = f.object_id + WHERE v.kb_id = $1 AND v.kind = 'derived_contradiction' AND v.status = 'open' + AND (v.detail->>'subject_id' = $2::text OR v.detail->>'object_id' = $2::text) + ORDER BY v.detected_at DESC", + ) + .bind(kb_id) + .bind(entity_id) + .fetch_all(pool) + .await?) +} + +/// 没落地的派生的证明链：它的前提就在违规的 `path` 里。找不到那条违规时 `None` +pub async fn blocked_proof( + pool: &PgPool, + kb_id: Uuid, + violation_id: Uuid, +) -> AppResult>> { + let path: Option<(Vec,)> = sqlx::query_as( + "SELECT path FROM axiom_violations + WHERE id = $1 AND kb_id = $2 AND kind = 'derived_contradiction'", + ) + .bind(violation_id) + .bind(kb_id) + .fetch_optional(pool) + .await?; + match path { + None => Ok(None), + Some((p,)) => Ok(Some(steps_for(pool, &p).await?)), + } } /// 按 id 取一条派生（失效的也取：证明要能回看）。 diff --git a/crates/utopia-store/tests/a_contradiction_points_upstream.rs b/crates/utopia-store/tests/a_contradiction_points_upstream.rs index 2ff4dd13b..04c1020c3 100644 --- a/crates/utopia-store/tests/a_contradiction_points_upstream.rs +++ b/crates/utopia-store/tests/a_contradiction_points_upstream.rs @@ -225,6 +225,49 @@ async fn a_contradiction_points_upstream() -> anyhow::Result<()> { assert_eq!(card.hint.as_deref(), Some("stale")); assert_eq!(card.detail["subject"], "Mira"); + // 争议在它坐的地方可见（0017 §3）：面板行挂 contested，图上有一条幽灵边， + // 「没落地的」一档有一行，它的证明链读得出前提 + let (_, facts) = utopia_store::graph::entity_detail(&pool, f.kb, f.mira).await?; + let hit = facts + .iter() + .find(|x| x.id == old) + .expect("the assertion is on the panel"); + let c = hit + .contested + .as_ref() + .expect("the hit assertion is contested"); + assert_eq!(c["kind"], "derived_contradiction"); + assert_eq!(c["ref_id"], serde_json::json!(vid)); + assert!( + facts + .iter() + .find(|x| x.id == ceo) + .unwrap() + .contested + .is_none(), + "the premise is not the disputed one" + ); + let (_, edges) = utopia_store::graph::neighborhood(&pool, f.kb, f.mira, 1, None).await?; + let ghost = edges + .iter() + .find(|e| e.blocked) + .expect("a ghost edge for the blocked derivation"); + assert_eq!(ghost.id, *vid); + assert!(ghost.derived && ghost.contested); + assert_eq!((ghost.source, ghost.target), (f.mira, f.acme)); + assert!(edges.iter().find(|e| e.id == old).unwrap().contested); + assert!(!edges.iter().find(|e| e.id == ceo).unwrap().contested); + let blocked = reasoning::blocked_for_entity(&pool, f.kb, f.acme).await?; + assert_eq!(blocked.len(), 1); + assert_eq!(blocked[0].violation_id, *vid); + assert_eq!(blocked[0].against_fact, old); + assert_eq!(blocked[0].premises, vec![ceo]); + let steps = reasoning::blocked_proof(&pool, f.kb, *vid) + .await? + .expect("the ghost has a proof"); + assert_eq!(steps.len(), 1); + assert_eq!(steps[0].fact_id, ceo); + // 重跑幂等：还是那一行 reasoning::run(&pool, f.kb).await?; assert_eq!(open_contradictions(&pool, &f).await?.len(), 1); diff --git a/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md b/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md index 5463554c5..b35d5fd51 100644 --- a/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md +++ b/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md @@ -1,6 +1,6 @@ # 0016 · Close the open seams before cutting new ones -- **Status**: in progress · the first schedule after v0.1.0 · A1, A2, A3 done · B1 done (#227) · B2a done (#238, [0017](0017-a-contradiction-points-upstream.md)), B2b planned · B3: the signature half done (#190 / #196), cross-pack signatures and range-aware direction done (#233), `disjointWith` into resolution still open · D2's blank-base problem worked around with builtin `metric` / `dimension` classes (#231), the pack itself still planned · the lakehouse engines landed ahead of D4 (#239, [0018](0018-the-lakehouse-is-one-protocol-away.md)) +- **Status**: in progress · the first schedule after v0.1.0 · A1, A2, A3 done · B1 done (#227) · B2 done (#238 / #243, [0017](0017-a-contradiction-points-upstream.md)) · B3: the signature half done (#190 / #196), cross-pack signatures and range-aware direction done (#233), `disjointWith` into resolution still open · D2's blank-base problem worked around with builtin `metric` / `dimension` classes (#231), the pack itself still planned · the lakehouse engines landed ahead of D4 (#239, [0018](0018-the-lakehouse-is-one-protocol-away.md)) - **Written**: 2026-09-02 · condensed into English 2026-09-03 - **Related**: written after checking [0001](0001-ontology-import-and-governance.md) through [0015](0015-recording-a-sentence-is-not-asserting-a-fact.md) against the code; every item below has its source in those fifteen records, whose 2026-09-02 revision notes are the check's product. This record only orders them and says why this order. @@ -44,8 +44,8 @@ A4 README against code, both languages: promise only what has landed. **B · Finish the reasoning engine**, after A, parallel with C. B1 the R2 proof chain (done, #227; a chain, not a tree — see [0002](0002-reasoning-engine.md)). B2 the derived-vs-asserted -contradiction signal, `axiom_violations` kind `derived_contradiction` (B2a done; B2b, visibility -on graph and panel, planned — 0017). B3 `classify_type_drift` reads `entity_type_disjoint` +contradiction signal, `axiom_violations` kind `derived_contradiction` (done: B2a engine and +queue #238, B2b visibility on graph and panel #243 — 0017). B3 `classify_type_drift` reads `entity_type_disjoint` instead of the hard-coded list, today's behavior when nothing is declared (class kinship from the hierarchy landed first, #226). B4 R3 incremental maintenance, deferred until a full re-derivation of `ai-timeline-ends` exceeds a threshold diff --git a/docs/decisions/0017-a-contradiction-points-upstream.md b/docs/decisions/0017-a-contradiction-points-upstream.md index f321908d7..808c2ecd9 100644 --- a/docs/decisions/0017-a-contradiction-points-upstream.md +++ b/docs/decisions/0017-a-contradiction-points-upstream.md @@ -1,6 +1,6 @@ # 0017 · A contradiction points at an error upstream -- **Status**: B2a implemented (engine and queue: `derive::contradictions`, migration 0020, the Review card with clues and repairs) · B2b (visibility in the graph and the entity panel) still planned · B2 of 0016, wider than the one line written there: contradictions become visible everywhere, not only as a new kind in the queue +- **Status**: implemented · B2a (#238): engine and queue — `derive::contradictions`, migration 0020, the Review card with clues and repairs · B2b: contested edges in the alert colour and ghost edges for blocked derivations on the graph, the disputed chip on panel rows, the "did not land" section of the Derived tab with its proof chain · B2 of 0016, wider than the one line written there: contradictions become visible everywhere, not only as a new kind in the queue - **Written**: 2026-09-03 (conventions in [README](README.md)) - **Related**: the two unbuilt rows of the "derived vs asserted" table in [0002](0002-reasoning-engine.md) §2; [0016](0016-close-the-open-seams-before-cutting-new-ones.md) B2; the proof chain (B1, #227) supplies the "premises expand to the sentence" half of the card below diff --git a/docs/decisions/README.md b/docs/decisions/README.md index 90b28d6e5..b2e8b9811 100644 --- a/docs/decisions/README.md +++ b/docs/decisions/README.md @@ -39,8 +39,8 @@ The test for writing one: if someone (including us) looks at a piece of code in | 0013 | [A source hands over its history](0013-a-source-should-hand-over-its-history.md) | Implemented for GitHub, Jira and Notion (#134 / #135 / #213) · Feishu and Confluence not started · `instant` precision not triggered | | 0014 | [Identity from the person, scope from the token](0014-identity-from-the-person-scope-from-the-token.md) | Implemented (#180) · five read-only MCP tools over Streamable HTTP · tokens page at `/account/tokens` · `can_write` still hard-coded false | | 0015 | [A recorded sentence waits for a nod](0015-recording-a-sentence-is-not-asserting-a-fact.md) | Implemented · memory facts wait in `pending_facts`, nod queue and chat card, `remember` reopened · MCP write is the next cut | -| 0016 | [Close the open seams before cutting new ones](0016-close-the-open-seams-before-cutting-new-ones.md) | In progress · A done · B1 and B2a done, B2b and `disjointWith` open · C untouched · D2 worked around (#231); the lakehouse landed ahead of D4 (#239) | -| 0017 | [A contradiction points at an error upstream](0017-a-contradiction-points-upstream.md) | B2a implemented: engine and queue, per-item cap, aggregation by rule pair, cards with clues and repairs (#238) · B2b planned: disputes visible on the graph and in the panel | +| 0016 | [Close the open seams before cutting new ones](0016-close-the-open-seams-before-cutting-new-ones.md) | In progress · A done · B1 and B2 done, `disjointWith` open · C untouched · D2 worked around (#231); the lakehouse landed ahead of D4 (#239) | +| 0017 | [A contradiction points at an error upstream](0017-a-contradiction-points-upstream.md) | Implemented · B2a: engine and queue, per-item cap, aggregation by rule pair, cards with clues and repairs (#238) · B2b: contested edges in the alert colour, ghost edges for blocked derivations, the disputed chip and the "did not land" section in the panel (#243) | | 0018 | [The lakehouse is one protocol away](0018-the-lakehouse-is-one-protocol-away.md) | Implemented: Trino (Iceberg / Delta / Hive), Databricks and Snowflake behind the same trait, scheme picks the engine (#239) · replay tests only, real clusters wanted (#240–#242) · MaxCompute waits | ## Not a decision record diff --git a/web/src/api.ts b/web/src/api.ts index 05d28ed1d..c2775ed09 100644 --- a/web/src/api.ts +++ b/web/src/api.ts @@ -324,6 +324,24 @@ export interface DerivedFact { premises: string[]; } +/** 一条**没有落地**的派生（0017 §3）：推出来了，撞上一条断言，拦在图外。 + * 没有自己的 id，用那条违规的 id 指它——面板、幽灵边、Review 卡片三处靠它对上 */ +export interface BlockedDerivation { + violation_id: string; + subject_id: string; + subject: string; + object_id: string; + object: string; + predicate: string; + rule: string; + via_label: string; + valid_from: string | null; + valid_to: string | null; + against_fact: string; + against_text: string; + premises: string[]; +} + /** 证明的一步：一条断言前提，带它的证据。前提一律是断言，所以证明是链不是树 */ export interface ProofStep { seq: number; @@ -646,6 +664,11 @@ export interface GraphEdge { valid_from: string | null; valid_to: string | null; confidence: number; + /** 有争议（0017 §3）：有一条 open 的公理违规或时态冲突指着它。整条边画成警戒色 */ + contested: boolean; + /** 幽灵边（0017 §3）：没落地的派生。`id` 是那条 `derived_contradiction` 违规的 id； + * `derived` 同时为 true，跟着派生开关走。点它打开主语的面板 */ + blocked: boolean; } export interface EntityFact { @@ -673,6 +696,13 @@ export interface EntityFact { stale: boolean; /** 修正行：区间闭合来自引擎对账/人工裁决而非抽取原文 */ corrected: boolean; + /** 有争议（0017 §3）：哪一种、Review 里那一项的 id、派生撞断言时推出来的那句话。 + * 行不压暗——断言仍然活着 */ + contested: { + kind: string; + ref_id: string; + derived?: string | null; + } | null; /** 证据集合里最新的文档时间（开放事实的"最后确认时间"） */ last_evidence_time: string | null; } @@ -1361,6 +1391,8 @@ export const api = { /** 推出来的那些**单独一个键**，不掺进 facts：混在同一个列表里， * 用户看不出「文档里写的」和「引擎推的」的区别 */ derived: DerivedFact[]; + /** 没落地的派生（0017 §3）：连 `derived_facts` 都不在，所以也单独一个键 */ + blocked: BlockedDerivation[]; /** 同名的其他实体。**打开面板就给**——合并入口要长在能看见同名的地方， * 而不是藏在「改一次名」之后 */ same_name: GraphNode[]; @@ -1391,6 +1423,11 @@ export const api = { request<{ proof: Proof | null }>( `/api/v1/kbs/${kbId}/derived/${derivedId}/proof`, ), + /** 没落地的派生的证明链（0017 §3）：前提在违规的 path 里 */ + blockedProof: (kbId: string, violationId: string) => + request<{ steps: ProofStep[] | null }>( + `/api/v1/kbs/${kbId}/violations/${violationId}/proof`, + ), documentDetail: (id: string) => request<{ document: Doc; chunks: ChunkFull[] }>(`/api/v1/documents/${id}`), extractDocument: (id: string) => diff --git a/web/src/i18n/en.ts b/web/src/i18n/en.ts index 1be5d4365..e5fb94032 100644 --- a/web/src/i18n/en.ts +++ b/web/src/i18n/en.ts @@ -732,6 +732,19 @@ export const en = { derivedHint: "Edges no one asserted — the engine worked them out from axioms your ontology declares. Each one shows the premises it came from.", derivedNoProof: "The premises are gone.", + /* 争议（0017 §3） */ + contestedChip: "disputed", + contestedHint: (kind: string, derived: string | null) => + kind === "derived_contradiction" + ? `A derivation contradicts this assertion${derived ? `: ${derived}` : ""}. Open it under Review.` + : kind === "temporal_conflict" + ? "A newer assertion conflicts with this one in time. Open it under Review." + : "This assertion breaks an axiom the ontology declares. Open it under Review.", + blockedTitle: "Did not land", + blockedHint: + "The engine could draw these edges; an assertion stood in the way. They show on the graph as ghost edges.", + blockedBy: (t: string) => `blocked by ${t}`, + blockedReview: "Review", /** 证明链（0002 R2）：每一步是一条断言前提，展开到原句 */ proofStep: (n: number) => `Step ${n}`, proofRetracted: "since retracted", diff --git a/web/src/i18n/zh.ts b/web/src/i18n/zh.ts index 7971a3d55..73a027d66 100644 --- a/web/src/i18n/zh.ts +++ b/web/src/i18n/zh.ts @@ -674,6 +674,17 @@ export const zh: Strings = { derivedHint: "没有人断言过的边——引擎按本体声明的公理推出来的。每一条都附着它用到的前提。", derivedNoProof: "前提已经不在了。", + contestedChip: "有争议", + contestedHint: (kind: string, derived: string | null) => + kind === "derived_contradiction" + ? `有一条推出来的事实与它抵触${derived ? `：${derived}` : ""}。去 Review 看。` + : kind === "temporal_conflict" + ? "有一条更新的断言在时间上与它冲突。去 Review 看。" + : "这条断言违反了本体声明的公理。去 Review 看。", + blockedTitle: "没落地的", + blockedHint: "引擎本可以画出这些边，被一条断言挡住了。图上画成幽灵边。", + blockedBy: (t: string) => `挡住它的：${t}`, + blockedReview: "去 Review", proofStep: (n: number) => `第 ${n} 步`, proofRetracted: "后来撤了", proofLoading: "正在展开证明…", diff --git a/web/src/pages/Graph.tsx b/web/src/pages/Graph.tsx index 5f32501fa..e69a0cea8 100644 --- a/web/src/pages/Graph.tsx +++ b/web/src/pages/Graph.tsx @@ -1,4 +1,11 @@ -import { useCallback, useEffect, useMemo, useRef, useState } from "react"; +import { + useCallback, + useEffect, + useMemo, + useRef, + useState, + type MutableRefObject, +} from "react"; import { useMutation, useQuery, useQueryClient } from "@tanstack/react-query"; import { Link, useNavigate, useSearch } from "@tanstack/react-router"; import Graphology from "graphology"; @@ -34,6 +41,8 @@ import { type Evidence, type GraphEdge, type GraphNode, + type BlockedDerivation, + type ProofStep, } from "../api"; import { S } from "../i18n"; import { usePopoverFlip } from "../ui/popoverFlip"; @@ -69,6 +78,10 @@ const EDGE_COLOR_INFERRED = "rgba(163,163,163,0.1)"; // 用户要在余光里就分得出「文档里写的」和「推出来的」 const EDGE_COLOR_DERIVED = "rgba(231,197,124,0.42)"; const EDGE_COLOR_DERIVED_DIM = "rgba(231,197,124,0.14)"; +/* 争议（0017 §3）：珊瑚橙 `--u-contest`。金是派生、琥珀是警告、粉是危险， + 它得跟三个都拉开。**整条边换色**——环在节点上、边还是灰的，余光分不出来 */ +const EDGE_COLOR_CONTEST = "rgba(255,106,61,0.55)"; +const EDGE_FOCUS_CONTEST = "rgba(255,106,61,1)"; /** 相邻两条弧之间的曲率差。太小仍然糊，太大在长边上会甩得离节点很远 */ const EDGE_CURVATURE_STEP = 0.18; @@ -187,6 +200,10 @@ const NODE_BUDGETS: number[] = [150, 300, 600, 1000]; // 注意：sigma 边着色器在预乘混合(ONE, ONE_MINUS_SRC_ALPHA)下不预乘 RGB， // alpha 无法压暗边——暗度必须编码进 RGB（不透明近背景色） const EDGE_DIM = "#141414"; +/* 幽灵边：没落地的派生。同一个色相往 EDGE_DIM 混（预乘混合下 alpha 压不暗边）， + 更细。sigma 默认的边程序画不了虚线，也不为此另写一个 */ +const EDGE_GHOST = lerpColor("rgba(255,106,61,1)", EDGE_DIM, 0.55); +const EDGE_GHOST_FOCUS = lerpColor("rgba(255,106,61,1)", EDGE_DIM, 0.2); const EDGE_FOCUS = "rgba(255,255,255,0.55)"; // 选中/悬停时的派生边。**不能跟着走白**：选中恰恰是看得最仔细的时候， // 而这时候「这条边是推出来的、没人写过」比任何时候都该说清楚。 @@ -439,6 +456,8 @@ export function Graph() { 先留在原地演完退场，再真的移除。用 selectedRef 取当前值而不是把 setState 写成带副作用的 updater：那种写法在 StrictMode 下会跑两遍 */ const [exiting, setExiting] = useState(null); + // 打开面板时想停在哪一档、展开哪一行——幽灵边点进来时用 + const panelIntentRef = useRef<{ view: "derived"; open: string } | null>(null); const deselect = useCallback(() => { const cur = selectedRef.current; if (!cur) return; @@ -843,13 +862,20 @@ export function Graph() { ); for (const { edge: e, curvature, alsoLabels } of placed.edges) { g.addEdgeWithKey(e.id, e.source, e.target, { - label: e.label?.toUpperCase() ?? "", - size: 1, - color: e.derived - ? EDGE_COLOR_DERIVED - : e.inferred - ? EDGE_COLOR_INFERRED - : EDGE_COLOR, + // 争议的边标签前置 ⚠：颜色之外再给一个不靠色觉的记号 + label: (e.contested ? "⚠ " : "") + (e.label?.toUpperCase() ?? ""), + size: e.blocked ? 0.7 : 1, + color: e.blocked + ? EDGE_GHOST + : e.contested + ? EDGE_COLOR_CONTEST + : e.derived + ? EDGE_COLOR_DERIVED + : e.inferred + ? EDGE_COLOR_INFERRED + : EDGE_COLOR, + contested: e.contested, + blocked: e.blocked, // 独一条就走直线：曲线是为了把重叠分开，没有重叠就不必弯 type: curvature === 0 ? "line" : "curved", curvature, @@ -1170,16 +1196,24 @@ export function Graph() { : null; const hovNow = hoverRef.current; const focused = selNow ?? hovNow; + const ghost = attrs.blocked === true; const from = !focused - ? EDGE_COLOR_DERIVED + ? ghost + ? EDGE_GHOST + : EDGE_COLOR_DERIVED : s === focused || t === focused - ? EDGE_FOCUS_DERIVED + ? ghost + ? EDGE_GHOST_FOCUS + : EDGE_FOCUS_DERIVED : EDGE_DIM; res.color = lerpColor(from, EDGE_DIM, k); res.label = ""; return res; } - const pulse = lerpColor( + // 幽灵边不呼吸：它不是知识，是一条没走通的路 + const pulse = attrs.blocked === true + ? EDGE_GHOST + : lerpColor( EDGE_COLOR_DERIVED_DIM, EDGE_COLOR_DERIVED, // 三角波而不是正弦：两端各停一瞬，看起来是「呼吸」不是「闪」 @@ -1199,7 +1233,14 @@ export function Graph() { ? selectedRef.current : null; const boost = () => { - res.color = isDerived ? EDGE_FOCUS_DERIVED : EDGE_FOCUS; + res.color = + attrs.blocked === true + ? EDGE_GHOST_FOCUS + : attrs.contested === true + ? EDGE_FOCUS_CONTEST + : isDerived + ? EDGE_FOCUS_DERIVED + : EDGE_FOCUS; res.size = Math.max((attrs.size as number) * 1.42, 1.85); res.zIndex = 5; }; @@ -1245,6 +1286,13 @@ export function Graph() { }, }); sigma.on("clickNode", ({ node }) => setSelected(node)); + // 幽灵边点一下：打开它主语的面板，停在「推出来的」那一档、展开那一行（0017 §3） + sigma.on("clickEdge", ({ edge }) => { + if (g.getEdgeAttribute(edge, "blocked") !== true) return; + const [s] = g.extremities(edge); + panelIntentRef.current = { view: "derived", open: edge }; + setSelected(s); + }); sigma.on("doubleClickNode", ({ node, event }) => { event.preventSigmaDefault(); setFocusEntity(node); @@ -1840,6 +1888,7 @@ export function Graph() { kbId={kb.id} entityId={(selected ?? exiting)!} exiting={!selected} + intent={panelIntentRef} onClose={deselect} onNavigate={(id) => { // 跳转目标可能不在当前画布：同时把图 refocus 到它的邻域（与搜索选择一致） @@ -2515,56 +2564,7 @@ function ProofChain({ kbId, d }: { kbId: string; d: DerivedFact }) { {proof.isPending && (

{S.graph.proofLoading}

)} - {steps && ( -
    - {steps.map((st) => ( -
  1. -
    - - {S.graph.proofStep(st.seq + 1)} - - - {st.subject} - — {st.predicate ?? "?"} → - {st.object ?? "?"} - - {st.retracted && ( - {S.graph.proofRetracted} - )} -
    -
    - {st.evidence.map((ev) => ( - -
    - {ev.quote ? `“${ev.quote}”` : S.graph.noQuote} -
    -
    - {S.graph.sectionRef(ev.filename, ev.seq + 1)} - {ev.stale && ( - - {S.graph.fromVersion(ev.doc_version)} - - )} -
    - - ))} - {st.evidence.length === 0 && ( -

    {S.graph.noEvidence}

    - )} -
    -
    2. - ))} -
- )} + {steps && } {/* 派生已失效、证明取不到：退回列表里带来的那几行文本 */} {!proof.isPending && !steps && (
    @@ -2582,10 +2582,200 @@ function ProofChain({ kbId, d }: { kbId: string; d: DerivedFact }) { ); } +/** 证明的步，落了地的与没落地的派生共用：前提是同一种东西 */ +function ProofSteps({ kbId, steps }: { kbId: string; steps: ProofStep[] }) { + return ( +
      + {steps.map((st) => ( +
    1. +
      + + {S.graph.proofStep(st.seq + 1)} + + + {st.subject} + — {st.predicate ?? "?"} → + {st.object ?? "?"} + + {st.retracted && ( + {S.graph.proofRetracted} + )} +
      +
      + {st.evidence.map((ev) => ( + +
      + {ev.quote ? `“${ev.quote}”` : S.graph.noQuote} +
      +
      + {S.graph.sectionRef(ev.filename, ev.seq + 1)} + {ev.stale && ( + + {S.graph.fromVersion(ev.doc_version)} + + )} +
      + + ))} + {st.evidence.length === 0 && ( +

      {S.graph.noEvidence}

      + )} +
      +
      2. + ))} +
    + ); +} + +/** 没落地的派生（0017 §3）：像 DerivedRow 一样的一行，多一句「挡住它的是谁」， + * 展开是它的证明链——人在这里看到「引擎本可以画这条边，是什么拦住了它」 */ +function BlockedRow({ + kbId, + b, + entityId, + open, + onToggle, + onNavigate, +}: { + kbId: string; + b: BlockedDerivation; + entityId: string; + open: boolean; + onToggle: () => void; + onNavigate: (entityId: string) => void; +}) { + const navigate = useNavigate(); + const out = b.subject_id === entityId; + const otherId = out ? b.object_id : b.subject_id; + const otherName = out ? b.object : b.subject; + const proof = useQuery({ + queryKey: ["blocked-proof", b.violation_id], + queryFn: () => api.blockedProof(kbId, b.violation_id), + enabled: open, + }); + return ( +
    + +
    + + {S.graph.blockedBy(b.against_text)} + + + navigate({ + to: "/kb/$kbId/review", + params: { kbId }, + search: { queue: "violations", item: b.violation_id }, + }) + } + className="ml-auto shrink-0 text-neutral-500 hover:text-neutral-300 hover:underline underline-offset-2" + > + {S.graph.blockedReview} → + +
    + {open && ( +
    + {proof.isPending && ( +

    {S.graph.proofLoading}

    + )} + {proof.data?.steps && ( + + )} +
    + )} +
    + ); +} + +/** 争议 chip（0017 §3）：有一条 open 的违规或冲突指着这条断言。行不压暗—— + * 它仍然活着。点它去 Review 对应那一档，并把那张卡点亮 */ +function ContestedChip({ + kbId, + c, +}: { + kbId: string; + c: NonNullable; +}) { + const navigate = useNavigate(); + const queue = c.kind === "temporal_conflict" ? "conflicts" : "violations"; + return ( + { + ev.stopPropagation(); + navigate({ + to: "/kb/$kbId/review", + params: { kbId }, + search: { queue, item: c.ref_id }, + }); + }} + onKeyDown={(ev) => { + if (ev.key === "Enter") { + ev.stopPropagation(); + navigate({ + to: "/kb/$kbId/review", + params: { kbId }, + search: { queue, item: c.ref_id }, + }); + } + }} + className="u-chip u-chip-contest shrink-0 !text-[10px] !px-1.5 cursor-pointer" + title={S.graph.contestedHint(c.kind, c.derived ?? null)} + > + {S.graph.contestedChip} + + ); +} + function EntityPanel({ kbId, entityId, exiting, + intent, onClose, onNavigate, }: { @@ -2593,6 +2783,8 @@ function EntityPanel({ entityId: string; /** 正在演退场：还挂在 DOM 上，但已经不接受点击 */ exiting: boolean; + /** 打开时停在哪一档、展开哪一行；读一次就清掉 */ + intent?: MutableRefObject<{ view: "derived"; open: string } | null>; onClose: () => void; onNavigate: (entityId: string) => void; }) { @@ -2604,6 +2796,8 @@ function EntityPanel({ // 推出来的那些。**单独一个键，不掺进 facts**——混在一个列表里，用户看不出 // 「文档里写的」和「引擎推的」的区别 const derived = detail.data?.derived ?? []; + // 没落地的（0017 §3）：推出来了，撞上一条断言 + const blocked = detail.data?.blocked ?? []; /* 按「方向 + 谓词 + 规则」分组，骨架与 Relations 的 groups 一致。 规则挂在组上而不是每一行：它对整组都成立，逐行重复既冗余， 那个琥珀色小字还会跟派生边抢色相 */ @@ -2635,6 +2829,13 @@ function EntityPanel({ const [view, setView] = useState< "relations" | "timeline" | "history" | "derived" >("relations"); + useEffect(() => { + const it = intent?.current; + if (!it) return; + intent.current = null; + setView(it.view); + setOpenFact(it.open); + }, [entityId, intent]); const e: GraphNode | undefined = detail.data?.entity; @@ -2919,8 +3120,10 @@ function EntityPanel({
    {(["relations", "timeline", "history", "derived"] as const) // 推出来的那一档：**没有派生就不出现**。一个没开推理的库不该看到 - // 一个永远是空的标签页 - .filter((v) => v !== "derived" || derived.length > 0) + // 一个永远是空的标签页。没落地的也算——那正是这一档要说的事 + .filter( + (v) => v !== "derived" || derived.length > 0 || blocked.length > 0, + ) .map((v) => (
    ))} + {blocked.length > 0 && ( +
    +
    + {S.graph.blockedTitle} + + {blocked.length} + +
    +

    + {S.graph.blockedHint} +

    + {blocked.map((b) => ( + + setOpenFact( + openFact === b.violation_id ? null : b.violation_id, + ) + } + onNavigate={onNavigate} + /> + ))} +
    + )} )} {view !== "history" && @@ -3212,6 +3443,9 @@ function TimelineRow({ {S.graph.staleFactChip} )} + {fact.contested && ( + + )} {open && } @@ -3296,6 +3530,7 @@ function FactRow({ {S.graph.staleFactChip} )} + {fact.contested && } {interval && ( {interval} diff --git a/web/src/pages/Review.tsx b/web/src/pages/Review.tsx index 6ca977c25..47e7d5651 100644 --- a/web/src/pages/Review.tsx +++ b/web/src/pages/Review.tsx @@ -1,6 +1,6 @@ import { useEffect, useState } from "react"; import { useMutation, useQuery, useQueryClient } from "@tanstack/react-query"; -import { useNavigate } from "@tanstack/react-router"; +import { useNavigate, useSearch } from "@tanstack/react-router"; import { ArrowUpRight } from "lucide-react"; import { api, @@ -830,7 +830,11 @@ export function Review() { const { kb } = useKb(); const queryClient = useQueryClient(); const navigate = useNavigate(); - const [sel, setSel] = useState(null); + // 面板的争议 chip 带着 queue / item 跳过来：先落到那一档，再把那张卡点亮 + const search = useSearch({ from: "/app/kb/$kbId/review" }); + const [sel, setSel] = useState( + QUEUE_ORDER.includes(search.queue as Sel) ? (search.queue as Sel) : null, + ); const [page, setPage] = useState(0); // 队列变化经 SSE 事件流推送（useKbEvents 挂在 Shell），无需轮询。 @@ -1301,8 +1305,15 @@ export function Review() { )} {asViolations().map((v) => ( - + select("duplicates")} onOntology={() => navigate({ to: "/ontology" })} /> + ))} )} diff --git a/web/src/router.tsx b/web/src/router.tsx index 6de3aceeb..d511346e6 100644 --- a/web/src/router.tsx +++ b/web/src/router.tsx @@ -143,6 +143,13 @@ const mappingsRoute = createRoute({ const reviewRoute = createRoute({ getParentRoute: () => kbRoute, path: "review", + // 从实体面板的争议 chip 跳过来：落到对应那一档，并点亮那一张卡（0017 §3） + validateSearch: ( + search: Record, + ): { queue?: string; item?: string } => ({ + queue: typeof search.queue === "string" ? search.queue : undefined, + item: typeof search.item === "string" ? search.item : undefined, + }), component: Review, }); diff --git a/web/src/styles.css b/web/src/styles.css index 85397ce83..e6b0719c3 100644 --- a/web/src/styles.css +++ b/web/src/styles.css @@ -413,6 +413,11 @@ select.input-dark option { background: rgba(242, 182, 109, 0.12); color: var(--u-warn); } +/* 争议（0017 §3）：与图上的争议边同一个色相 */ +.u-chip-contest { + background: rgba(255, 106, 61, 0.14); + color: var(--u-contest); +} .u-chip-danger { background: rgba(255, 157, 175, 0.12); color: var(--u-danger);