sync: UI core from OpenGA web/src

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<string, any> = {
@@ -46,6 +48,11 @@ const components: Record<string, any> = {
     // Entry components
     div: ({ node, children, ...props }: any) => {
         if (node?.properties?.dataStatus) return <ProjectStatus />
+        if (node?.properties?.dataChapters) return <ProjectChapters />
+        if (node?.properties?.dataStorageTree) return <StorageTree />
+        if (node?.properties?.dataAtomExample) return <AtomExample />
+        if (node?.properties?.dataEdgeExample) return <EdgeExample />
+        if (node?.properties?.dataNumberingFlow) return <NumberingFlow />
         const entryId = node?.properties?.dataEntry
         if (entryId) {
             const collapsible = node?.properties?.dataCollapsible

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<DocFile[]>([])
+
+  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 (
+    <ul className="my-4 space-y-1.5">
+      {chapters.map((f) => (
+        <li key={f.name} className="text-[14px] text-white/70">{f.title}</li>
+      ))}
+    </ul>
+  )
+}

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 (
+    <div className="my-4 rounded-lg border border-white/10 bg-white/[0.02] p-4">
+      <div className="flex items-baseline gap-3 mb-3">
+        <span className="text-[10px] uppercase tracking-[0.2em] text-white/30">Formalization status</span>
+        <span className="inline-flex items-center gap-1.5 text-[10px] text-white/35">
+          <span className="w-1 h-1 rounded-full bg-white/50" /> live
+        </span>
+      </div>
+
+      <div className="flex mb-1">
+        <div className="pr-8">
+          <div className="text-2xl text-white/90 tabular-nums leading-none">{open.length}</div>
+          <div className="text-[10px] uppercase tracking-[0.15em] text-white/30 mt-1.5">Open sorries</div>
+        </div>
+        <div className="px-8 border-l border-white/10">
+          <div className="text-2xl text-white/90 tabular-nums leading-none">{lean.length}</div>
+          <div className="text-[10px] uppercase tracking-[0.15em] text-white/30 mt-1.5">Declarations</div>
+        </div>
+      </div>
+
+      <p className="text-[11px] leading-relaxed text-white/30 mt-3">
+        Counts only what is written in Lean so far — a live tally of open
+        <code className="mx-1 bg-white/10 text-cyan-400 px-1 py-0.5 rounded text-[10px] font-mono">sorry</code>s,
+        not a completion percentage.
+      </p>
+    </div>
+  )
+}

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 }) => (
+  <span className="text-cyan-300/80">{children}</span>
+)
+const Num = ({ children }: { children: React.ReactNode }) => (
+  <span className="text-[#e67e22]">{children}</span>
+)
+const Dim = ({ children }: { children: React.ReactNode }) => (
+  <span className="text-white/30">{children}</span>
+)
+
+/** The one-file-per-node storage layout. */
+export function StorageTree() {
+  return (
+    <figure className="my-8">
+      <pre className="rounded-lg border border-white/10 bg-white/[0.02] p-5 text-[13px] leading-relaxed font-mono text-white/55 overflow-x-auto">
+        <div><Dim>.astrolabe/</Dim></div>
+        <div>├─ atoms/</div>
+        <div>│  ├─ <Hash>38c99016b279</Hash>.md{'   '}<Dim>← one file per node</Dim></div>
+        <div>│  └─ <Hash>097d60abf481</Hash>.md</div>
+        <div>├─ edges/</div>
+        <div>│  └─ <Hash>014c1e2a49fe</Hash>.md{'   '}<Dim>← a (lean, tex) bridge</Dim></div>
+        <div>└─ docs/</div>
+        <div>{'   '}├─ 00-index.mdx</div>
+        <div>{'   '}└─ 03-geodesics.mdx{'  '}<Dim>composes nodes by hash</Dim></div>
+      </pre>
+      <figcaption className="mt-2 text-[13px] text-white/35">
+        Every node is a single file named by its hash; documents only reference them.
+      </figcaption>
+    </figure>
+  )
+}
+
+/** 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 (
+    <div className={`flex gap-2 ${pad}`}>
+      <span className="w-14 shrink-0 text-white/35">{k}</span>
+      <span className="text-white/65 min-w-0 break-words">{v}</span>
+    </div>
+  )
+}
+
+/** 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) ? (
+      <div key={k}>
+        <div className={`${depth >= 2 ? 'pl-10' : 'pl-5'} text-white/35`}>{k}</div>
+        {renderFields(v, depth + 1)}
+      </div>
+    ) : (
+      <Field key={k} k={k} v={v} depth={depth} />
+    ),
+  )
+}
+
+/** 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 (
+    <figure className="my-5">
+      <div className="rounded-lg border border-white/10 bg-white/[0.02] p-4 text-[12px] font-mono leading-relaxed">
+        <Field k="hash" v={<Hash>{hash}</Hash>} />
+        <Field k="ref" v={<>[ <Hash>{refs.join(', ')}</Hash> ]{badge && <Dim>{'  ← '}{badge}</Dim>}</>} />
+        <div className="text-white/35 mt-0.5">record</div>
+        {renderFields(record, 1)}
+      </div>
+    </figure>
+  )
+}
+
+/** A real atom from the Riemannian Geometry project. */
+export function AtomExample() {
+  return (
+    <NodeEntry
+      hash="38c99016b279"
+      refs={['38c99016b279']}
+      record={[
+        ['sort', <>(ref[0].source)<Dim>{'  = (tex)'}</Dim></>],
+        ['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 (
+    <NodeEntry
+      hash="014c1e2a49fe"
+      refs={['264fbf8cb406', '6e6c552589c3']}
+      record={[
+        ['sort', <>(ref[0].source, ref[1].source)<Dim>{'  = (lean, tex)'}</Dim></>],
+        ['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 (
+    <figure className="my-8">
+      <div className="rounded-lg border border-white/10 bg-white/[0.02] p-5 text-[13px] font-mono">
+        <div className="flex items-center gap-2 mb-4 text-white/45">
+          03-geodesics.mdx <Dim>→ chapter 3</Dim>
+        </div>
+        <div className="space-y-2.5">
+          {rows.map(([h, kind, n]) => (
+            <div key={h} className="flex items-center gap-3 whitespace-nowrap">
+              <Hash>{h}…</Hash>
+              <Dim>{kind} · first appears</Dim>
+              <span className="text-white/25">→</span>
+              <Num>{n}</Num>
+            </div>
+          ))}
+          <div className="flex items-center gap-3 whitespace-nowrap pt-1.5 border-t border-white/[0.07]">
+            <Hash>a1f3c9e2…</Hash>
+            <Dim>appears again</Dim>
+            <span className="text-white/25">→</span>
+            <Num>3.2.1</Num>
+            <Dim>(same hash, same number)</Dim>
+          </div>
+        </div>
+      </div>
+      <figcaption className="mt-2 text-[13px] text-white/35">
+        The number is assigned on first occurrence and follows the hash — never stored,
+        always consistent within the project.
+      </figcaption>
+    </figure>
+  )
+}

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, '<div data-status="true"></div>')
+    // \chapters → a live chapter list (derived from the project's docs)
+    result = result.replace(/\\chapters\b/g, '<div data-chapters="true"></div>')
+    // data-model schematic diagrams
+    result = result.replace(/\\storageTree\b/g, '<div data-storage-tree="true"></div>')
+    result = result.replace(/\\atomExample\b/g, '<div data-atom-example="true"></div>')
+    result = result.replace(/\\edgeExample\b/g, '<div data-edge-example="true"></div>')
+    result = result.replace(/\\numberingFlow\b/g, '<div data-numbering-flow="true"></div>')
     return result
 }