diff --git a/.gitignore b/.gitignore index 206eaad..21eb149 100644 --- 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 new file mode 100644 index 0000000..6ea98ec --- /dev/null +++ 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 -d physlibsearch physlibsearch.dump +``` + +Poi aggiorna la stringa di connessione nel file `.env`: + +``` +CONNECTION_STRING = "dbname=physlibsearch user= 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= password=" +GEMINI_API_KEY = "" +CHROMA_PATH = "chroma" +``` diff --git a/changelog/2026-04-15.md b/changelog/2026-04-15.md new file mode 100644 index 0000000..d75b8fe --- /dev/null +++ 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 + + {children} + +``` + +`attribute="class"` means the theme is applied by toggling a `dark` class on the `` 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 `` so `ThemeProvider` is available everywhere. +2. `suppressHydrationWarning` was added to `` — 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 `` 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 + + +``` + +The divider is a `1px` wide `` 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 `` to `/browse/`, 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="#"`), 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 `
` 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 `
`. It is now an `` tag that links to the corresponding browse page:
+
+```tsx
+
+  {/* breadcrumb segments */}
+
+```
+
+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
index 0bd478e..5102d9d 100644
--- 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
new file mode 100644
index 0000000..9aa6b3c
--- /dev/null
+++ 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
index c95f5ee..dbbc5c0 100644
--- 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) {
               

                 {moduleName.join(".")}
               

-              {moduleDocstring && (
-                

-                  {moduleDocstring}
-                

-              )}
+              {moduleDocstring && }
               

                 {filteredDeclarations.length} declaration
                 {filteredDeclarations.length !== 1 ? "s" : ""}
diff --git a/frontend/src/app/sitemap.ts b/frontend/src/app/sitemap.ts
new file mode 100644
index 0000000..c8214b5
--- /dev/null
+++ 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 {
+  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
new file mode 100644
index 0000000..8786afb
--- /dev/null
+++ 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[1]}
;
+
+  const h2 = first.match(/^## (.+)/);
+  if (h2) return 
{h2[1]}
;
+
+  const h1 = first.match(/^# (.+)/);
+  if (h1) return 
{h1[1]}
;
+
+  const isAllBullets = lines.every((l) => l.startsWith("- "));
+  if (isAllBullets) {
+    return (
+      
    
+        {lines.map((l, i) => (
+          
  • 
+            
+          
    • 
+        ))}
+      

+    );
+  }
+
+  return (
+    

+      
+    

+  );
+}
+
+export default function ModuleDocstring({ text }: Props) {
+  const paragraphs = text.split(/\n{2,}/);
+  return (
+    

+      {paragraphs.map((p, i) => p.trim() && )}
+    

+  );
+}
diff --git a/server.py b/server.py
index 23a5220..4279821 100644
--- a/server.py
+++ b/server.py
@@ -9,7 +9,7 @@
 from psycopg.rows import scalar_row, class_row
 from psycopg.types.json import Jsonb
 from psycopg_pool import ConnectionPool
-from pydantic import BaseModel
+from pydantic import BaseModel, field_validator
 from slowapi import Limiter, _rate_limit_exceeded_handler
 from slowapi.errors import RateLimitExceeded
 from slowapi.middleware import SlowAPIMiddleware
@@ -121,6 +121,47 @@ class ModuleInfo(BaseModel):
     count: int
     docstring: str | None = None
 
+    @field_validator("docstring", mode="before")
+    @classmethod
+    def join_sections(cls, v: object) -> str | None:
+        if v is None:
+            return None
+        if isinstance(v, list):
+            return "\n\n".join(str(s) for s in v if s)
+        if isinstance(v, str) and v.startswith("{") and v.endswith("}"):
+            # Parse PostgreSQL text[] literal: {"section1","section2",...}
+            inner = v[1:-1]
+            parts: list[str] = []
+            i = 0
+            while i < len(inner):
+                if inner[i] == '"':
+                    j = i + 1
+                    buf: list[str] = []
+                    while j < len(inner):
+                        if inner[j] == "\\" and j + 1 < len(inner):
+                            buf.append(inner[j + 1])
+                            j += 2
+                        elif inner[j] == '"':
+                            j += 1
+                            break
+                        else:
+                            buf.append(inner[j])
+                            j += 1
+                    parts.append("".join(buf))
+                    i = j
+                    if i < len(inner) and inner[i] == ",":
+                        i += 1
+                else:
+                    end = inner.find(",", i)
+                    if end == -1:
+                        end = len(inner)
+                    token = inner[i:end].strip()
+                    if token.upper() not in ("NULL", ""):
+                        parts.append(token)
+                    i = end + 1
+            return "\n\n".join(p for p in parts if p.strip())
+        return v
+
 
 @app.get("/modules")
 @limiter.limit("30/minute")