From 17b7f1a1ef818f6e7c18e32b513a4d7d576df399 Mon Sep 17 00:00:00 2001 From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com> Date: Tue, 30 Jun 2026 02:18:54 +0000 Subject: [PATCH] sync: UI core from OpenGA web/src --- src/components/MarkdownRenderer.tsx | 7 ++ src/components/ProjectChapters.tsx | 39 ++++++ src/components/ProjectStatus.tsx | 55 +++++++++ src/components/mdx/DataModelDiagrams.tsx | 147 +++++++++++++++++++++++ src/components/mdx/preprocess.ts | 7 ++ 5 files changed, 255 insertions(+) create mode 100644 src/components/ProjectChapters.tsx create mode 100644 src/components/ProjectStatus.tsx create mode 100644 src/components/mdx/DataModelDiagrams.tsx diff --git a/src/components/MarkdownRenderer.tsx b/src/components/MarkdownRenderer.tsx index 57de067..1f87435 100644 --- a/src/components/MarkdownRenderer.tsx +++ b/src/components/MarkdownRenderer.tsx @@ -18,6 +18,8 @@ import { InlineMath } from './mdx/InlineMath' import { EntryBlock } from './mdx/EntryBlock' import { EntryLink } from './mdx/EntryLink' import { ProjectStatus } from './ProjectStatus' +import { ProjectChapters } from './ProjectChapters' +import { StorageTree, AtomExample, EdgeExample, NumberingFlow } from './mdx/DataModelDiagrams' // eslint-disable-next-line @typescript-eslint/no-explicit-any const components: Record = { @@ -46,6 +48,11 @@ const components: Record = { // Entry components div: ({ node, children, ...props }: any) => { if (node?.properties?.dataStatus) return + if (node?.properties?.dataChapters) return + if (node?.properties?.dataStorageTree) return + if (node?.properties?.dataAtomExample) return + if (node?.properties?.dataEdgeExample) return + if (node?.properties?.dataNumberingFlow) return const entryId = node?.properties?.dataEntry if (entryId) { const collapsible = node?.properties?.dataCollapsible diff --git a/src/components/ProjectChapters.tsx b/src/components/ProjectChapters.tsx new file mode 100644 index 0000000..22bd98a --- /dev/null +++ b/src/components/ProjectChapters.tsx @@ -0,0 +1,39 @@ +'use client' + +import { useEffect, useState } from 'react' +import { API_BASE } from '@/lib/apiBase' + +interface DocFile { name: string; title: string } + +/** Live chapter list for the current project, derived from the docs in the + * store (the same source the sidebar uses) — so it never goes stale when a + * chapter is added, removed, or renamed. Rendered wherever the `\chapters` + * macro appears. */ +export function ProjectChapters() { + const [files, setFiles] = useState([]) + + useEffect(() => { + const path = typeof window !== 'undefined' + ? new URLSearchParams(window.location.search).get('path') + : null + if (!path) return + let alive = true + fetch(`${API_BASE}/api/docs/list?path=${encodeURIComponent(path)}`) + .then((r) => (r.ok ? r.json() : { files: [] })) + .then((data) => { if (alive) setFiles(data.files || []) }) + .catch(() => {}) + return () => { alive = false } + }, []) + + // Drop the index page itself; keep the ordered chapter docs. + const chapters = files.filter((f) => !/(^|\/)(00-index|index|_index)\.mdx?$/.test(f.name)) + if (chapters.length === 0) return null + + return ( +
    + {chapters.map((f) => ( +
  • {f.title}
    • + ))} +
+ ) +} diff --git a/src/components/ProjectStatus.tsx b/src/components/ProjectStatus.tsx new file mode 100644 index 0000000..5d72b0e --- /dev/null +++ b/src/components/ProjectStatus.tsx @@ -0,0 +1,55 @@ +'use client' + +import { useDataStore } from '@/stores/dataStore' + +interface LeanRec { name?: string; title?: string; sort?: string; state?: string; file?: string; line?: number } + +/** Live formalization status for the current project, computed from the store + * already loaded in memory (no extra fetch). The single source of truth is each + * lean node's `state` field, so the numbers never go stale. Rendered in the + * project reader wherever the `\status` macro appears. */ +export function ProjectStatus() { + const objects = useDataStore((s) => s.objects) + + const lean: LeanRec[] = [] + for (const o of objects) { + let r: any = o + const rec = (o as any).record + if (typeof rec === 'string') { + try { r = JSON.parse(rec) } catch { continue } + } + if (r?.source !== 'lean') continue + lean.push(r) + } + const open = lean + .filter((r) => r.state === 'sorry') + .sort((a, b) => (a.name || '').localeCompare(b.name || '')) + + return ( +
+
+ Formalization status + + live + +
+ +
+
+
{open.length}
+
Open sorries
+
+
+
{lean.length}
+
Declarations
+
+
+ +

+ Counts only what is written in Lean so far — a live tally of open + sorrys, + not a completion percentage. +

+
+ ) +} diff --git a/src/components/mdx/DataModelDiagrams.tsx b/src/components/mdx/DataModelDiagrams.tsx new file mode 100644 index 0000000..cf03d24 --- /dev/null +++ b/src/components/mdx/DataModelDiagrams.tsx @@ -0,0 +1,147 @@ +// Hand-authored schematic diagrams for the docs — pure presentational, no deps. +// Styled to the site: monochrome + hairlines, mono cyan for hashes, the Astrolabe +// orange for assigned numbers. Used from MDX via the route's components map. + +const Hash = ({ children }: { children: React.ReactNode }) => ( + {children} +) +const Num = ({ children }: { children: React.ReactNode }) => ( + {children} +) +const Dim = ({ children }: { children: React.ReactNode }) => ( + {children} +) + +/** The one-file-per-node storage layout. */ +export function StorageTree() { + return ( +
+ 
+        
.astrolabe/

