From 58f8c38cdd789ff63148374aef6dd11fd535d487 Mon Sep 17 00:00:00 2001 From: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com> Date: Tue, 18 Aug 2026 18:10:57 +0100 Subject: [PATCH 1/3] changed api maps to use the yaml files --- .github/workflows/api-map.yml | 75 +++ web2/data/APIMap.json | 551 ++++++++++++++++++ web2/scripts/generate-api-map.js | 177 ++++++ .../app/api-tracker/api-tracker-client.tsx | 87 +-- web2/src/app/api-tracker/page.tsx | 19 +- web2/src/lib/yaml.ts | 26 + 6 files changed, 894 insertions(+), 41 deletions(-) create mode 100644 .github/workflows/api-map.yml create mode 100644 web2/data/APIMap.json create mode 100644 web2/scripts/generate-api-map.js diff --git a/.github/workflows/api-map.yml b/.github/workflows/api-map.yml new file mode 100644 index 0000000..b843d26 --- /dev/null +++ b/.github/workflows/api-map.yml @@ -0,0 +1,75 @@ +name: Generate API map + +on: + schedule: + # Weekly refresh — API-map.yaml files change far less often than commits. + - cron: "20 4 * * 1" + workflow_dispatch: {} + +permissions: + contents: write + +# Two runs committing to the same branch would race on push. +concurrency: + group: api-map + cancel-in-progress: false + +jobs: + generate: + runs-on: ubuntu-latest + timeout-minutes: 20 + env: + HAS_MIRROR_PAT: ${{ secrets.MIRROR_PAT != '' }} + steps: + - name: Checkout + uses: actions/checkout@v4 + with: + persist-credentials: true + fetch-depth: 0 + + - name: Set up Node.js + uses: actions/setup-node@v4 + with: + node-version: "20" + + # Shared with the monthly-updates generator, which also reads this repo. + - name: Cache physlib clone + uses: actions/cache@v4 + with: + path: web2/.cache/physlib.git + key: physlib-clone-${{ github.run_id }} + restore-keys: physlib-clone- + + - name: Run generator + working-directory: web2 + run: node scripts/generate-api-map.js + + - name: Commit & push updated API map + id: commit + run: | + git config user.name "github-actions[bot]" + git config user.email "41898282+github-actions[bot]@users.noreply.github.com" + git add web2/data/APIMap.json + if git diff --cached --quiet; then + echo "No API map changes to commit." + echo "committed=false" >> "$GITHUB_OUTPUT" + exit 0 + fi + git commit -m "chore(api-map): auto-generated update" + git pull --rebase --autostash origin "${GITHUB_REF_NAME}" + git push origin "HEAD:${GITHUB_REF_NAME}" + echo "committed=true" >> "$GITHUB_OUTPUT" + + # See monthly-updates.yml for why this step exists: pushes made with the + # default GITHUB_TOKEN don't trigger mirror-to-personal.yml, so without + # this the API map would never reach the deployed (Vercel) site. + - name: Mirror to personal repo (Vercel) + if: steps.commit.outputs.committed == 'true' && env.HAS_MIRROR_PAT == 'true' + env: + MIRROR_PAT: ${{ secrets.MIRROR_PAT }} + run: | + git config --unset-all http.https://github.com/.extraheader || true + git config --global credential.helper store + echo "https://x-access-token:${MIRROR_PAT}@github.com" > ~/.git-credentials + git remote add mirror https://github.com/Gabrielebattimelli/Physlib-Website.git + git push mirror "HEAD:refs/heads/${GITHUB_REF_NAME}" diff --git a/web2/data/APIMap.json b/web2/data/APIMap.json new file mode 100644 index 0000000..d5ab0f9 --- /dev/null +++ b/web2/data/APIMap.json @@ -0,0 +1,551 @@ +{ + "repo": "leanprover-community/physlib", + "branch": "master", + "generatedAt": "2026-08-18T16:52:46.574Z", + "nodes": [ + { + "path": "Physlib/ClassicalFieldTheory/GaugeTheory", + "title": "Gauge theory", + "requirementsDone": 8, + "requirementsTotal": 15, + "parents": [ + { + "name": "Electromagnetic potential", + "path": "Physlib/Electromagnetism/Kinematics/EMPotential.lean" + }, + { + "name": "Field strength", + "path": "Physlib/Electromagnetism/Kinematics/FieldStrength.lean" + }, + { + "name": "Standard Model gauge group", + "path": "Physlib/Particles/StandardModel/Basic.lean" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml" + }, + { + "path": "Physlib/ClassicalMechanics/DampedHarmonicOscillator", + "title": "Damped harmonic oscillator", + "requirementsDone": 14, + "requirementsTotal": 14, + "parents": [ + { + "name": "Harmonic oscillator", + "path": "Physlib/ClassicalMechanics/HarmonicOscillator" + }, + { + "name": "Time", + "path": "Physlib/SpaceAndTime/Time" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml" + }, + { + "path": "Physlib/ClassicalMechanics/HarmonicOscillator/Geometric", + "title": "Configuration space of the harmonic oscillator", + "requirementsDone": 9, + "requirementsTotal": 9, + "parents": [ + { + "name": "Harmonic oscillator", + "path": "Physlib/ClassicalMechanics/HarmonicOscillator" + }, + { + "name": "Space", + "path": "Physlib/SpaceAndTime/Space" + }, + { + "name": "Time", + "path": "Physlib/SpaceAndTime/Time" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/API-map.yaml" + }, + { + "path": "Physlib/ClassicalMechanics/Lagrangian", + "title": "Configuration Space", + "requirementsDone": 0, + "requirementsTotal": 2, + "parents": [ + { + "name": "Space", + "path": "Physlib/SpaceAndTime/Space" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml" + }, + { + "path": "Physlib/ClassicalMechanics/Pendulum", + "title": "Configuration space for pendulum", + "requirementsDone": 1, + "requirementsTotal": 5, + "parents": [ + { + "name": "Classical mechanics Lagrangian", + "path": "Physlib/ClassicalMechanics/Lagrangian" + }, + { + "name": "Space", + "path": "Physlib/SpaceAndTime/Space" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/ClassicalMechanics/Pendulum/API-map.yaml" + }, + { + "path": "Physlib/ClassicalMechanics/RigidBody", + "title": "Rigid body", + "requirementsDone": 10, + "requirementsTotal": 13, + "parents": [ + { + "name": "Space", + "path": "Physlib/SpaceAndTime/Space" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/ClassicalMechanics/RigidBody/API-map.yaml" + }, + { + "path": "Physlib/Cosmology/FLRW", + "title": "FLRW cosmology", + "requirementsDone": 5, + "requirementsTotal": 7, + "parents": [ + { + "name": "Time", + "path": "Physlib/SpaceAndTime/Time" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/Cosmology/FLRW/API-map.yaml" + }, + { + "path": "Physlib/Electromagnetism/Kinematics", + "title": "Electromagnetic Potential", + "requirementsDone": 7, + "requirementsTotal": 8, + "parents": [ + { + "name": "SpaceTime", + "path": "Physlib/SpaceAndTime/SpaceTime" + }, + { + "name": "LorentzGroup", + "path": "Physlib/Relativity/LorentzGroup" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/Electromagnetism/Kinematics/API-map.yaml" + }, + { + "path": "Physlib/FluidDynamics", + "title": "Fluid", + "requirementsDone": 5, + "requirementsTotal": 9, + "parents": [ + { + "name": "Space", + "path": "Physlib/SpaceAndTime/Space" + }, + { + "name": "Time", + "path": "Physlib/SpaceAndTime/Time" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/FluidDynamics/API-map.yaml" + }, + { + "path": "Physlib/Particles/BeyondTheStandardModel/TwoHDM", + "title": "Two Higgs Doublet Model", + "requirementsDone": 13, + "requirementsTotal": 15, + "parents": [ + { + "name": "Higgs Field", + "path": "Physlib/Particles/StandardModel/HiggsBoson" + }, + { + "name": "Pauli matrices", + "path": "Physlib/Relativity/PauliMatrices" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/Particles/BeyondTheStandardModel/TwoHDM/API-map.yaml" + }, + { + "path": "Physlib/Particles/StandardModel", + "title": "Standard Model gauge group", + "requirementsDone": 10, + "requirementsTotal": 15, + "parents": [], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/Particles/StandardModel/API-map.yaml" + }, + { + "path": "Physlib/Particles/StandardModel/HiggsBoson", + "title": "Higgs Field", + "requirementsDone": 16, + "requirementsTotal": 21, + "parents": [ + { + "name": "SpaceTime", + "path": "Physlib/SpaceAndTime/SpaceTime" + }, + { + "name": "Standard Model gauge group", + "path": "Physlib/Particles/StandardModel" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/Particles/StandardModel/HiggsBoson/API-map.yaml" + }, + { + "path": "Physlib/QFT/PerturbationTheory/FeynmanDiagrams", + "title": "Feynman diagrams", + "requirementsDone": 0, + "requirementsTotal": 6, + "parents": [ + { + "name": "Field specification", + "path": "Physlib/QFT/PerturbationTheory/FieldSpecification" + }, + { + "name": "Field operator free algebra", + "path": "Physlib/QFT/PerturbationTheory/FieldOpFreeAlgebra" + }, + { + "name": "Wick algebra", + "path": "Physlib/QFT/PerturbationTheory/WickAlgebra" + }, + { + "name": "Wick contractions", + "path": "Physlib/QFT/PerturbationTheory/WickContraction" + }, + { + "name": "Koszul signs", + "path": "Physlib/QFT/PerturbationTheory/Koszul" + }, + { + "name": "Field statistics", + "path": "Physlib/QFT/PerturbationTheory/FieldStatistics" + }, + { + "name": "Lorentz group", + "path": "Physlib/Relativity/LorentzGroup" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/QFT/PerturbationTheory/FeynmanDiagrams/API-map.yaml" + }, + { + "path": "Physlib/QFT/TopologicalFieldTheory", + "title": "Topological field theory", + "requirementsDone": 0, + "requirementsTotal": 17, + "parents": [ + { + "name": "Time", + "path": "Physlib/SpaceAndTime/Time" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/QFT/TopologicalFieldTheory/API-map.yaml" + }, + { + "path": "Physlib/QuantumMechanics/HilbertSpaces/SpaceD", + "title": "Hilbert spaces on Space", + "requirementsDone": 8, + "requirementsTotal": 15, + "parents": [ + { + "name": "Space", + "path": "Physlib/SpaceAndTime/Space" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml" + }, + { + "path": "Physlib/QuantumMechanics/HilbertSpaces/TensorProducts", + "title": "Hilbert space tensor products", + "requirementsDone": 3, + "requirementsTotal": 7, + "parents": [], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/QuantumMechanics/HilbertSpaces/TensorProducts/API-map.yaml" + }, + { + "path": "Physlib/QuantumMechanics/Operators", + "title": "Operator algebra", + "requirementsDone": 25, + "requirementsTotal": 29, + "parents": [ + { + "name": "Hilbert spaces on Space", + "path": "Physlib/QuantumMechanics/HilbertSpaces/SpaceD" + }, + { + "name": "Space", + "path": "Physlib/SpaceAndTime/Space" + }, + { + "name": "Planck constant", + "path": "Physlib/QuantumMechanics/PlanckConstant.lean" + }, + { + "name": "Partially defined linear maps", + "path": "Physlib/Mathematics/LinearPMap.lean" + }, + { + "name": "Inner product spaces", + "path": "Physlib/Mathematics/InnerProductSpace" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/QuantumMechanics/Operators/API-map.yaml" + }, + { + "path": "Physlib/QuantumMechanics/Operators/SpectralTheory", + "title": "Spectral theory of unbounded operators", + "requirementsDone": 14, + "requirementsTotal": 17, + "parents": [ + { + "name": "Operator algebra", + "path": "Physlib/QuantumMechanics/Operators" + }, + { + "name": "Partially defined linear maps", + "path": "Physlib/Mathematics/LinearPMap.lean" + }, + { + "name": "Inner product spaces", + "path": "Physlib/Mathematics/InnerProductSpace" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/QuantumMechanics/Operators/SpectralTheory/API-map.yaml" + }, + { + "path": "Physlib/QuantumMechanics/QuantumSystem", + "title": "QuantumSystem", + "requirementsDone": 3, + "requirementsTotal": 9, + "parents": [], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/QuantumMechanics/QuantumSystem/API-map.yaml" + }, + { + "path": "Physlib/QuantumMechanics/Qubit", + "title": "Qubits", + "requirementsDone": 7, + "requirementsTotal": 21, + "parents": [ + { + "name": "Kets and bras of a finite dimensional system", + "path": "QuantumInfo/States/Pure" + }, + { + "name": "Mixed states", + "path": "QuantumInfo/States/Mixed" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/QuantumMechanics/Qubit/API-map.yaml" + }, + { + "path": "Physlib/Relativity/Fermions/Dirac", + "title": "Dirac Fermions", + "requirementsDone": 9, + "requirementsTotal": 16, + "parents": [ + { + "name": "Weyl Fermions", + "path": "Physlib/Relativity/Fermions/Weyl" + }, + { + "name": "Lorentz Group", + "path": "Physlib/Relativity/LorentzGroup" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/Relativity/Fermions/Dirac/API-map.yaml" + }, + { + "path": "Physlib/Relativity/Fermions/Weyl", + "title": "Weyl Fermions", + "requirementsDone": 14, + "requirementsTotal": 18, + "parents": [ + { + "name": "Lorentz Group", + "path": "Physlib/Relativity/LorentzGroup" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/Relativity/Fermions/Weyl/API-map.yaml" + }, + { + "path": "Physlib/Relativity/LorentzGroup", + "title": "Lorentz Group", + "requirementsDone": 9, + "requirementsTotal": 12, + "parents": [ + { + "name": "MinkowskiMatrix", + "path": "Physlib/Relativity/MinkowskiMatrix.lean" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/Relativity/LorentzGroup/API-map.yaml" + }, + { + "path": "Physlib/Relativity/Tensors", + "title": "Tensors", + "requirementsDone": 16, + "requirementsTotal": 22, + "parents": [ + { + "name": "Lorentz Group", + "path": "Physlib/Relativity/LorentzGroup" + }, + { + "name": "Weyl Fermions", + "path": "Physlib/Relativity/Fermions/Weyl" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/Relativity/Tensors/API-map.yaml" + }, + { + "path": "Physlib/SpaceAndTime/GalileanGroup", + "title": "Galilean group", + "requirementsDone": 8, + "requirementsTotal": 9, + "parents": [ + { + "name": "Space", + "path": "Physlib/SpaceAndTime/Space" + }, + { + "name": "Time", + "path": "Physlib/SpaceAndTime/Time" + }, + { + "name": "Euclidean group", + "path": "Physlib/SpaceAndTime/Space/EuclideanGroup" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/SpaceAndTime/GalileanGroup/API-map.yaml" + }, + { + "path": "Physlib/SpaceAndTime/Space", + "title": "Space", + "requirementsDone": 16, + "requirementsTotal": 18, + "parents": [ + { + "name": "Distribution", + "path": "Physlib/Mathematics/Distribution" + }, + { + "name": "Time", + "path": "Physlib/SpaceAndTime/Time" + }, + { + "name": "Lorentz vectors", + "path": "Physlib/Relativity/Tensors/RealTensor/Vector" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/SpaceAndTime/Space/API-map.yaml" + }, + { + "path": "Physlib/SpaceAndTime/SpaceTime", + "title": "SpaceTime", + "requirementsDone": 9, + "requirementsTotal": 10, + "parents": [ + { + "name": "Lorentz vectors", + "path": "Physlib/Relativity/Tensors/RealTensor/Vector" + }, + { + "name": "Space", + "path": "Physlib/SpaceAndTime/Space" + }, + { + "name": "Time", + "path": "Physlib/SpaceAndTime/Time" + }, + { + "name": "Lorentz group", + "path": "Physlib/Relativity/LorentzGroup" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/SpaceAndTime/SpaceTime/API-map.yaml" + }, + { + "path": "Physlib/SpaceAndTime/Time", + "title": "Time", + "requirementsDone": 11, + "requirementsTotal": 16, + "parents": [ + { + "name": "Space", + "path": "Physlib/SpaceAndTime/Space" + }, + { + "name": "Lorentz vectors", + "path": "Physlib/Relativity/Tensors/RealTensor/Vector" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/SpaceAndTime/Time/API-map.yaml" + }, + { + "path": "Physlib/SpaceAndTime/TimeAndSpace", + "title": "TimeAndSpace", + "requirementsDone": 6, + "requirementsTotal": 6, + "parents": [ + { + "name": "Time", + "path": "Physlib/SpaceAndTime/Time" + }, + { + "name": "Space", + "path": "Physlib/SpaceAndTime/Space" + }, + { + "name": "Euclidean group", + "path": "Physlib/SpaceAndTime/Space/EuclideanGroup" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/SpaceAndTime/TimeAndSpace/API-map.yaml" + }, + { + "path": "Physlib/StatisticalMechanics/CanonicalEnsemble", + "title": "Canonical ensemble", + "requirementsDone": 11, + "requirementsTotal": 13, + "parents": [ + { + "name": "Temperature", + "path": "Physlib/Thermodynamics/Temperature" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/StatisticalMechanics/CanonicalEnsemble/API-map.yaml" + }, + { + "path": "Physlib/Units", + "title": "Units", + "requirementsDone": 63, + "requirementsTotal": 67, + "parents": [ + { + "name": "Time", + "path": "Physlib/SpaceAndTime/Time" + }, + { + "name": "Space", + "path": "Physlib/SpaceAndTime/Space" + }, + { + "name": "Mass", + "path": "Physlib/ClassicalMechanics/Mass" + }, + { + "name": "Charge", + "path": "Physlib/Electromagnetism/Charge" + }, + { + "name": "Temperature", + "path": "Physlib/Thermodynamics/Temperature" + } + ], + "url": "https://github.com/leanprover-community/physlib/blob/master/Physlib/Units/API-map.yaml" + } + ] +} diff --git a/web2/scripts/generate-api-map.js b/web2/scripts/generate-api-map.js new file mode 100644 index 0000000..6185165 --- /dev/null +++ b/web2/scripts/generate-api-map.js @@ -0,0 +1,177 @@ +#!/usr/bin/env node +/* + * Generate the API dependency graph for the API Tracker page. + * + * Physlib records the design status of each API in an `API-map.yaml` file + * next to it (Title, ParentAPIs, Requirements with done/location, ...). This + * script walks a clone of leanprover-community/physlib for every such file, + * parses it, and writes the resulting graph to data/APIMap.json. + * + * Why not fetch this at request time (as the page used to, from GitHub + * issues): there is no API that lists "every API-map.yaml in the repo" apart + * from walking the git tree, and doing that from the browser on every page + * load would mean dozens of raw-content fetches against GitHub's anonymous + * rate limit. A local clone makes it one `ls-tree` plus one `show` per file, + * and reuses the same .cache/physlib.git clone the monthly-updates generator + * already keeps around. + * + * Usage: + * node scripts/generate-api-map.js + * node scripts/generate-api-map.js --repo # reuse an existing clone + */ + +const fs = require("node:fs"); +const path = require("node:path"); +const { execFileSync } = require("node:child_process"); +const yaml = require("js-yaml"); + +const OWNER = "leanprover-community"; +const REPO = "physlib"; +const CLONE_URL = `https://github.com/${OWNER}/${REPO}.git`; +const CACHE_REPO = path.join(__dirname, "..", ".cache", "physlib.git"); +const OUT_PATH = path.join(__dirname, "..", "data", "APIMap.json"); +const FILE_NAME = "API-map.yaml"; + +const args = process.argv.slice(2); +function argValue(name) { + const i = args.indexOf(name); + return i >= 0 && i + 1 < args.length ? args[i + 1] : null; +} +const repoArg = argValue("--repo") || process.env.PHYSLIB_REPO || ""; + +// ─── Local git (same approach as generate-monthly-updates.js) ───────────── +let REPO_DIR = ""; + +function git(gitArgs) { + return execFileSync("git", ["-C", REPO_DIR, ...gitArgs], { + encoding: "utf8", + maxBuffer: 1 << 28, + }); +} + +function ensureRepo() { + if (repoArg) { + REPO_DIR = path.resolve(repoArg); + if (!fs.existsSync(path.join(REPO_DIR, ".git")) && !fs.existsSync(path.join(REPO_DIR, "HEAD"))) { + throw new Error(`--repo ${REPO_DIR} is not a git repository`); + } + console.log(`• using existing clone at ${REPO_DIR}`); + } else { + REPO_DIR = CACHE_REPO; + if (!fs.existsSync(REPO_DIR)) { + console.log(`• cloning ${CLONE_URL} → ${path.relative(process.cwd(), REPO_DIR)} (once)`); + fs.mkdirSync(path.dirname(REPO_DIR), { recursive: true }); + execFileSync("git", ["clone", "--bare", CLONE_URL, REPO_DIR], { stdio: "inherit" }); + } + } + try { + git(["fetch", "--quiet", "origin", "+refs/heads/*:refs/remotes/origin/*", "--tags"]); + } catch { + try { + git(["fetch", "--quiet", "--all"]); + } catch { + console.warn(" ⚠ could not fetch; working from whatever the clone already has"); + } + } +} + +function resolveBranchRef() { + const candidates = []; + try { + const remotes = git(["remote", "-v"]) + .split("\n") + .filter(Boolean) + .map((l) => l.split(/\s+/)) + .filter(([, url]) => url && new RegExp(`[/:]${OWNER}/${REPO}(\\.git)?$`, "i").test(url)) + .map(([name]) => name); + for (const r of [...new Set(remotes)]) { + candidates.push({ rev: `${r}/master`, name: "master" }); + candidates.push({ rev: `${r}/main`, name: "main" }); + } + } catch { + /* fall through to the generic candidates */ + } + candidates.push( + { rev: "origin/master", name: "master" }, + { rev: "origin/main", name: "main" }, + { rev: "master", name: "master" }, + { rev: "main", name: "main" }, + ); + for (const candidate of candidates) { + try { + git(["rev-parse", "--verify", "--quiet", candidate.rev]); + return candidate; + } catch { + /* try next */ + } + } + throw new Error(`could not resolve ${OWNER}/${REPO}'s default branch in ${REPO_DIR}`); +} + +// ─── ParentAPIs parsing ───────────────────────────────────────────────────── +// Each entry is normally "Name (path/to/parent)". Some entries are a bare +// path with no name (e.g. "Physlib/Relativity/MinkowskiMatrix.lean") - fall +// back to the path's basename as the display name for those. +function parseParentEntry(entry) { + const trimmed = String(entry).trim(); + const match = trimmed.match(/^(.*)\s\(([^()]+)\)$/); + if (match) { + return { name: match[1].trim(), path: match[2].trim() }; + } + const base = trimmed.split("/").pop().replace(/\.lean$/i, ""); + return { name: base, path: trimmed }; +} + +// ─── Main ─────────────────────────────────────────────────────────────────── +(function main() { + ensureRepo(); + const branch = resolveBranchRef(); + console.log(`• reading API-map.yaml files from ${OWNER}/${REPO}@${branch.name}`); + + const files = git(["ls-tree", "-r", branch.rev, "--name-only"]) + .split("\n") + .filter((f) => f.toLowerCase().endsWith(`/${FILE_NAME.toLowerCase()}`) || f.toLowerCase() === FILE_NAME.toLowerCase()); + + const nodes = []; + for (const file of files) { + const raw = git(["show", `${branch.rev}:${file}`]); + let doc; + try { + doc = yaml.load(raw); + } catch (err) { + console.warn(` ⚠ skipping ${file}: ${err.message}`); + continue; + } + if (!doc || typeof doc !== "object") { + console.warn(` ⚠ skipping ${file}: empty or invalid document`); + continue; + } + + const dir = file.slice(0, file.length - FILE_NAME.length - 1); + const requirements = Array.isArray(doc.Requirements) ? doc.Requirements : []; + const requirementsDone = requirements.filter((r) => r && r.done === true).length; + const parents = (Array.isArray(doc.ParentAPIs) ? doc.ParentAPIs : []).map(parseParentEntry); + + nodes.push({ + path: dir, + title: doc.Title ? String(doc.Title).trim() : dir, + requirementsDone, + requirementsTotal: requirements.length, + parents, + url: `https://github.com/${OWNER}/${REPO}/blob/${branch.name}/${file}`, + }); + } + + nodes.sort((a, b) => a.path.localeCompare(b.path)); + + const out = { + repo: `${OWNER}/${REPO}`, + branch: branch.name, + generatedAt: new Date().toISOString(), + nodes, + }; + + fs.mkdirSync(path.dirname(OUT_PATH), { recursive: true }); + fs.writeFileSync(OUT_PATH, JSON.stringify(out, null, 2) + "\n", "utf8"); + console.log(`• wrote ${nodes.length} API nodes → ${path.relative(process.cwd(), OUT_PATH)}`); +})(); diff --git a/web2/src/app/api-tracker/api-tracker-client.tsx b/web2/src/app/api-tracker/api-tracker-client.tsx index 1ce4a5b..acd045a 100644 --- a/web2/src/app/api-tracker/api-tracker-client.tsx +++ b/web2/src/app/api-tracker/api-tracker-client.tsx @@ -2,43 +2,64 @@ import { useCallback } from "react"; import { GraphvizView } from "@/components/graphviz-view"; +import type { ApiMapNode } from "@/lib/yaml"; -async function buildDot(): Promise { - const res = await fetch( - "https://api.github.com/repos/leanprover-community/Physlib/issues?labels=API&per_page=100", - ); - const data = await res.json(); +function escapeHtml(str: string): string { + return str + .replace(/&/g, "&") + .replace(//g, ">"); +} - if (!Array.isArray(data)) throw new Error("Unexpected API response"); +function escapeDotId(str: string): string { + return str.replace(/"/g, '\\"'); +} - const apiIssues = data.filter((issue: { labels: { name: string }[] }) => - issue.labels.some((l: { name: string }) => l.name === "API"), - ); +function buildDot(nodes: ApiMapNode[]): string { + const byPath = new Map(nodes.map((n) => [n.path, n])); + // Parents referenced by path but with no API-map.yaml of their own get a + // plain node using the first name they were introduced under. + const phantomNames = new Map(); + for (const node of nodes) { + for (const parent of node.parents) { + if (!byPath.has(parent.path) && !phantomNames.has(parent.path)) { + phantomNames.set(parent.path, parent.name); + } + } + } let dot = "digraph G {\n rankdir=TB;\n node [shape=box, style=filled];\n"; - for (const issue of apiIssues) { - const needsReqs = issue.labels.some( - (l: { name: string }) => l.name === "requirements-needed", - ); - const body: string = issue.body ?? ""; - const total = (body.match(/- \[[ x]\]/g) ?? []).length; - const checked = (body.match(/- \[x\]/g) ?? []).length; - - const fillColor = needsReqs ? "#FFCCCC" : "#CCFFCC"; - const rawLabel = issue.title.replace(/"/g, '\\"').replace("API: ", ""); - const subLabel = needsReqs - ? "Next step: Specify requirements" - : `Next step: Build requirements (${checked}/${total})`; - - dot += ` "${issue.number}" [label=<${rawLabel}
${subLabel}>, fillcolor="${fillColor}", URL="${issue.html_url}"];\n`; - - const parentMatch = body.match(/## Parent APIs\s+((?:#\d+\s*)+)/); - if (parentMatch) { - const parents = parentMatch[1].match(/#(\d+)/g) ?? []; - for (const p of parents) { - dot += ` "${parseInt(p.slice(1))}" -> "${issue.number}";\n`; - } + for (const node of nodes) { + let subLabel: string; + let fillColor: string; + if (node.requirementsTotal === 0) { + subLabel = "No requirements defined yet"; + fillColor = "#EEEEEE"; + } else if (node.requirementsDone === node.requirementsTotal) { + subLabel = "Complete"; + fillColor = "#CCFFCC"; + } else if (node.requirementsDone === 0) { + subLabel = `Next step: build requirements (0/${node.requirementsTotal})`; + fillColor = "#FFCCCC"; + } else { + subLabel = `${node.requirementsDone}/${node.requirementsTotal} requirements done`; + fillColor = "#FFE8A3"; + } + + const label = escapeHtml(node.title); + const id = escapeDotId(node.path); + dot += ` "${id}" [label=<${label}
${subLabel}>, fillcolor="${fillColor}", URL="${node.url}"];\n`; + } + + for (const [nodePath, name] of phantomNames) { + const id = escapeDotId(nodePath); + dot += ` "${id}" [label=<${escapeHtml(name)}>, fillcolor="#FFFFFF"];\n`; + } + + for (const node of nodes) { + for (const parent of node.parents) { + dot += ` "${escapeDotId(parent.path)}" -> "${escapeDotId(node.path)}";\n`; } } @@ -46,7 +67,7 @@ async function buildDot(): Promise { return dot; } -export function APITrackerClient() { - const getDot = useCallback(() => buildDot(), []); +export function APITrackerClient({ nodes }: { nodes: ApiMapNode[] }) { + const getDot = useCallback(() => Promise.resolve(buildDot(nodes)), [nodes]); return ; } diff --git a/web2/src/app/api-tracker/page.tsx b/web2/src/app/api-tracker/page.tsx index 54fb2e6..e75a7d7 100644 --- a/web2/src/app/api-tracker/page.tsx +++ b/web2/src/app/api-tracker/page.tsx @@ -1,24 +1,27 @@ import type { Metadata } from "next"; +import { getApiMap } from "@/lib/yaml"; import { APITrackerClient } from "./api-tracker-client"; export const metadata: Metadata = { title: "API Tracker | Physlib", description: - "Visualize the API dependency graph for Physlib based on GitHub issues.", + "Visualize the API dependency graph for Physlib based on its API-map.yaml files.", }; -export default function APITrackerPage() { +export default async function APITrackerPage() { + const { nodes } = await getApiMap(); + return (

API Tracker

- This graph visualizes the API-related issues for Physlib. Feel free to - explore the issues and help where you can! This graph does not currently - show progress of the APIs being built, as some issues have not yet - defined their requirements, even though the requirements may already - exist in Physlib. + This graph visualizes the APIs defined across Physlib, built from each + API's API-map.yaml file. Green nodes have all their + requirements done, yellow nodes are in progress, and red nodes have no + requirements done yet. White nodes are referenced as a parent API but + don't have their own API-map.yaml yet.

- +
); } diff --git a/web2/src/lib/yaml.ts b/web2/src/lib/yaml.ts index cd39a34..f628b6a 100644 --- a/web2/src/lib/yaml.ts +++ b/web2/src/lib/yaml.ts @@ -76,6 +76,32 @@ export async function getTodo(): Promise { return loadYaml("TODO.yml"); } +// ─── API map ──────────────────────────────────────────────────────────── +export type ApiMapParent = { + name: string; + path: string; +}; + +export type ApiMapNode = { + path: string; + title: string; + requirementsDone: number; + requirementsTotal: number; + parents: ApiMapParent[]; + url: string; +}; + +export type ApiMap = { + repo: string; + branch: string; + generatedAt: string; + nodes: ApiMapNode[]; +}; + +export async function getApiMap(): Promise { + return loadJson(path.join(dataDir, "APIMap.json")); +} + // ─── Monthly updates ────────────────────────────────────────────────────── export type MonthlyContributor = { login: string | null; From 78fe175d458a0120ca322ab8900721698c401b02 Mon Sep 17 00:00:00 2001 From: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com> Date: Tue, 18 Aug 2026 18:44:29 +0100 Subject: [PATCH 2/3] added sidebar --- .../skills/physlib-design-language/SKILL.md | 137 ++++++++++++++++++ .../app/api-tracker/api-tracker-client.tsx | 76 ++++++++-- web2/src/app/api-tracker/page.tsx | 3 +- web2/src/app/api/api-map/route.ts | 11 ++ .../api-tracker/api-tracker-sidebar.tsx | 101 +++++++++++++ web2/src/components/conditional-sidebar.tsx | 2 + web2/src/lib/api-map-tree.ts | 74 ++++++++++ 7 files changed, 394 insertions(+), 10 deletions(-) create mode 100644 .claude/skills/physlib-design-language/SKILL.md create mode 100644 web2/src/app/api/api-map/route.ts create mode 100644 web2/src/components/api-tracker/api-tracker-sidebar.tsx create mode 100644 web2/src/lib/api-map-tree.ts diff --git a/.claude/skills/physlib-design-language/SKILL.md b/.claude/skills/physlib-design-language/SKILL.md new file mode 100644 index 0000000..aeecb05 --- /dev/null +++ b/.claude/skills/physlib-design-language/SKILL.md @@ -0,0 +1,137 @@ +--- +name: physlib-design-language +description: Design language, layout, and data-generation conventions for the Physlib website (web2 Next.js app). Load before adding or modifying any page, component, or data-generation script in web2, so new UI matches the rest of the site instead of inventing a one-off layout. +--- + +# Physlib website design language + +This site (`web2/`) has established, repeated conventions. New pages should +reuse them rather than build ad-hoc layouts — a page that looks or is wired +differently from its siblings is a design bug, not a stylistic choice. + +## Page shell + +Every content page wraps its content the same way: + +```tsx +
+

