Live: https://qed64-showcase.fawadworkaddress.workers.dev/showcase/ (first deployed 2026-10-05; since 2026-11-05 pin O, serving the packages' v4.35.0 builds; Chromium-based desktop browser, ~16 GB RAM; first visit downloads ~680 MB).
Eight InfoView widget packages for Lean 4 and Mathlib (v4.35.0), and two ways to see them without installing anything: a static gallery of their real panels, and the widgets running live in QED64, Lean compiled to wasm64 and running in the browser. Everything in this repository builds from a clone.
The v4.32.2 original of the packages is the git tag
lean-v4.32.2. The port to v4.34.0 exists because
QED64 pairs its snapshots to Lean 4.34.0 and Mathlib 5ed2965; the last v4.34.0 state is commit 4d93a28 (branch
qed64-pin-i). The packages are now on Lean v4.35.0 / Mathlib v4.35.0 (56a00585). The QED64 showcase has two
registered pins (qed64-showcase/pins/): O 521cf3f, live, on QED64's Lean 4.35.0 runtime with overlays baked from
these v4.35.0 packages, and N 58ebbad, on Lean 4.34.0 with overlays baked from the v4.34.0 packages. Every package has a PORT-NOTES.md that lists what changed and why
(v4.34.0 → v4.35.0, v4.32.2 → v4.34.0).
| Part | Directory | What it is | Build and test from a clone |
|---|---|---|---|
| Widget packages | packages/ |
The eight packages (table below) and lean-widget-kit, which re-exports all of them. Each is a self-contained Lake project with a compile-time test suite. |
./test-all.sh |
| Static showcase | showcase/ |
A static site with every widget's real panels: the Html trees the InfoView receives, rendered through the same React conversion. Deployed to GitHub Pages when enabled. |
./showcase/build.sh && node showcase/verify.mjs |
| QED64 showcase | qed64-showcase/ |
The widgets live in the stock, unmodified QED64 page: a gallery at /showcase/ that drives QED64's editor and InfoView. It also holds the pins, native build, snapshot bakes, the Playwright UX suite and the Cloudflare deploy kit. QED64 itself is the git submodule qed64-showcase/deps/qed64. |
qed64-showcase/scripts/showcase.sh bootstrap --origin <origin>, then verify, gallery, ux |
| CI | .github/workflows/, ci/ |
lean-ci.yml (packages, static showcase, QED64-showcase static gates, optional Pages) and qed64-deploy.yml (QED64 showcase to Cloudflare). ci/run-local.mjs runs any job on your machine in a fresh clone. |
node ci/run-local.mjs --workflow .github/workflows/lean-ci.yml |
packages/<name>/ the eight widget packages + lean-widget-kit (Lake projects)
showcase/ static gallery: probes/ (dump scripts), dumps/ (committed panel dumps), build.sh, verify.mjs
qed64-showcase/ the widgets in the QED64 page
deps/qed64 QED64 at the served pin (git submodule, github.com/FawadHa1der/QED64)
pins/<id>/ per QED64 pin: pin.json and QED64.lock.json (sha256 of every file that is served)
gallery/ the /showcase/ page (rail of 8 examples, iframe of the stock page, QED64's embedding API)
scripts/ showcase.sh (one entry point), build-shell, fetch-artifacts, serve, deploy scripts, …
tests/ux/ Playwright UX suite (35 tests)
infra/ Cloudflare Worker (worker.js), its tests, wrangler pin, committed UX verdict record
lean/ widget examples, native goldens, native delta lists
docs/ architecture, build from source, deploy, results, history
test-all.sh lake build + lake test in every package, with a summary table
.github/workflows/ lean-ci.yml, qed64-deploy.yml
ci/ run-local.mjs (local workflow runner), install-elan.sh, rehearse-deploy.sh
git clone --recursive https://github.com/FawadHa1der/lean-widgets.git
cd lean-widgets
# an existing clone without the submodule: git submodule update --init| You want to | You need |
|---|---|
| build and test the packages | elan (each package pins leanprover/lean4:v4.35.0), git, about 8 GB of disk per Mathlib-dependent package (each package fetches its own Mathlib build cache) |
| build the static showcase | the packages built (to regenerate the dumps), Python 3, Node (any recent version) |
| run the QED64 showcase | Node 26 with npm (the lock records v26.3.0; another 26.x is reported as a DRIFT), git, an artifact origin, about 2.4 GB of disk for the artifacts; macOS or Linux |
| run its browser tests | Playwright's Chromium (npx playwright install chromium chromium-headless-shell), 16 GB of RAM |
| rebuild its snapshot overlays (rarely) | the wasm64 kernel fork's toolchain, Docker, a large machine: heavy path |
./test-all.sh # lake build + lake test in all 9 packages; prints a GREEN/FAILED table, exit 1 on any failureOne package at a time:
cd packages/interval-inspector # or any package directory
lake exe cache get # once, for the packages that depend on Mathlib (see the table below)
lake build && lake testThe tests are compile-time assertions (#guard, #guard_msgs, throwing MetaM asserts): a failing assertion is a
build error. To see a widget, open the package folder in VS Code with the Lean 4 extension and open
<Lib>/Demo.lean (Quick start).
./showcase/build.sh # regenerate showcase/dumps/ from showcase/probes/ (needs the packages built), assemble showcase/site/
./showcase/build.sh --no-dump # or assemble from the committed dumps only (no Lean needed)
node showcase/verify.mjs # every panel through React's development checks in Node; exit 1 on any error or warning
open showcase/site/index.html # the gallery (site/verify.html is the same check in a browser)After ./showcase/build.sh, git status must show no change under showcase/dumps/: the committed dumps are
exactly what the probes produce. CI checks this. Details: showcase/README.md.
The light path serves and tests the showcase without building QED64's binaries or the widget snapshots. Run it in
qed64-showcase/:
cd qed64-showcase
cp .env.example .env.local # optional: QED64_SHOWCASE_WORK (work dir, no spaces), artifact origins
scripts/showcase.sh bootstrap --origin <artifact origin>
scripts/showcase.sh verify # chain of trust: sources, page, binaries and overlays against the lock
scripts/showcase.sh gallery # static gallery gate (check-gallery + sim-gallery), prints the gallery hash
scripts/showcase.sh serve # http://localhost:5190/showcase/ (stop: scripts/showcase.sh stop)
npx playwright install chromium chromium-headless-shell
scripts/showcase.sh ux # the Playwright UX suite (35 tests, 25–40 min; one browser at a time on the host)bootstrap checks out QED64's sources (the submodule), builds QED64's page from them with QED64's own build and
installs it only if all its files are byte-identical to the committed lock. It then fetches QED64's binaries and the
widget overlays by path from the artifact origin and checks every file's sha256 against the lock, links the served pin
and runs verify. So an origin never has to be trusted. --origin is the deployed showcase (for its deployed pin's runtime and packs), or scripts/serve.mjs
of a checkout that has the artifacts (PORT=5297 scripts/showcase.sh serve there). --qed64-origin https://qed64.fawadworkaddress.workers.dev serves QED64's own files. The deployed Worker has only the overlays uploaded
to it (since 2026-11-05 O's widgets8.<runtime id>/); any other pin's overlays exist only where they were baked until
they are uploaded.
Other checks: node scripts/check-portable.mjs (no machine path in code or configuration),
node scripts/deploy-manifest.mjs --check (deploy gates), node --test infra/worker.test.mjs (the Worker),
scripts/showcase.sh pin list (registered QED64 pins and their UX verdicts). scripts/showcase.sh headless controls
(the wasm runtime in Node, no browser) needs the build stores of the heavy path, so in a bootstrapped clone verify
lists those stores as ABSENT.
Full guide: qed64-showcase/docs/BUILD-FROM-SOURCE.md. Everything
showcase.sh can do: qed64-showcase/README.md.
npm ci --prefix ci
node ci/run-local.mjs --workflow .github/workflows/lean-ci.yml # every job, each in a fresh clone of HEAD
node ci/run-local.mjs --workflow .github/workflows/lean-ci.yml --job qed64-static
ci/rehearse-deploy.sh # the deploy job against local fakes (macOS, after rehearse.sh all)run-local.mjs runs the run: steps of the committed workflow file as GitHub would (shell flags, working
directories, env, outputs, if:, needs, matrix, timeout-minutes) and lists every place where it differs from a
GitHub runner. A full lean-ci run clones Mathlib once per Mathlib-dependent package, so it needs about 50 GB of disk.
visitor's browser ── /showcase/ ──► gallery (rail of 8 examples)
│ iframe, same origin
▼
/ ?snapshots=snapshots/<dir> ──► the STOCK QED64 page, built from deps/qed64, unmodified
│ fetches
▼
/runtime/ /profiles/ /snapshots/ QED64's wasm64 runtime, packs and stock snapshots
/snapshots/<dir>/ our snapshot region: Mathlib + the eight packages
<dir> is the pin's served overlay directory, widgets8.<runtime id> (widgets8.36d7f415704473d9 on O), so each
runtime's region has its own directory and a new runtime's upload never replaces the one a live page reads. The
gallery's ?overlay=widgets8 maps to it. (The retired pins up to H used the bare widgets8 and widgets7; since P2 there
is one overlay.)
- QED64 is a dependency, never a copy. Its sources are the submodule
qed64-showcase/deps/qed64at the served pin's commit. Several QED64 commits can be registered as pins (pins/<id>/); one is active. Each pin'sQED64.lock.jsonrecords the sha256 of every file that is served. - The widgets reach the browser as a snapshot region. The packages are compiled to oleans with the kernel fork's
native64 compiler, staged on top of QED64's served Mathlib tree and baked by QED64's pinned wasm runtime into a
snapshot (
widgets8: the eight packages). QED64 loads it like its ownmathlibregion, so the example files start with a plainimport Mathlib/import HasseViewand also work in VS Code. - The gallery iframes the stock page from the same origin, checks that the region is paired with the runtime
before navigating, and drives the editor and the cursor through QED64's declared embedding API v1 (
qed64.api,?embed=1,#code=), which both registered pins, O521cf3f(QED64 main on the kernel fork's releaselean-v4.35.0-b081e7c, Lean 4.35.0; live since 2026-11-05) and N58ebbad(QED64 main onlean-v4.34.0-53cb11e, Lean 4.34.0), provide (gallery/README.md "Embedding API v1"). The pins A–L are retired and kept at the git tagpins-history-2026-11-07, which is the commitb24587d(git show b24587d:qed64-showcase/pins/<id>/pin.jsonreads one without the tag); until then the gallery also had a legacy mode for the pre-v1 pages A–E, which used the page's internal hooks and a small bridge for three InfoView defects of those pages (D1, D2, D3 in the upstream report). Hbf9d947, live from 2026-10-08 to 2026-11-05, is the rollback target. - Tests: a static gate (
showcase.sh gallery), headless wasm checks in Node, and the Playwright UX suite. Every fulluxrun is recorded with the gallery, lock and overlay hashes it ran on. A run is a VERDICT only if it was green on unchanged inputs, and a deploy needs a verdict on exactly the inputs it deploys.
In depth: ARCHITECTURE.md (how QED64 is consumed and which QED64 internals are used), qed64-showcase/README.md (pins, results, limitations: visitors need a Chromium-based desktop browser and 16 GB of RAM, and a first visit downloads about 700 MB).
The QED64 showcase is hosted on Cloudflare the way lean4game and QED64 are: a Worker qed64-showcase serves the
shell (QED64's page and the gallery, about 18 MB of static assets) and streams the artifacts from the R2 bucket
qed64-artifacts: the runtime and the packs (1.26 GB at pin O) from the kernel's toolchain release under
lean4-wasm64/<release id>/, never uploaded by us, and the stock snapshots, our overlays and the indexes (1.11 GB at pin O's upload, 0.745 GB from P2 on, with one overlay)
under the prefix qed64-showcase/, with the cross-origin isolation headers the wasm runtime needs. (H, the rollback
target, reads its own copy of the runtime and packs under that prefix.) A release has two steps:
- Artifacts to R2, from the machine that has them:
scripts/upload-artifacts.sh(rclone, copy only, never sync; the bucket is shared with QED64 and lean4game, so it refuses QED64's root and their prefixes, and any prefix other thanqed64-showcase/needs an explicit override). CI never uploads artifacts, so no R2 key is ever stored in GitHub. The upload runs in three phases (digest-named objects, then the indexes no older shell reads, then the shared indexes); a pin on a new runtime replaces the live stock and profile indexes only in the last phase, andPHASES=can hold that phase back until the new shell is live (by hand, withALLOW_PARTIAL_UPLOAD=1; a CI deploy refuses until phase 3 is up: DEPLOY-CLOUDFLARE.md §3.2). - The shell to the Worker, either locally with
scripts/deploy-app.sh, or from GitHub Actions:qed64-deploy.ymlruns on pushes tomainthat touchqed64-showcase/and on manual dispatch. It builds QED64's page from the submodule (byte-identical to the lock), runs the gallery gate, requires the committed UX verdict recordqed64-showcase/infra/ux-verdict.jsonto match the gallery, lock and overlays it deploys, runswrangler versions upload, checks every asset and artifact on that version's preview URL (Preview URLs must be on for the Worker), runswrangler versions deployand smoke-tests the deployed URL. Without the secretsCLOUDFLARE_API_TOKENandCLOUDFLARE_ACCOUNT_IDit logs a skip line and deploys nothing.
Both paths are rehearsed locally against fakes (scripts/deploy-rehearsal/rehearse.sh all, ci/rehearse-deploy.sh):
an rclone local backend and a local S3 endpoint for R2, wrangler versions upload --dry-run and wrangler dev --local, inside
a macOS sandbox that blocks outbound traffic. Release routing passed both rehearsals (2026-11-02 to 11-04: rehearse.sh all browser stop
on dbfd000, all nine ci/rehearse-deploy.sh scenarios on eca8f22; qed64-showcase/docs/DEPLOY-CLOUDFLARE.md).
P1 and P2 (pins A–L and the gallery's legacy mode retired, one overlay; the local branch p1-p2, not pushed yet) were
re-gated on 2026-11-07, with the UX verdict p12r-full2 committed in fb3174a, and rehearsed (all OK on 8362a6f;
rehearsed again on fb3174a, result in qed64-showcase/docs/REPIN-LOG.md); they deploy with one push of that branch to
main and no upload
(NEXT-STEPS.md). The owner's steps for the first real deploy (token scope, the two secrets, Preview URLs, the SHOWCASE_ORIGIN
variable) are the
first deploy checklist.
The static showcase deploys to GitHub Pages from lean-ci.yml, only on a push to main with the repository variable
DEPLOY_GITHUB_PAGES=true and Settings → Pages → Source set to "GitHub Actions", and only from a fully green suite.
Current state is printed by commands, not written here: ./test-all.sh, node showcase/verify.mjs, and in
qed64-showcase/ scripts/showcase.sh verify, scripts/showcase.sh gallery (UX CURRENT … names the newest
verdict on exactly the current gallery, lock and overlays, or says UX STALE), scripts/showcase.sh pin list and
node scripts/deploy-manifest.mjs --check. Dated records of full test rounds:
qed64-showcase/docs/results/REPO-TEST-ROUND.md (the whole
repository, main checkout and a fresh clone), qed64-showcase/docs/UX-RESULTS.md
and qed64-showcase/docs/REPIN-LOG.md.
Eight production-quality InfoView widget packages: the top-3 recommendations from the
visualization research (not part of this repository), a proof-state-integrated
graph visualizer, a universal tree/heap visualizer, and the three
next-frontier builds: Hasse diagrams, exact
probability distributions, and verified charting primitives. Every package is a self-contained Lake project on
Lean v4.35.0, builds green, and ships an adversarially-audited compile-time
test suite (lake test) — including mutation testing (deliberate logic mutations
must break the suite).
The Assertions column is each package's census on the v4.35.0 tree, counted mechanically with the method its
README states (2026-10-26, rechecked 2026-10-27); the Audit column records the packages' original audits (each port's audits are in its
PORT-NOTES.md).
| Package | What it does | Deps | Assertions | Audit |
|---|---|---|---|---|
interval-inspector/ |
Draws interval goals as a theme-aware SVG number line (open/closed endpoint glyphs, stacked subset/eq comparisons, mismatch shading, order-unknown captions) and suggests the right Mathlib lemma from a 62-entry table where every lemma is proof-verified against pinned Mathlib, side conditions checked ready/missing against an order graph built from your hypotheses. Recognizes Set.Icc/…/Iio, ∪/∩ trees, set-builder spellings ({x | a ≤ x ∧ x < b} → Ico), and Set.Nonempty / = ∅ / ≠ ∅ shapes. #interval_inspect + panel + interval_inspect? tactic with click-to-insert. |
Mathlib | 857 | pass (3 audited rounds, 6/6 mutations) |
expr-xray/ |
Elaborated-expression inspector: collapsible tree with binder-role classification, universe levels, coercion badges, four preset views, pp.explicit block — and a defeq-aware diff: every mismatch is checked with isDefEq (reducible, then default transparency), re-ranked so definitionally real blockers come first, with an "all mismatches are defeq — syntactic only" verdict when nothing truly differs. #xray / #xray_diff + shift-click panel (1 selection = inspect, 2 = compare). |
ProofWidgets | 480 | pass (3 audited rounds, 6/6 mutations) |
simp-lens/ |
simp_lens — a drop-in simp with full location support (at h, at h ⊢, at *): per-location rewrite filmstrips (origin, before/after, hover/go-to-def), the minimal Try this: simp only [...] at … (reusing core's mkSimpOnly), and per-lemma exclusion previews with essential/redundant badges. Equivalence tests execute the generated call and assert it reaches the same state as simp. |
ProofWidgets | 428 | pass (3 audited rounds, 6/6 mutations) |
graph-scope/ |
#graph_scope g — evaluates a concrete SimpleGraph through its own Fintype/DecidableRel instances and draws a theme-aware SVG: circular layout, stats (order/size/degrees/components/connectivity/bipartiteness), walk overlays with step numbers, highlight rings for vertex subsets. Bipartiteness returns validated evidence — a proper 2-coloring or an odd-cycle witness the tests verify programmatically. All analysis is pure #guard-testable code over an extracted edge list. Click-to-insert (RPC panel): edges insert example : (g).Adj a b := by decide, vertices insert degree facts, and the stats line inserts (dis)connectivity facts — gated by a calibrated cost model (kernel decide on Connected enumerates Mathlib's walks: the panel counts that walk work exactly, measures one adjacency decision of the graph's own instance, and offers the link only when the heartbeat estimate stays within half the default maxHeartbeats; since the v4.35.0 port, which replaced a diameter/size budget that was unsound at its corner and kept that budget's limits as the recursion-depth domain). All texts round-trip-gated and compile-verified. |
Mathlib | 513 | pass (3 audited rounds + polish, 7/7 mutations) |
tree-scope/ |
#tree_scope v — universal tree/heap visualizer: a ToTreeView typeclass with semantic instances (core RBNode/RBMap rendered in true red/black with red-red, black-height, and BST-order violation overlays using the type's own cmp; Batteries.BinomialHeap forests with rank badges and heap-property checks via the type's le; Mathlib Tree; Std.TreeMap), plus a constructor-reflection fallback that renders any concrete inductive value (whnf-evaluated, not Repr). #tree_evolve filmstrips a fold of operations with per-step added-node diff badges — watch RB rebalancing happen. Exact-ℚ tidy layout with proven non-overlap/centering/translation-invariance properties; Catalan gallery demo (all 14 four-node trees). |
Mathlib | 500 | pass (2 audited rounds + polish, 4/4 mutations) |
hasse-view/ |
#hasse V — layered Hasse diagrams for any finite decidable order (fills the Zulip request open since Jan 2022): covering relation computed from the extracted ≤ table, ⊥/⊤/atom/coatom badges, lattice verdict with a concrete no-join witness pair, upset/downset shading, height and antichain bounds — and validity self-checks that warn about non-antisymmetric/non-transitive instances instead of drawing them wrong. Click-to-insert (RPC panel): cover edges insert example : a ⋖ b := by decide (the package ships its own lawful DecidableRel (· ⋖ ·) instance for [Preorder] [DecidableLE] [Fintype] orders; Mathlib v4.35.0's new instance needs DecidableLT, which products and the bowtie demo lack), ⊥/⊤ badges insert instance-free bound facts, and the non-lattice caption inserts the compiled no-join witness; every offered text is round-trip-gated and compile-verified. Demos: the powerset cube, divisors of 12 (shows the gate rejecting unparseable labels), a non-lattice bowtie. |
Mathlib | 476 | pass (2 audited rounds, 5/5 mutations) |
dist-lens/ |
#dist / #dist_film / #chain — exact probability distributions (probe-validated architecture): whitelist extraction of PMF terms to exact ℚ weights (uniform/bernoulli/binomial/pure/bind/map/ofFintype; the uniform constructors are DistLens.uniformOfFintype / DistLens.uniformOfFinset since Mathlib v4.35.0 made its uniform PMFs measures), bars + CDF + E/Var with fraction labels, bind-convolution filmstrips, and finite Markov chains with exact Gaussian-elimination stationary distributions. Ships the pmf_num tactic: every displayed weight offers a click-to-insert compiled proof example : p x = 1/6 := by pmf_num — including bernoulli's truncated-subtraction residues and stationary equations. |
Mathlib | 401 | pass (r1, 2/2 mutations + polish) |
chart-kit/ |
Verified-exact charting primitives (the demand-backed build): ChartSpec → Html library for widget authors + #chart command — bar/line/step/scatter marks over exact ℚ data, nice-tick computation entirely in ℚ (no Float in the math), categorical bars, legends, themed palette, and Series.ofFloats with bit-exact IEEE-754 decoding (0.1 charts as its true rational value; NaN/∞ refused by name). |
ProofWidgets | 261 | pass (r1, 2/2 mutations + polish) |
Each package README documents its architecture and an honest LIMITATIONS section (e.g. the live panel round-trip needs a running Lean server and was verified headlessly at the HTML-assembly level, not by driving VS Code).
Each package is independent. In VS Code:
cd packages/interval-inspector # or any of the eight package directories
lake buildthen open the package folder in VS Code with the Lean 4 extension and open
<Lib>/Demo.lean — every demo elaborates on build, so what you see is tested.
Run a package's test suite (compile-time assertions; a failing #guard /
#guard_msgs / assert is a build error):
lake testNote: interval-inspector, graph-scope, tree-scope, hasse-view and dist-lens depend on Mathlib — run
lake exe cache get before the first build if you cloned them fresh.
Add to your lakefile.toml, either from git (the package lives in a subdirectory of
this repository):
[[require]]
name = "interval-inspector" # or any of the eight packages
git = "https://github.com/FawadHa1der/lean-widgets"
rev = "main" # better: a commit hash
subDir = "packages/interval-inspector"or from a local checkout:
[[require]]
name = "interval-inspector"
path = "path/to/lean-widgets/packages/interval-inspector"All eight (and lean-widget-kit) pin leanprover/lean4:v4.35.0 and ProofWidgets
df72b022e558978a1c50264cfc4d7fec86fa8e04 (the rev in Mathlib v4.35.0's manifest, so mixing with Mathlib v4.35.0
projects is safe). The five Mathlib-dependent packages and the kit also pin Mathlib v4.35.0 (rev 56a00585), and
every other rev in their manifests (Batteries 66e46918, Aesop, Qq, plausible, importGraph, LeanSearchClient, Cli)
is Mathlib v4.35.0's own.
- Implemented and then improved by parallel agents against detailed specs derived
from the research phase (not part of this repository), grepping the pinned local sources
(toolchain
src/lean/, vendored ProofWidgets/Mathlib) as API ground truth. - Every implementation and every improvement round was audited by fresh adversarial agents: full rebuild, every file read, stub/fake hunting, assertion census, README-claim verification, and two mandatory mutations per round that the test suite had to catch. Improvement audits additionally enforced no-regression: baselines could only grow, and every snapshot change needed a written justification.
- The process caught real bugs: an inverted suggestion side-condition direction
that survived 408 assertions (fixed with direction-pinning tests), an
Expr.eqvbinder-annotation blind spot, and a weak component invariant that let a BFS mutation slip one test layer (strengthened and re-mutation-tested). - A dedicated adversarial bug-hunt round (six hunters, evidence-only rule:
every finding needs an executed repro) then found 43 findings — 13 major —
including ALL-READY lemma suggestions on provably false statements (missing
typeclass gating), ℕ division literals valued as rationals, continuum-semantics
mismatch shading over discrete types, a timeout that escaped
catchand failedsimp_lenswheresimpsucceeds, and false "NOT defeq" verdicts on metavariable-containing terms. Every fix round was audited by re-executing the original repros (33/34 verified fixed; the 34th is a documented stretch item) — and one fix round caught a real bug in another agent's fix (mkAppMleaving trailing instance args unapplied in the gating check). - Test philosophy: all tests are compile-time (
#guard,#guard_msgs, throwing MetaM asserts), deterministic on the pinned toolchain; CI needs nothing butlake— or./test-all.shfor the whole suite (incl. thelean-widget-kitmeta-package: one require +import LeanWidgetKit= the entire suite). Combined: 3,916 assertions across the eight packages (the sum of the census column above). The frontier builds were specced directly from probe-verified feasibility research — dist-lens's proof tactic implements a closer chain validated by executed probes before a line of the widget existed.
Ported in place on the branch port-lean-4.35 (from qed64-pin-i, commit 4d93a28): Lean v4.35.0, Mathlib
v4.35.0 (56a00585), ProofWidgets df72b022 (Mathlib v4.35.0's manifest rev). Each package's pins were set with one
lake update (plus lake exe cache get where Mathlib is a dependency), then the package was ported and adversarially
audited (pin check, census, mandatory mutations, re-execution of every claimed transcript); the findings were fixed.
simp-lens, hasse-view, dist-lens and graph-scope were then re-audited: the re-audit passed simp-lens (two more
#lens_origins pins) and hasse-view (a correction to its PORT-NOTES.md), and failed dist-lens and graph-scope, which
went through a second round of library fixes. chart-kit, expr-xray, interval-inspector and tree-scope record a single
audit and its fixes. Two packages needed library code changes: dist-lens (a Mathlib API removal) and graph-scope
(Mathlib's new decidability instances exposed a connectivity link budget that was unsound at its corner, very likely
since before the port).
No test was weakened; the only changed expected outputs are documented in the packages' PORT-NOTES.md. Counts are
the package census (the README method), recounted mechanically on both trees.
| Package | Changes | Assertions (4.34.0 → 4.35.0) |
|---|---|---|
chart-kit |
none (documentation only) | 261 → 261 |
expr-xray |
none in the library; tests for coercions detected only through @[coe] |
459 → 480 |
tree-scope |
none in the library; PanelTests pins what #tree_scope / #tree_evolve store in the panel |
476 → 500 |
hasse-view |
docstrings only (Mathlib's new CovBy instance made one statement false); tests pin which ⋖ instance is selected and why the package's own is still needed |
463 → 476 |
simp-lens |
none in the library; tests pin per-frame origin lists, including the simproc .continue (some _) path that Lean 4.35's simprocCore change touched |
404 → 428 |
interval-inspector |
none in the library; ℕ end-to-end tests of the DenselyOrdered gate on the ≠ ∅ suggestion |
846 → 857 |
graph-scope |
Gate.lean: an adjacency-cost guard for Mathlib's new quantifying hasse / pathGraph instances; Insert.lean + Gate.lean: a walk-work cost model calibrated on measured heartbeats (250 calibration graphs, validated on 50 more) replaces the connectivity link's diameter/size budget as its cost bound; the diameter/size limits stay as the recursion-depth domain, and a recursion-depth estimate (≤ 500) replaces the disconnected graphs' max-degree ≤ 2 proxy; tests for both |
426 → 513 |
dist-lens |
new DistLens/Uniform.lean with DistLens.uniformOfFintype / DistLens.uniformOfFinset (Mathlib v4.34.0's definitions, with Apache-2.0 attribution, LICENSE-APACHE-2.0 and NOTICE); the extractor whitelist and pmf_num's simp set name them; a hint when a refused term is Measure-valued |
357 → 401 |
lean-widget-kit |
none (one docstring pointer corrected) | no assertions of its own |
| Total | 3,692 → 3,916 |
(Two 4.34.0 figures differ from the v4.32.2 → v4.34.0 table below: expr-xray's 459 is the corrected census, where
the old grep said 456 because it missed 10 bare #guard lines, counted 2 docstring mentions of #guard_msgs and
counted the 5 helper definitions; dist-lens's 357 includes StackGuardTests, added on 2026-10-12 after that port's
345.)
User files must name the DistLens constructors: DistLens.uniformOfFintype / DistLens.uniformOfFinset, or the bare
names under a top-level open DistLens (as in open PMF DistLens). That covers files that spelled
PMF.uniformOfFintype / PMF.uniformOfFinset, and also the v4.34 idiom of the bare uniformOfFintype under
open PMF alone (the usage block of dist-lens's v4.34 README, and QED64's showcase example): with import Mathlib
the bare name now means Mathlib's Measure-valued alias and fails, and with import DistLens alone it does not
resolve. An open DistLens written inside namespace Foo.DistLens opens Foo.DistLens instead (dist-lens
PORT-NOTES.md, gotcha 2). The static showcase dumps were regenerated on 4.35 and are byte-identical to the v4.34.0
ones (see showcase/README.md). The QED64 showcase's served pins are unaffected until it is
re-pinned: each pin's QED64.lock.json records the widgets commit its overlays are built from (WIDGETS_COMMIT,
exported with git archive <commit> packages/), and every registered pin names a v4.34.0 tree (90e415c or
6b31bba). Two things do see the port: once it is committed, showcase.sh verify reports a DRIFT on #7
(HEAD:packages is no longer WIDGETS_COMMIT:packages), and the native golden generator and gates
(qed64-showcase/lean/goldens/, which write the goldens in lean/expect/) compile against the working tree's
packages/, which is now on v4.35.0. The re-pin also needs the dist-lens example fix: the top-level open PMF
of qed64-showcase/lean/examples/dist-lens.lean becomes open PMF DistLens (dist-lens
PORT-NOTES.md, F5).
4.35.0 gotchas worth knowing:
- Mathlib v4.35.0 (#42909, part of deprecating
PMF, #42821) removedPMF.uniformOfFinsetand madePMF.uniformOfFintypea deprecated alias of the Measure-valueduniformOfFinset. Name literals (``PMF.uniformOfFintype) still compile, soisAppOfAritymatchers silently stop matching, and lemma names inside syntax quotations fail only at run time: grep every use of a changed name, not just the build errors. - Mathlib v4.35.0 (#40728) adds
DecidableRelinstances forCovBy/WCovByon finite orders and forSimpleGraph.hasse/pathGraph, and removes the Bool-onlyCovByinstances. The new graph instances quantify over the vertex type, so kerneldecidethrough them can be far more expensive than through a closed adjacency. - Simprocs stop at the first rewrite per visit (
simprocCore/dsimprocCore): a tracer wrappingSimp.Methodscan see a chain of simproc rewrites split into separate visits. - Lake warns "imports X from package mathlib, which is designed for use with the module system; consider adding
module" for every non-module file that imports Mathlib. It is expected here and left alone. - Lake's manifest format is now
1.3.0(path entries gain"copy": false).
Ported package by package by parallel agents, each port adversarially audited (pin check, assertion census, two mandatory mutations, re-execution of every claimed transcript). Assertion counts are preserved or grown; no test was weakened. (Counts are the line-anchored census each package's README now states; the audit follow-up found two historic over-counts, tree-scope 478→476 and dist-lens 346→345, identical on both trees.)
| Package | Lean source changes | Assertions (4.32.2 → 4.34.0) |
|---|---|---|
expr-xray |
none (one docstring) | 456 → 456 |
chart-kit |
none (one module docstring) | 261 → 261 |
tree-scope |
none (byte-identical sources) | 476 → 476 |
hasse-view |
none | 463 → 463 |
simp-lens |
test helper renamed assert → assertThat (gotcha 7); two #guard_msgs pins follow the new unusedSimpArgs hint format |
404 → 404 |
interval-inspector |
Mathlib.Data.Real.Basic → Mathlib.Basic.Real.Basic; set-builder recognizer accepts Set.ofPred as well as the deprecated setOf; click-E2E uses enableInitializersExecution : BaseIO Unit |
845 → 846 |
graph-scope |
tests only: import Lean.Meta.ExprDefEq, Lean.FileMap.ofString, a new section pinning the flipped backward.isDefEq.respectTransparency.types default |
421 → 426 |
dist-lens |
pmf_num's internal simp runs under backward.isDefEq.respectTransparency.types false (the 4.34 default breaks the fraction normalisation) |
345 → 345 |
4.34.0 gotchas worth knowing (each one cost a port iteration):
setOfis now a deprecated alias ofSet.ofPred— a distinct constant, soExpr.isAppOfAritymatchers must accept both.Mathlib.Data.Real.Basicmoved toMathlib.Basic.Real.Basic(the old name is adeprecated_moduleshim that warns).Lean.Elab.enableInitializersExecutionis nowBaseIO Unit(wasIO Unit).String.toFileMapis gone: useLean.FileMap.ofString.backward.isDefEq.respectTransparency.typesdefaults to true; tactics that relied onisDefEqunfolding through type-level definitions (here:pmf_num'ssimpoverPMFcoercions) need the option set tofalselocally.- The
unusedSimpArgslinter hint is now[apply] simptext instead of a strike-through diff, so any#guard_msgspinning it must change. - A do-block line starting with the identifier
assertnow parses as core's newdoAssertionelement (experimental intrinsic verification), so a test helper namedassertfails with "Function expected" plus aWPMonadinstance error. Rename such helpers (assert!is unaffected).
- QED64 (in-browser wasm64 Lean): https://github.com/FawadHa1der/QED64, live at https://qed64.fawadworkaddress.workers.dev
- The wasm64 kernel fork (branch
qed64-wasm64): https://github.com/FawadHa1der/lean4/tree/qed64-wasm64 - ProofWidgets: https://github.com/leanprover-community/ProofWidgets4; Mathlib: https://github.com/leanprover-community/mathlib4
- QED64 showcase docs: README, ARCHITECTURE, BUILD-FROM-SOURCE, DEPLOY-CLOUDFLARE, UPSTREAM-REPORT-QED64, NEXT-STEPS
- Static showcase: showcase/README.md
- License: LICENSE