Kernel-Science · Gabrielebattimelli · Jun 2, 2026 · Apr 29, 2026 · May 26, 2026 · May 26, 2026
diff --git a/.gitignore b/.gitignore
@@ -41,3 +41,16 @@ frontend/out/
 
 ### Vector DB ###
 chroma/
+
+### Database exports ###
+*.dump
+*.zip
+
+### Paper drafts ###
+paper/
+
+### Screenshots ###
+Capture-*.png
+
+### pnpm (project uses npm) ###
+pnpm-lock.yaml
diff --git a/README_DB.md b/README_DB.md
@@ -0,0 +1,47 @@
+# Istruzioni per il ripristino del database
+
+Questo archivio contiene due componenti del database di LeanSearch:
+
+- `physlibsearch.dump` — dump del database PostgreSQL
+- `chroma/` — cartella del database vettoriale ChromaDB
+
+---
+
+## Requisiti
+
+- PostgreSQL 18
+- Python 3.13+ con ChromaDB installato (tramite `uv sync`)
+
+---
+
+## 1. Ripristino PostgreSQL
+
+Crea un nuovo database e ripristina il dump:
+
+```bash
+createdb physlibsearch
+pg_restore -U <tuo_utente> -d physlibsearch physlibsearch.dump
+```
+
+Poi aggiorna la stringa di connessione nel file `.env`:
+
+```
+CONNECTION_STRING = "dbname=physlibsearch user=<tuo_utente> password=<tua_password>"
+```
+
+## 2. Ripristino ChromaDB
+
+Copia la cartella `chroma/` nella radice del progetto LeanSearch (accanto al file `.env`).
+La variabile `CHROMA_PATH = "chroma"` nel file `.env` punta già a questa posizione, quindi non serve modificarla.
+
+## 3. Variabili d'ambiente
+
+Crea il file `.env` nella radice del progetto e compila almeno queste variabili:
+
+```
+JIXIA_PATH = "/percorso/al/binario/jixia"
+LEAN_SYSROOT = "/percorso/al/toolchain/lean4"
+CONNECTION_STRING = "dbname=physlibsearch user=<tuo_utente> password=<tua_password>"
+GEMINI_API_KEY = "<tua_chiave_api>"
+CHROMA_PATH = "chroma"
+```
diff --git a/changelog/2026-04-15.md b/changelog/2026-04-15.md
@@ -0,0 +1,183 @@
+# Changelog — 2026-04-15
+
+A batch of frontend improvements to PhyslibSearch covering dark mode, submodule navigation, improved declaration display, and better linking throughout the UI.
+
+---
+
+## 1. Dark Mode Support
+
+**Files changed:**
+- `frontend/package.json` — added `next-themes ^0.4.6`
+- `frontend/src/app/providers.tsx` *(new)*
+- `frontend/src/components/ThemeSwitch.tsx` *(new)*
+- `frontend/src/app/layout.tsx`
+
+### What was added
+
+Dark mode is now a first-class feature of the app, powered by the [`next-themes`](https://github.com/pacocoursey/next-themes) library.
+
+**`providers.tsx`** — a new client-side wrapper component that puts `ThemeProvider` at the root of the React tree:
+
+```tsx
+<ThemeProvider attribute="class" defaultTheme="light">
+  {children}
+</ThemeProvider>
+```
+
+`attribute="class"` means the theme is applied by toggling a `dark` class on the `<html>` element, which is the standard approach for Tailwind CSS dark mode. `defaultTheme="light"` ensures the app starts in light mode until the user's preference is saved.
+
+**`ThemeSwitch.tsx`** — a small toggle button rendered in the header that switches between light and dark:
+
+- Uses `useTheme()` from `next-themes` to read and set the current theme.
+- Renders a `Sun` icon in dark mode and a `Moon` icon in light mode (from `lucide-react`).
+- Guards its render with a `mounted` state flag to avoid a hydration mismatch: on the server there is no theme yet, so the component renders an invisible placeholder of the same size until the client mounts and resolves the real theme.
+
+**`layout.tsx`** — the root layout was updated in three ways:
+1. Children are now wrapped in `<Providers>` so `ThemeProvider` is available everywhere.
+2. `suppressHydrationWarning` was added to `<html>` — required by `next-themes` because it injects a theme attribute server-side that differs from what React expects, causing a harmless but noisy console warning without the suppression.
+3. `className="bg-background text-foreground"` was added to `<body>` so that Tailwind's semantic colour tokens (which flip automatically between light/dark) are applied to the page background and default text colour from the very first paint.
+
+---
+
+## 2. Header: Dark Mode Toggle
+
+**File changed:** `frontend/src/components/Header.tsx`
+
+A thin vertical divider and the `ThemeSwitch` button were appended to the right side of the header bar, after the existing "physlib.io ↗" external link.
+
+```tsx
+<span className="w-px h-4 bg-foreground/15 shrink-0" />
+<ThemeSwitch />
+```
+
+The divider is a `1px` wide `<span>` that visually separates the navigation links from the toggle button. Both the divider and the button use `foreground/` opacity tokens so they automatically adapt their colour in light and dark mode without any extra logic.
+
+---
+
+## 3. Browse Page: Submodule Navigation
+
+**File changed:** `frontend/src/app/browse/[...slug]/page.tsx`
+
+### Problem
+
+Previously, visiting a namespace like `/browse/Mathlib/Algebra` would only list declarations directly in that module. It had no way to navigate further down — users could not discover what child namespaces existed.
+
+### Solution
+
+The page now fetches the full list of all modules in parallel with the declarations for the current path:
+
+```tsx
+const [declarations, allModules] = await Promise.all([
+  getModuleDeclarations(moduleName),
+  listModules(),
+]);
+```
+
+A new pure function `getDirectChildren` computes which immediate child namespaces exist under the current path:
+
+```ts
+function getDirectChildren(modules, prefix) {
+  const childMap = new Map();
+  for (const m of modules) {
+    if (m.name.length > prefix.length && prefix.every((part, i) => m.name[i] === part)) {
+      const childName = m.name[prefix.length];
+      childMap.set(childName, (childMap.get(childName) ?? 0) + m.count);
+    }
+  }
+  return Array.from(childMap.entries())
+    .map(([name, count]) => ({ name, fullPath: [...prefix, name], count }))
+    .sort((a, b) => a.name.localeCompare(b.name));
+}
+```
+
+It walks every module, keeps only those whose name *starts with* the current prefix and has at least one more segment, then groups them by the *next* segment (the immediate child name). The count for each child is the sum of all declarations across all sub-namespaces under it — a useful "size hint" displayed on the right of each row.
+
+### UI
+
+When submodules exist they are rendered in a bordered card list above the declarations:
+
+```
+Submodules
+┌──────────────────────────────┐
+│ Algebra              1,204   │
+│ Analysis               873   │
+│ Topology               541   │
+└──────────────────────────────┘
+```
+
+Each row is a `<Link>` to `/browse/<full-path>`, styled with a hover highlight and a monospace font. A section heading labelled **Declarations** is added above the declaration list whenever submodules are also present, so the two sections are clearly separated.
+
+The subtitle under the module name was also updated to show both counts:
+
+```
+1,204 declarations · 6 submodules
+```
+
+---
+
+## 4. DeclarationItem: Physlib Docs Links + Value Display
+
+**File changed:** `frontend/src/components/DeclarationItem.tsx`
+
+### Doc links
+
+Previously the `#anchor` link next to each declaration name was a fragment-only link (`href="#<anchor>"`), which did nothing useful — it just scrolled to the top of the page.
+
+A new helper `docUrl` now generates a real link to the corresponding page in the Physlib documentation site:
+
+```ts
+function docUrl(moduleName: string[], name: string[]): string {
+  const path = moduleName.join("/");
+  const anchor = name.join(".");
+  return `https://physlib.io/docs/${path}.html#${anchor}`;
+}
+```
+
+The link opens in a new tab (`target="_blank"` with `rel="noopener noreferrer"` for security). Users can now jump directly from a search result to the canonical documentation for any declaration.
+
+### Value display
+
+When a user expands a declaration to see its signature, the declaration's `value` field (the right-hand side of a definition, i.e. `:= ...`) is now shown below the type signature when it is present:
+
+```
+theorem Foo.bar : α → β
+:=
+fun x => ...
+```
+
+This is appended to the existing `<pre>` block with a `:=\n` separator, matching Lean 4 syntax. It only appears when `record.value != null`, so pure `theorem` / `axiom` declarations (which have no value) are unaffected.
+
+---
+
+## 5. ResultCard: Clickable Module Breadcrumb
+
+**File changed:** `frontend/src/components/ResultCard.tsx`
+
+The module name breadcrumb displayed under each search result title was previously a purely decorative `<div>`. It is now an `<a>` tag that links to the corresponding browse page:
+
+```tsx
+<a
+  href={`/browse/${record.module_name.join("/")}`}
+  className="flex items-center gap-1 mt-1 flex-wrap hover:text-foreground/70 transition-colors"
+>
+  {/* breadcrumb segments */}
+</a>
+```
+
+Clicking `Mathlib › Algebra › Group › Basic` on a result card navigates directly to `/browse/Mathlib/Algebra/Group/Basic`. A subtle hover colour transition provides visual affordance that the breadcrumb is interactive.
+
+---
+
+## Summary of files changed
+
+| File | Change type | Description |
+|---|---|---|
+| `frontend/package.json` | Dependency | Added `next-themes ^0.4.6` |
+| `frontend/package-lock.json` | Lock file | Updated to include `next-themes` |
+| `frontend/src/app/providers.tsx` | New file | `ThemeProvider` wrapper component |
+| `frontend/src/components/ThemeSwitch.tsx` | New file | Light/dark toggle button for the header |
+| `frontend/src/app/layout.tsx` | Modified | Wrap app in `Providers`, add hydration suppression, semantic body classes |
+| `frontend/src/components/Header.tsx` | Modified | Added divider + `ThemeSwitch` to header right side |
+| `frontend/src/app/browse/[...slug]/page.tsx` | Modified | Submodule navigation: fetch + render child namespaces |
+| `frontend/src/components/DeclarationItem.tsx` | Modified | Real doc links to physlib.io, show declaration value when expanded |
+| `frontend/src/components/ResultCard.tsx` | Modified | Module breadcrumb is now a clickable link to the browse page |
diff --git a/database/__main__.py b/database/__main__.py
@@ -8,9 +8,9 @@
 
 dotenv.load_dotenv()
 logging.basicConfig(
-    filename=os.environ["LOG_FILENAME"] or None,
-    filemode=os.environ["LOG_FILEMODE"],
-    level=os.environ["LOG_LEVEL"],
+    filename=os.environ.get("LOG_FILENAME") or None,
+    filemode=os.environ.get("LOG_FILEMODE", "a"),
+    level=os.environ.get("LOG_LEVEL", "INFO"),
 )
 jixia.run.executable = os.environ["JIXIA_PATH"]
 

diff --git a/frontend/public/robots.txt b/frontend/public/robots.txt
@@ -0,0 +1,4 @@
+User-agent: *
+Allow: /
+
+Sitemap: https://physlibsearch.net/sitemap.xml
diff --git a/frontend/src/app/browse/[...slug]/page.tsx b/frontend/src/app/browse/[...slug]/page.tsx
@@ -7,6 +7,7 @@ import Header from "@/components/Header";
 import Footer from "@/components/Footer";
 import BrowseSidebar from "@/components/BrowseSidebar";
 import MobileKindFilter from "@/components/MobileKindFilter";
+import ModuleDocstring from "@/components/ModuleDocstring";
 import type { ModuleInfo, DeclarationKind } from "@/types";
 
 interface Props {
@@ -106,11 +107,7 @@ export default async function ModulePage({ params, searchParams }: Props) {
               <h1 className="text-2xl font-bold tracking-tight font-mono break-all">
                 {moduleName.join(".")}
               </h1>
-              {moduleDocstring && (
-                <p className="text-foreground/70 text-sm mt-2 leading-relaxed whitespace-pre-wrap">
-                  {moduleDocstring}
-                </p>
-              )}
+              {moduleDocstring && <ModuleDocstring text={moduleDocstring} />}
               <p className="text-foreground/40 text-sm mt-1">
                 {filteredDeclarations.length} declaration
                 {filteredDeclarations.length !== 1 ? "s" : ""}

diff --git a/frontend/src/app/sitemap.ts b/frontend/src/app/sitemap.ts
@@ -0,0 +1,42 @@
+import type { MetadataRoute } from "next";
+import { listModules } from "@/lib/api";
+
+const BASE_URL = "https://physlibsearch.net";
+
+export default async function sitemap(): Promise<MetadataRoute.Sitemap> {
+  const staticRoutes: MetadataRoute.Sitemap = [
+    {
+      url: BASE_URL,
+      lastModified: new Date(),
+      changeFrequency: "weekly",
+      priority: 1,
+    },
+    {
+      url: `${BASE_URL}/browse`,
+      lastModified: new Date(),
+      changeFrequency: "weekly",
+      priority: 0.8,
+    },
+    {
+      url: `${BASE_URL}/docs`,
+      lastModified: new Date(),
+      changeFrequency: "monthly",
+      priority: 0.7,
+    },
+  ];
+
+  let moduleRoutes: MetadataRoute.Sitemap = [];
+  try {
+    const modules = await listModules();
+    moduleRoutes = modules.map((m) => ({
+      url: `${BASE_URL}/browse/${m.name.join("/")}`,
+      lastModified: new Date(),
+      changeFrequency: "weekly" as const,
+      priority: 0.5,
+    }));
+  } catch {
+    // If the API is unavailable at build time, skip module routes
+  }
+
+  return [...staticRoutes, ...moduleRoutes];
+}
diff --git a/frontend/src/components/ModuleDocstring.tsx b/frontend/src/components/ModuleDocstring.tsx
@@ -0,0 +1,49 @@
+"use client";
+
+import LatexText from "./LatexText";
+
+interface Props {
+  text: string;
+}
+
+function Paragraph({ text }: { text: string }) {
+  const lines = text.trim().split("\n");
+  const first = lines[0];
+
+  const h3 = first.match(/^### (.+)/);
+  if (h3) return <h3 className="font-semibold text-foreground/80 text-sm mt-3">{h3[1]}</h3>;
+
+  const h2 = first.match(/^## (.+)/);
+  if (h2) return <h2 className="font-semibold text-foreground/85 mt-3 first:mt-0">{h2[1]}</h2>;
+
+  const h1 = first.match(/^# (.+)/);
+  if (h1) return <h2 className="font-semibold text-foreground/90 mt-3 first:mt-0">{h1[1]}</h2>;
+
+  const isAllBullets = lines.every((l) => l.startsWith("- "));
+  if (isAllBullets) {
+    return (
+      <ul className="list-disc list-inside space-y-0.5">
+        {lines.map((l, i) => (
+          <li key={i} className="text-foreground/70">
+            <LatexText text={l.slice(2)} />
+          </li>
+        ))}
+      </ul>
+    );
+  }
+
+  return (
+    <p className="text-foreground/70">
+      <LatexText text={text.trim()} />
+    </p>
+  );
+}
+
+export default function ModuleDocstring({ text }: Props) {
+  const paragraphs = text.split(/\n{2,}/);
+  return (
+    <div className="text-sm leading-relaxed space-y-2 mt-2">
+      {paragraphs.map((p, i) => p.trim() && <Paragraph key={i} text={p.trim()} />)}
+    </div>
+  );
+}