Page Title

+

Intro copy.

+ {/* page content */} +
+``` + +`max-w-5xl` is the default. Don't widen it to fit extra UI (e.g. a sidebar) — +see below, sidebars are not page content. + +## Root layout & the left sidebar slot + +`src/app/layout.tsx` renders a persistent flex row: + +``` + +
+ +
{children}
+
+``` + +`ConditionalSidebar` (`src/components/conditional-sidebar.tsx`) picks a +sidebar by route: + +```ts +if (pathname === "/") return null; +if (pathname.startsWith("/monthly-updates")) return ; +if (pathname.startsWith("/api-tracker")) return ; +return ; // default: auto-built from h2/h3 on the page +``` + +**If a new page needs left-rail navigation (a list of items, a tree, a table +of contents), add a branch here and a dedicated sidebar component.** Do not +build the sidebar inline inside the page/client component with a local flex +layout — that duplicates the shell, breaks the shared sticky/scroll behavior, +and is the mistake this skill exists to prevent (it's what the API Tracker +page did on the first pass, before being corrected to match this pattern). + +### Sidebar visual pattern + +Every left sidebar (`TableOfContents`, `MonthSidebar`, `ApiTrackerSidebar`) +uses the same markup: + +```tsx + +``` + +- Hidden below `lg`; sticky at `top-16`, independently scrollable + (`max-h-[calc(100vh-4rem)] overflow-y-auto`). +- Active item = `text-accent font-medium` + a small accent dot prefix. Inactive + = `text-muted hover:text-foreground`. +- Nested/indented levels use extra left padding (either a Tailwind step like + `pl-6` for a fixed two-level case, or `style={{ paddingLeft: 8 + depth * 16 }}` + for an arbitrary-depth tree) — never a second nested `