quangvdao

Shared Lean/Lake Dependency Cache Workflow

This note describes a portable workflow for sharing large Lean/Lake dependency checkouts, especially mathlib, across multiple projects on one machine.

The workflow is local-only. It does not change lakefile.lean, lakefile.toml, or lake-manifest.json. Each project keeps its normal Lake manifest, but selected directories under .lake/packages/ are replaced by symlinks into a central cache keyed by:

quangvdao

---

name: Benchmark Contract Overhaul overview: "Redesign the benchmark-facing API around explicit semantics and phase-level measurement so this repo can publish honest, comparable zkVM benchmark rows. The plan favors truthfulness over convenience: every row must say what was proved, what was measured, and what workload family it belongs to." todos:

• id: pr1-benchmark-vocabulary content: "PR1: define benchmark vocabulary, canonical workload families, and deterministic fixtures." status: pending
• id: pr2-backend-semantics content: "PR2: make each backend declare explicit benchmark semantics and capabilities." status: pending

quangvdao

{"valueParameterDescriptions":[],"slotParameterDescriptions":[],"roleDescriptions":[],"contractType":"O","contractName":"","contractDescription":"","choiceDescriptions":[]}