diff --git a/web2/public/images/physlib-logo.png b/web2/public/images/physlib-logo.png new file mode 100644 index 0000000..a606eca Binary files /dev/null and b/web2/public/images/physlib-logo.png differ diff --git a/web2/src/app/about/beneficiaries/page.tsx b/web2/src/app/about/beneficiaries/page.tsx new file mode 100644 index 0000000..ca6b14d --- /dev/null +++ b/web2/src/app/about/beneficiaries/page.tsx @@ -0,0 +1,61 @@ +import type { Metadata } from "next"; +import { AboutSectionNav } from "@/components/about-section-nav"; +import { audiences } from "@/lib/about-content"; + +export const metadata: Metadata = { + title: "Beneficiaries", + description: + "Who Physlib is for — researchers, students, companies, and labs working with physics and formal methods.", +}; + +export default function BeneficiariesPage() { + return ( +
+ +

About

+

+ Beneficiaries +

+

+ For physicists and formal-methods researchers. +

+ +
+ {audiences.map((a) => ( +
+

{a.tag}

+

+ {a.title} +

+
    + {a.items.map((item) => ( +
  • + — + {item} +
    • + ))} +
+
+ ))} +
+ + +
+ ); +} diff --git a/web2/src/app/about/impact/page.tsx b/web2/src/app/about/impact/page.tsx new file mode 100644 index 0000000..e65bddc --- /dev/null +++ b/web2/src/app/about/impact/page.tsx @@ -0,0 +1,66 @@ +import type { Metadata } from "next"; +import { AboutSectionNav } from "@/components/about-section-nav"; +import { impacts, paper } from "@/lib/about-content"; + +export const metadata: Metadata = { + title: "Impact", + description: + "Why formalize physics — what a library of digitalized physics results makes possible.", +}; + +export default function ImpactPage() { + return ( +
+ +

About

+

+ Impact +

+

+ Why formalize physics? +

+ +
+ {impacts.map((item, i) => ( +
+ + {String(i + 1).padStart(2, "0")} + +

+ {item} +

+
+ ))} +
+ +

+ Read the paper:{" "} + + {paper.label} + +

+ + +
+ ); +} diff --git a/web2/src/app/about/mission/page.tsx b/web2/src/app/about/mission/page.tsx new file mode 100644 index 0000000..aaa27cf --- /dev/null +++ b/web2/src/app/about/mission/page.tsx @@ -0,0 +1,48 @@ +import type { Metadata } from "next"; +import { AboutSectionNav } from "@/components/about-section-nav"; +import { missionStatement, visionPoints } from "@/lib/about-content"; + +export const metadata: Metadata = { + title: "Mission", + description: missionStatement, +}; + +export default function MissionPage() { + return ( +
+ +

About

+

+ Mission +

+

+ Create a library of digitalized physics results in Lean 4, + useful to the broad physics community. +

+ +
+ {visionPoints.map((point, i) => ( +
+ + {String(i + 1).padStart(2, "0")} + +

+ {point} +

+
+ ))} +
+ + +
+ ); +} diff --git a/web2/src/app/about/page.tsx b/web2/src/app/about/page.tsx new file mode 100644 index 0000000..d6e9539 --- /dev/null +++ b/web2/src/app/about/page.tsx @@ -0,0 +1,75 @@ +import type { Metadata } from "next"; +import Link from "next/link"; +import { aboutSections, paper } from "@/lib/about-content"; +import { site } from "@/lib/site"; + +export const metadata: Metadata = { + title: "About", + description: + "The mission, values, beneficiaries, and intended impact of Physlib — a library of digitalized physics results in Lean 4.", +}; + +export default function AboutPage() { + return ( +
+ + {/* Page intro */} +

About

+

+ About Physlib +

+

+ {site.description} +

+ + {/* Section index */} +
+ {aboutSections.map((s, i) => ( + + + {String(i + 1).padStart(2, "0")} + + + {s.label} + + + {s.tagline} + + + Read more → + + + ))} +
+ + {/* Paper */} +
+ Read the paper:{" "} + + {paper.label} + +
+
+ ); +} diff --git a/web2/src/app/about/values/page.tsx b/web2/src/app/about/values/page.tsx new file mode 100644 index 0000000..15b858a --- /dev/null +++ b/web2/src/app/about/values/page.tsx @@ -0,0 +1,57 @@ +import type { Metadata } from "next"; +import { AboutSectionNav } from "@/components/about-section-nav"; +import { values } from "@/lib/about-content"; + +export const metadata: Metadata = { + title: "Values", + description: + "The principles Physlib is built on — welcoming, open and transparent, accessible and practical.", +}; + +export default function ValuesPage() { + return ( +
+ +

About

+

+ Values +

+

+ Built on principles. +

+ +
+ {values.map((v, i) => ( +
+ + {String(i + 1).padStart(2, "0")} + +

+ {v.title} +

+

+ {v.body} +

+
+ ))} +
+ + +
+ ); +} diff --git a/web2/src/app/documentation-tracker/page.tsx b/web2/src/app/documentation-tracker/page.tsx index eb70526..ecfd434 100644 --- a/web2/src/app/documentation-tracker/page.tsx +++ b/web2/src/app/documentation-tracker/page.tsx @@ -28,7 +28,7 @@ export default function DocumentationTrackerPage() {
-

+

Steps to Help with Documentation

@@ -38,7 +38,9 @@ export default function DocumentationTrackerPage() { {docSteps.map((step) => (

-

{step.title}

+

+ {step.title} +

    {step.items.map((item, i) => (
  1. @@ -52,6 +54,10 @@ export default function DocumentationTrackerPage() { ); } +function slugify(title: string) { + return title.toLowerCase().replace(/[^a-z0-9]+/g, "-").replace(/(^-|-$)/g, ""); +} + const docSteps = [ { title: "Phase 1: Get the Code", diff --git a/web2/src/app/getting-started/page.tsx b/web2/src/app/getting-started/page.tsx index 42acfb6..709bc3d 100644 --- a/web2/src/app/getting-started/page.tsx +++ b/web2/src/app/getting-started/page.tsx @@ -52,6 +52,61 @@ export default function GettingStartedPage() { ))}
+ {/* About Lean */} + +
+
+

+ A theorem prover that guarantees correctness. +

+

+ Lean is an interactive theorem prover where you write mathematical + definitions, theorems, and proofs — and the system verifies + correctness using type theory, with no gaps or hand-waving. +

+

+ Increasingly used by AI labs and mathematicians, Lean is now + making its way into physics through Physlib. +

+
+ + {/* Code card */} +
+
+ + + + WicksTheorem.lean +
+
+ 
+              
+                theorem wicks_theorem : (φs : List 𝓕.FieldOp) → 𝓣(ofFieldOpList φs) ={"\n"}
+                {"  "}∑ (φsΛ : WickContraction φs.length), φsΛ.wickTerm{"\n"}
+                | [] => by{"\n"}
+                {"  "}rw [timeOrder_ofFieldOpList_nil]{"\n"}
+                {"  "}simp only [map_one, List.length_nil, Algebra.smul_mul_assoc]{"\n"}
+                {"  "}rw [sum_WickContraction_nil]{"\n"}
+                {"  "}simp only [wickTerm_empty_nil]{"\n"}
+                | φ :: φs => by
+              
+
+
+
+ Wick's theorem — formally verified in Physlib. +
+
+
+ {/* Useful Resources */}
@@ -231,6 +286,7 @@ const tocSections = [ { title: "Getting Started", links: [ + { label: "About Lean", href: "#about-lean" }, { label: "Useful Resources", href: "#useful-resources" }, { label: "Installation Guide", href: "#installing" }, ], diff --git a/web2/src/app/gh-guide/page.tsx b/web2/src/app/gh-guide/page.tsx index 048ecb4..fe8645e 100644 --- a/web2/src/app/gh-guide/page.tsx +++ b/web2/src/app/gh-guide/page.tsx @@ -1,5 +1,6 @@ import { Card } from "@heroui/react"; import type { Metadata } from "next"; +import { PageHeader } from "@/components/page-header"; import { site } from "@/lib/site"; export const metadata: Metadata = { @@ -28,12 +29,7 @@ export default function GhGuidePage() { {/* Step 1 — Deciding on a Problem to Work On */}
-

- 1. Deciding on a Problem to Work On -

+
@@ -44,7 +40,7 @@ export default function GhGuidePage() { Before starting any work, you can open an issue on the Physlib repository to describe the problem you are encountering or the feature you want to add. This makes maintainers aware of the work you plan on doing and helps with - tracking the project. + tracking the project.

{/* Step 3 — Pull Request */}
-

- 3. Make a Pull Request -

+

Small pull-requests are better than large ones — even if it's just a single result. Follow the PR template provided by GitHub when opening your PR. @@ -169,7 +155,8 @@ export default function GhGuidePage() {

Adding Labels @@ -190,7 +177,8 @@ export default function GhGuidePage() {

Lifecycle of a PR @@ -207,7 +195,8 @@ export default function GhGuidePage() {

Other Common Labels @@ -253,12 +242,7 @@ export default function GhGuidePage() {

-

- 4. Managing the PR -

+

After opening a PR, the maintainers will review the changes and provide feedback. Feel free to begin work on a separate PR in the meantime but be prepared to make changes to this one if required.

@@ -282,12 +266,7 @@ export default function GhGuidePage() {
-

- 5. Merging the PR -

+

Once the reviewer is happy with the changes, they will merge the PR into the main branch. Physlib uses a{" "} -

- Additional Guidance -

+

Please use your real name in your GitHub account settings and commit author. Physlib uses GitHub account names in its automated documentation generation, so using your real name diff --git a/web2/src/app/globals.css b/web2/src/app/globals.css index dc17816..b42085e 100644 --- a/web2/src/app/globals.css +++ b/web2/src/app/globals.css @@ -86,6 +86,13 @@ body { var(--background); } +/* ─── Logo mark ─────────────────────────────────────────────── */ +/* The logo is black line-art on transparency, so it flips to white in dark + mode. invert() leaves alpha alone, which keeps the edges anti-aliased. */ +[data-theme="dark"] .logo-mark { + filter: invert(1); +} + /* ─── Animations ────────────────────────────────────────────── */ @keyframes fade-up { from { opacity: 0; transform: translateY(20px); } @@ -96,6 +103,30 @@ body { .delay-100 { animation-delay: 100ms; } .delay-200 { animation-delay: 200ms; } +@keyframes carousel-in-right { + from { opacity: 0; transform: translateX(24px); } + to { opacity: 1; transform: translateX(0); } +} +@keyframes carousel-in-left { + from { opacity: 0; transform: translateX(-24px); } + to { opacity: 1; transform: translateX(0); } +} + +@keyframes carousel-progress { + from { transform: scaleX(0); } + to { transform: scaleX(1); } +} + +.carousel-progress { + animation-name: carousel-progress; + animation-timing-function: linear; + animation-fill-mode: forwards; +} + +@media (prefers-reduced-motion: reduce) { + .carousel-progress { animation: none; } +} + /* ─── Prose ─────────────────────────────────────────────────── */ @layer components { .prose-physlib { @apply text-foreground leading-relaxed; } @@ -124,6 +155,11 @@ body { .prose-physlib img { @apply rounded my-4 max-w-full h-auto; } } +/* ─── TOC anchor offset (clears fixed navbar) ───────────────── */ +h2[id], h3[id] { + scroll-margin-top: 5rem; +} + @keyframes shimmer { 0% { background-position: -200% 0; } 100% { background-position: 200% 0; } diff --git a/web2/src/app/page.tsx b/web2/src/app/page.tsx index 21e4c50..745dde2 100644 --- a/web2/src/app/page.tsx +++ b/web2/src/app/page.tsx @@ -1,40 +1,52 @@ import Link from "next/link"; import { site } from "@/lib/site"; +import { GetInvolvedCarousel } from "@/components/get-involved-carousel"; export default function HomePage() { return ( -

+
- {/* ═══ HERO ═══════════════════════════════════════════════ */} -
-
- - {/* ═══ WHAT IS LEAN ═══════════════════════════════════════ */} -
-
-
-

About Lean

-

- A theorem prover that guarantees correctness. -

-

- Lean is an interactive theorem prover where you write mathematical - definitions, theorems, and proofs — and the system verifies - correctness using type theory, with no gaps or hand-waving. -

-

- Increasingly used by AI labs and mathematicians, Lean is now - making its way into physics through Physlib. -

-
- - {/* Code card */} -
-
- - - - WicksTheorem.lean -
-
- 
-                
-                  theorem wicks_theorem : (φs : List 𝓕.FieldOp) → 𝓣(ofFieldOpList φs) ={"\n"}
-                  {"  "}∑ (φsΛ : WickContraction φs.length), φsΛ.wickTerm{"\n"}
-                  | [] => by{"\n"}
-                  {"  "}rw [timeOrder_ofFieldOpList_nil]{"\n"}
-                  {"  "}simp only [map_one, List.length_nil, Algebra.smul_mul_assoc]{"\n"}
-                  {"  "}rw [sum_WickContraction_nil]{"\n"}
-                  {"  "}simp only [wickTerm_empty_nil]{"\n"}
-                  | φ :: φs => by
-                
-
-
-
- Wick's theorem — formally verified in Physlib. -
-
-
-
- - {/* ═══ MISSION ═════════════════════════════════════════════ */} -
-
-

Mission

-

- Create a library of digitalized physics results in Lean 4, - useful to the broad physics community. -

- -
- {visionPoints.map((point, i) => ( -
- - {String(i + 1).padStart(2, "0")} - -

- {point} -

-
- ))} -
-
-
- - {/* ═══ VALUES ═════════════════════════════════════════════ */} -
-
-

Values

-

- Built on principles. -

-
- {values.map((v, i) => ( -
- - {String(i + 1).padStart(2, "0")} - -

- {v.title} -

-

- {v.body} -

-
- ))} -
-
-
- - {/* ═══ AUDIENCES ═══════════════════════════════════════════ */} -
-
-

Beneficiaries

-

- For physicists and
formal-methods researchers. -

-
- {audiences.map((a) => ( -
-

{a.tag}

-

- {a.title} -

-
    - {a.items.map((item) => ( -
  • - — - {item} -
    • - ))} -
-
- ))} -
-
-
+
- {/* ═══ IMPACT ═════════════════════════════════════════════ */} -
-
-

Impact

+ {/* ═══ GET INVOLVED ════════════════════════════════════════ */} +
+
+

Get Involved

- Why formalize physics? + How you can contribute:

-
- {impacts.map((item, i) => ( -
- - {String(i + 1).padStart(2, "0")} - -

- {item} -

-
- ))} -
+
-
- - {/* ═══ CTA ════════════════════════════════════════════════ */} -
-
-

Join Physlib

-

- Help build the future
of physics. -

-

- Whether you're a physicist, a Lean developer, or just curious — - there's a place for you in Physlib. -

-
- - Start contributing - - - - Learn more - -
-

- Read the paper:{" "} - - arXiv:2405.08863 - -

-
-
- -
+
+ ); } -/* ─── Data ──────────────────────────────────────────────────── */ - -const visionPoints = [ - "Comprehensive repository of fundamental physics definitions, theorems, and calculations.", - "Interface between experimental data, simulations, and formal theoretical frameworks.", - "Extensive, physics-focused documentation to support adoption.", - "Accessible to physicists at all levels — especially those new to formal methods.", - "An intuitive setup that aligns with how physicists think and work.", - "A large, active team with the potential for high-energy-physics-style collaborations.", -]; - -const values = [ - { - title: "Welcoming", - body: "Contributors of all academic backgrounds and experience levels are valued, supported, and empowered to make meaningful contributions.", - }, - { - title: "Open & Transparent", - body: "Physlib is openly accessible, freely available, and developed with full transparency for the benefit of both communities.", - }, - { - title: "Accessible & Practical", - body: "Designed to be intuitive and well-documented, directly useful to physicists regardless of their familiarity with formal methods.", - }, -]; - -const audiences = [ - { - tag: "Academic", - title: "Researchers & Students", - items: [ - "Students in physics, mathematics, or computer science", - "Research physicists formalizing theoretical results", - "AI researchers verifying mathematical theorems", - "Educators creating novel teaching approaches", - ], - }, - { - tag: "Industrial", - title: "Companies & Labs", - items: [ - "Companies leveraging AI for formal reasoning at scale", - "Organizations proving correctness of physical processes", - "Teams building verified simulation frameworks", - "Enterprises ensuring theoretical soundness of models", - ], - }, -]; - -const impacts = [ - "Make it easier to find and reference existing results across physics.", - "Enable AI and machine learning to automate discovery of new results.", - "Check papers and results for mathematical correctness automatically.", - "Create new avenues through which physics can be taught and explored.", - "Open new ways to interface between theory and computer programs.", - "Build a shared, standardized foundation for the whole physics community.", -]; - /* ─── Icons ─────────────────────────────────────────────────── */ function ArrowRight() { @@ -381,11 +101,3 @@ function ArrowRight() { ); } - -function GitHubIcon() { - return ( - - - - ); -} diff --git a/web2/src/components/about-section-nav.tsx b/web2/src/components/about-section-nav.tsx new file mode 100644 index 0000000..ace4b01 --- /dev/null +++ b/web2/src/components/about-section-nav.tsx @@ -0,0 +1,40 @@ +import Link from "next/link"; +import { aboutSections } from "@/lib/about-content"; + +/** Links to the other pages in the About section, shown at the foot of each one. */ +export function AboutSectionNav({ current }: { current: string }) { + const others = aboutSections.filter((s) => s.href !== current); + + return ( + + ); +} diff --git a/web2/src/components/conditional-sidebar.tsx b/web2/src/components/conditional-sidebar.tsx index 8ea90db..49dfaf0 100644 --- a/web2/src/components/conditional-sidebar.tsx +++ b/web2/src/components/conditional-sidebar.tsx @@ -1,10 +1,10 @@ "use client"; import { usePathname } from "next/navigation"; -import { SidebarNav } from "./sidebar-nav"; +import { TableOfContents } from "./table-of-contents"; export function ConditionalSidebar() { const pathname = usePathname(); if (pathname === "/") return null; - return ; + return ; } diff --git a/web2/src/components/footer.tsx b/web2/src/components/footer.tsx index e92ec54..6f089a0 100644 --- a/web2/src/components/footer.tsx +++ b/web2/src/components/footer.tsx @@ -2,6 +2,13 @@ import Link from "next/link"; import { site } from "@/lib/site"; const footerLinks = { + About: [ + { label: "Overview", href: "/about" }, + { label: "Mission", href: "/about/mission" }, + { label: "Values", href: "/about/values" }, + { label: "Impact", href: "/about/impact" }, + { label: "Maintainers", href: "/maintainers" }, + ], Learn: [ { label: "Getting Started", href: "/getting-started" }, { label: "APIs", href: "/apis" }, @@ -9,7 +16,6 @@ const footerLinks = { ], Community: [ { label: "Get Involved", href: "/get-involved" }, - { label: "Maintainers", href: "/maintainers" }, { label: "Todo list", href: "/todo" }, { label: "Discussion", href: site.zulip, external: true }, ], @@ -38,7 +44,7 @@ export function Footer() { Physlib

-
+
{/* Brand */}
(null); + const [animKey, setAnimKey] = useState(0); + + useEffect(() => { + if (window.matchMedia("(prefers-reduced-motion: reduce)").matches) { + return; + } + + const timer = window.setTimeout(() => { + setDir("right"); + setIndex((currentIndex) => (currentIndex + 1) % cards.length); + setAnimKey((key) => key + 1); + }, AUTO_ADVANCE_MS); + + return () => window.clearTimeout(timer); + }, [index]); + + function go(next: number) { + const newIndex = (next + cards.length) % cards.length; + setDir(next > index || (index === cards.length - 1 && next === 0) ? "right" : "left"); + setIndex(newIndex); + setAnimKey((k) => k + 1); + } + + const card = cards[index]; + + return ( +
+ {/* carousel row */} +
+ + {/* left arrow */} + + + {/* card */} +
+

+ {card.title} +

+ +
    + {card.items.map((item) => ( +
  • + — + {item} +
    • + ))} +
+ +
+ {card.cta.external ? ( + + {card.cta.label} + + + ) : ( + + {card.cta.label} + + )} +
+
+ + {/* right arrow */} + +
+ + {/* dot indicators */} +
+ {cards.map((_, i) => ( + + ))} +
+
+ ); +} + +function ChevronLeft() { + return ( + + + + ); +} + +function ChevronRight() { + return ( + + + + ); +} + +function ExternalIcon() { + return ( + + + + ); +} diff --git a/web2/src/components/graphviz-view.tsx b/web2/src/components/graphviz-view.tsx index 4e9d79d..d55b659 100644 --- a/web2/src/components/graphviz-view.tsx +++ b/web2/src/components/graphviz-view.tsx @@ -10,18 +10,25 @@ declare global { } } +// Keyed by src, so repeat calls - e.g. React Strict Mode's dev-only +// mount/unmount/remount cycle - await the *same* load rather than each +// racing to check "is a