+        
├─ atoms/

+        
│  ├─ 38c99016b279.md{'   '}← one file per node

+        
│  └─ 097d60abf481.md

+        
├─ edges/

+        
│  └─ 014c1e2a49fe.md{'   '}← a (lean, tex) bridge

+        
└─ docs/

+        
{'   '}├─ 00-index.mdx

+        
{'   '}└─ 03-geodesics.mdx{'  '}composes nodes by hash

+
+
+ Every node is a single file named by its hash; documents only reference them. +
+
+ ) +} + +/** One row of an entry: a fixed-width key and its value, at an indent depth. */ +function Field({ k, v, depth = 0 }: { k: string; v: React.ReactNode; depth?: number }) { + const pad = depth >= 2 ? 'pl-10' : depth === 1 ? 'pl-5' : '' + return ( +
+ {k} + {v} +
+ ) +} + +/** Render record fields, descending into a nested group when the value is an array. */ +function renderFields(entries: any[], depth: number): React.ReactNode { + return entries.map(([k, v]) => + Array.isArray(v) ? ( +
+
= 2 ? 'pl-10' : 'pl-5'} text-white/35`}>{k}
+ {renderFields(v, depth + 1)} +
+ ) : ( + + ), + ) +} + +/** An entry in the canonical (hash, ref, record) shape — everything but ref and + * hash lives, layered, inside record. */ +function NodeEntry({ hash, refs, record }: { hash: string; refs: string[]; record: any[] }) { + const badge = refs.length === 1 ? 'self-reference → atom' : refs.length === 2 ? 'two atoms → edge' : '' + return ( +
+
+ {hash}} /> + [ {refs.join(', ')} ]{badge && {' ← '}{badge}}} /> +
record
+ {renderFields(record, 1)} +
+
+ ) +} + +/** A real atom from the Riemannian Geometry project. */ +export function AtomExample() { + return ( + (ref[0].source){' = (tex)'}], + ['source', 'tex'], + ['content', [ + ['title', 'Geodesic sphere'], + ['notes', String.raw`$S_\delta = \exp_p(\{v : \lVert v\rVert = \delta\})$`], + ]], + ]} + /> + ) +} + +/** A real (lean, tex) cross-source edge. */ +export function EdgeExample() { + return ( + (ref[0].source, ref[1].source){' = (lean, tex)'}], + ['rel', 'formalizes'], + ]} + /> + ) +} + +/** How a hash gets its derived number from its first appearance in a document. */ +export function NumberingFlow() { + const rows: [string, string, string][] = [ + ['a1f3c9e2', 'Definition', '3.2.1'], + ['9c2e0f81', 'Theorem', '3.2.2'], + ['4e7d22b0', 'Corollary', '3.2.3'], + ] + return ( +
+
+
+ 03-geodesics.mdx → chapter 3 +
+
+ {rows.map(([h, kind, n]) => ( +
+ {h}… + {kind} · first appears + → + {n} +
+ ))} +
+ a1f3c9e2… + appears again + → + 3.2.1 + (same hash, same number) +
+
+
+
+ The number is assigned on first occurrence and follows the hash — never stored, + always consistent within the project. +
+
+ ) +} diff --git a/src/components/mdx/preprocess.ts b/src/components/mdx/preprocess.ts index 9c7ccd1..b6a1fce 100644 --- a/src/components/mdx/preprocess.ts +++ b/src/components/mdx/preprocess.ts @@ -16,6 +16,13 @@ export function preprocess(content: string, numbering?: Numbering): string { result = processEntryBlocks(result, numbering) // \status → a live formalization-status block (rendered from the in-memory store) result = result.replace(/\\status\b/g, '
') + // \chapters → a live chapter list (derived from the project's docs) + result = result.replace(/\\chapters\b/g, '
') + // data-model schematic diagrams + result = result.replace(/\\storageTree\b/g, '
') + result = result.replace(/\\atomExample\b/g, '
') + result = result.replace(/\\edgeExample\b/g, '
') + result = result.replace(/\\numberingFlow\b/g, '
') return result }