Skip to content

feat(web): graph edge styling, navbar icons, shared lean index #104

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Xinze-Li-Moqian merged 1 commit into from
Jun 28, 2026
Merged

feat(web): graph edge styling, navbar icons, shared lean index #104

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 17 additions & 1 deletion web/src/components/Navbar.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,25 @@ export function Navbar() {
href="https://github.com/MathNetwork/OpenGA"
target="_blank"
rel="noopener noreferrer"
aria-label="GitHub"
title="GitHub"
className="hover:text-white/75 transition-colors"
>
GitHub
<svg width="18" height="18" viewBox="0 0 24 24" fill="currentColor" aria-hidden="true">
<path d="M12 .297c-6.63 0-12 5.373-12 12 0 5.303 3.438 9.8 8.205 11.385.6.113.82-.258.82-.577 0-.285-.01-1.04-.015-2.04-3.338.724-4.042-1.61-4.042-1.61C4.422 18.07 3.633 17.7 3.633 17.7c-1.087-.744.084-.729.084-.729 1.205.084 1.838 1.236 1.838 1.236 1.07 1.835 2.809 1.305 3.495.998.108-.776.417-1.305.76-1.605-2.665-.3-5.466-1.332-5.466-5.93 0-1.31.465-2.38 1.235-3.22-.135-.303-.54-1.523.105-3.176 0 0 1.005-.322 3.3 1.23.96-.267 1.98-.399 3-.405 1.02.006 2.04.138 3 .405 2.28-1.552 3.285-1.23 3.285-1.23.645 1.653.24 2.873.12 3.176.765.84 1.23 1.91 1.23 3.22 0 4.61-2.805 5.625-5.475 5.92.42.36.81 1.096.81 2.22 0 1.606-.015 2.896-.015 3.286 0 .315.21.69.825.57C20.565 22.092 24 17.592 24 12.297c0-6.627-5.373-12-12-12" />
</svg>
</a>
<a
href="https://discord.gg/CvfrT34ra"
target="_blank"
rel="noopener noreferrer"
aria-label="Join our Discord"
title="Join our Discord"
className="hover:text-white/75 transition-colors"
>
<svg width="22" height="18" viewBox="0 0 127.14 96.36" fill="currentColor" aria-hidden="true">
<path d="M107.7 8.07A105.15 105.15 0 0 0 81.47 0a72.06 72.06 0 0 0-3.36 6.83 97.68 97.68 0 0 0-29.11 0A72.37 72.37 0 0 0 45.64 0a105.89 105.89 0 0 0-26.25 8.09C2.79 32.65-1.71 56.6.54 80.21a105.73 105.73 0 0 0 32.17 16.15 77.7 77.7 0 0 0 6.89-11.11 68.42 68.42 0 0 1-10.85-5.18c.91-.66 1.8-1.34 2.66-2a75.57 75.57 0 0 0 64.32 0c.87.71 1.76 1.39 2.66 2a68.68 68.68 0 0 1-10.87 5.19 77 77 0 0 0 6.89 11.1 105.25 105.25 0 0 0 32.19-16.14c2.64-27.38-4.51-51.11-18.9-72.15ZM42.45 65.69C36.18 65.69 31 60 31 53s5-12.74 11.43-12.74S54 46 53.89 53s-5.05 12.69-11.44 12.69Zm42.24 0C78.41 65.69 73.25 60 73.25 53s5-12.74 11.44-12.74S96.23 46 96.12 53s-5.04 12.69-11.43 12.69Z" />
</svg>
</a>
<ThemeToggle className="hover:text-white/75 transition-colors" />
</div>
Expand Down
32 changes: 23 additions & 9 deletions web/src/panels/workspace/NetworkView.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,13 @@ import { getSortFill, parseSortFromRecord } from '@/lib/sortColors'
import { NetworkSettings } from './NetworkSettings'
import { usePluginStore } from '@/plugins/registry'

// 常规节点半径(refView 的 degreeRadius 基准值)——连线粗细以此为锚等比缩放。
const BASE_NODE_RADIUS = 8
// 连线粗细 = 常规节点半径的固定比例(世界单位),随缩放与节点同步放大。
const LINK_WIDTH_RATIO = 0.1
// 默认连线颜色:亮灰色。
const LINK_COLOR = 'rgba(200,200,210,0.5)'

// ── ref 模式箭头绘制 ──
function drawArrow(ctx: CanvasRenderingContext2D, sx: number, sy: number, tx: number, ty: number, headLen: number) {
const dx = tx - sx
Expand Down Expand Up @@ -109,7 +116,7 @@ export const NetworkView = memo(function NetworkView() {

const hoveredNode = hoveredNodeRef.current

// ── Draw links (directed arrows) ──
// ── Draw links (thin lines; arrow only on selected edges) ──
for (const link of linksRef.current) {
const s = link.source as ForceNode
const t = link.target as ForceNode
Expand All @@ -133,16 +140,20 @@ export const NetworkView = memo(function NetworkView() {
ctx.beginPath()
ctx.moveTo(ax, ay)
ctx.lineTo(bx, by)
const edgeColor = link.color || 'rgba(255,255,255,0.15)'
const edgeColor = link.color || LINK_COLOR
ctx.strokeStyle = isSelected ? 'rgba(255,255,255,0.5)' : edgeColor
ctx.lineWidth = (isSelected ? 1.5 : 0.8) / transform.k
// 线宽 = 常规节点半径 × 固定比例(世界单位),随缩放与节点同步。
ctx.lineWidth = BASE_NODE_RADIUS * LINK_WIDTH_RATIO * (isSelected ? 1.8 : 1)
if (link.dashed) ctx.setLineDash([4 / transform.k, 3 / transform.k])
ctx.stroke()
if (link.dashed) ctx.setLineDash([])

const headLen = Math.min(6 / transform.k, len * 0.3)
ctx.fillStyle = isSelected ? 'rgba(255,255,255,0.5)' : edgeColor
drawArrow(ctx, ax, ay, bx, by, headLen)
// 默认就是一条细线;方向箭头仅在选中节点的边上出现。
if (isSelected) {
const headLen = Math.min(6 / transform.k, len * 0.3)
ctx.fillStyle = 'rgba(255,255,255,0.5)'
drawArrow(ctx, ax, ay, bx, by, headLen)
}
ctx.globalAlpha = 1
}

Expand Down Expand Up @@ -435,7 +446,9 @@ export const NetworkView = memo(function NetworkView() {
}))
forceLinks = (data.edges || []).map((e: any) => ({
id: e.hash || `${e.source}-${e.target}`,
source: e.source, target: e.target, color: e.color || 'rgba(255,255,255,0.15)',
// sort(默认语义着色)下边统一灰,降噪;选了算法着色
// (community/depth/pagerank…)时保留后端算出的边色。
source: e.source, target: e.target, color: colorBy === 'sort' ? LINK_COLOR : (e.color || LINK_COLOR),
...(e.dashed ? { dashed: true } : {}),
}))
// Propagate colors to ALL atoms (not just filtered)
Expand All @@ -459,7 +472,7 @@ export const NetworkView = memo(function NetworkView() {
}))
forceLinks = refLinks.map(l => ({
id: `ref-${l.source}-${l.target}-${l.position}`,
source: l.source, target: l.target, color: 'rgba(255,255,255,0.15)',
source: l.source, target: l.target, color: LINK_COLOR,
}))
}

Expand Down Expand Up @@ -588,7 +601,8 @@ export const NetworkView = memo(function NetworkView() {
const s = typeof link.source === 'string' ? link.source : (link.source as any).id
const t = typeof link.target === 'string' ? link.target : (link.target as any).id
const updated = edgeMap[`${s}-${t}`]
if (updated) link.color = updated.color
// 与加载路径一致:sort 模式边统一灰,算法着色时用后端边色。
if (updated) link.color = colorBy === 'sort' ? LINK_COLOR : (updated.color || LINK_COLOR)
}

// Just re-render, no simulation restart
Expand Down
131 changes: 78 additions & 53 deletions web/src/plugins/leannets/EntryBlockRenderer.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,72 +9,97 @@ import { LeanCode } from './LeanHighlight'
import { LeanBadge } from './LeanBadge'
import { SORT_LABELS, parseRecord } from './utils'

/** Find the cross-source lean counterpart for a tex atom. */
interface LeanRecord { hash: string; record: Record<string, any> }
interface LeanIndex {
/** tex atom hash → its cross-source lean counterpart */
counterpart: Map<string, LeanRecord>
/** lean theorem hash → its proof entries */
proofs: Map<string, LeanRecord[]>
}

// Per-project lean index, built ONCE from a single atoms+edges fetch and shared
// by every card. Previously each card re-fetched the whole degree-1 edge set
// (megabytes) on mount, twice — the dominant source of read-view lag. Keyed by
// project path; the promise is cached so concurrent mounts dedupe to one build.
const leanIndexCache = new Map<string, Promise<LeanIndex>>()

async function buildLeanIndex(projectPath: string): Promise<LeanIndex> {
const counterpart = new Map<string, LeanRecord>()
const proofs = new Map<string, LeanRecord[]>()
const p = encodeURIComponent(projectPath)
try {
const [atomsRes, edgesRes] = await Promise.all([
fetch(`${API_BASE}/api/astrolabe/entries?path=${p}&degree=0`),
fetch(`${API_BASE}/api/astrolabe/entries?path=${p}&degree=1`),
])
const atoms: Record<string, any> = atomsRes.ok ? await atomsRes.json() : {}
const edges: Record<string, any> = edgesRes.ok ? await edgesRes.json() : {}

// Parse atom records once; index source + record for in-memory lookups.
const atomRec = new Map<string, Record<string, any>>()
for (const [h, e] of Object.entries(atoms)) {
const rec = parseRecord((e as any).record)
if (rec) atomRec.set(h, rec)
}
const isLean = (h: string) => atomRec.get(h)?.source === 'lean'

for (const edge of Object.values(edges) as any[]) {
const ref = edge.ref as string[]
if (!ref || ref.length !== 2) continue
const [a, b] = ref
// Cross-source counterpart: exactly one side is lean → map tex→lean.
const aLean = isLean(a), bLean = isLean(b)
if (aLean !== bLean) {
const leanH = aLean ? a : b
const texH = aLean ? b : a
const leanR = atomRec.get(leanH)
if (leanR && !counterpart.has(texH)) counterpart.set(texH, { hash: leanH, record: leanR })
}
// Proof edge: ref[0] is the lean theorem, sort ends in ", proof)".
if (isLean(ref[0])) {
let sort = ''
try { sort = JSON.parse(edge.record).sort || '' } catch { /* skip */ }
const proofR = sort.endsWith(', proof)') ? atomRec.get(ref[1]) : undefined
if (proofR) {
const list = proofs.get(ref[0]) ?? []
list.push({ hash: ref[1], record: proofR })
proofs.set(ref[0], list)
}
}
}
} catch { /* leave index empty on failure */ }
return { counterpart, proofs }
}

function loadLeanIndex(projectPath: string): Promise<LeanIndex> {
let cached = leanIndexCache.get(projectPath)
if (!cached) { cached = buildLeanIndex(projectPath); leanIndexCache.set(projectPath, cached) }
return cached
}

/** Find the cross-source lean counterpart for a tex atom (in-memory lookup). */
function useLeanCounterpart(hash: string, source: string | undefined, projectPath: string) {
const [leanEntry, setLeanEntry] = useState<{ hash: string; record: Record<string, any> } | null>(null)
const [leanEntry, setLeanEntry] = useState<LeanRecord | null>(null)

useEffect(() => {
if (source !== 'tex' || !hash || !projectPath) { setLeanEntry(null); return }
fetch(`${API_BASE}/api/astrolabe/entries?path=${encodeURIComponent(projectPath)}&degree=1`)
.then(r => r.ok ? r.json() : {})
.then(async (edges: Record<string, any>) => {
// Find degree-1 entry where one ref is this hash, other is a lean atom
for (const [, edge] of Object.entries(edges)) {
const ref = (edge as any).ref as string[]
if (ref.length !== 2) continue
const otherHash = ref[0] === hash ? ref[1] : ref[1] === hash ? ref[0] : null
if (!otherHash) continue
try {
const r = await fetch(`${API_BASE}/api/astrolabe/entries/${otherHash}?path=${encodeURIComponent(projectPath)}`)
if (!r.ok) continue
const otherEntry = await r.json()
if (!otherEntry?.record) continue
const parsed = parseRecord(otherEntry.record)
if (parsed?.source === 'lean') {
setLeanEntry({ hash: otherHash, record: parsed })
return
}
} catch { continue }
}
setLeanEntry(null)
})
.catch(() => setLeanEntry(null))
let alive = true
loadLeanIndex(projectPath).then(idx => { if (alive) setLeanEntry(idx.counterpart.get(hash) ?? null) })
return () => { alive = false }
}, [hash, source, projectPath])

return leanEntry
}

/** Find proof entries for a lean theorem via (theorem, proof) edges. */
/** Find proof entries for a lean theorem via (theorem, proof) edges (in-memory). */
function useLeanProofs(leanHash: string | undefined, projectPath: string) {
const [proofEntries, setProofEntries] = useState<{ hash: string; record: Record<string, any> }[]>([])
const [proofEntries, setProofEntries] = useState<LeanRecord[]>([])

useEffect(() => {
if (!leanHash || !projectPath) { setProofEntries([]); return }
fetch(`${API_BASE}/api/astrolabe/entries?path=${encodeURIComponent(projectPath)}&degree=1`)
.then(r => r.ok ? r.json() : {})
.then(async (edges: Record<string, any>) => {
const proofHashes: string[] = []
for (const [, edge] of Object.entries(edges) as [string, any][]) {
if (edge.ref[0] === leanHash) {
try {
const s = JSON.parse(edge.record).sort || ''
if (s.endsWith(', proof)')) proofHashes.push(edge.ref[1])
} catch { /* skip */ }
}
}
if (proofHashes.length === 0) { setProofEntries([]); return }
const results = await Promise.all(proofHashes.map(async h => {
try {
const r = await fetch(`${API_BASE}/api/astrolabe/entries/${h}?path=${encodeURIComponent(projectPath)}`)
if (!r.ok) return null
const e = await r.json()
if (!e?.record) return null
return { hash: h, record: parseRecord(e.record) }
} catch { return null }
}))
setProofEntries(results.filter((r): r is { hash: string; record: Record<string, any> } => r !== null))
})
.catch(() => setProofEntries([]))
let alive = true
loadLeanIndex(projectPath).then(idx => { if (alive) setProofEntries(idx.proofs.get(leanHash) ?? []) })
return () => { alive = false }
}, [leanHash, projectPath])

return proofEntries
Expand Down
Loading