feat: define VCVio’s public boundary over PolyFun - #511

Draft

dtumad wants to merge 8 commits into

mainfrom

refactor/polyfun-module-boundary

Commits on Aug 5, 2026

chore(deps): update PolyFun module-system baseline
dtumad
committed
bb61d6a
refactor: migrate active Lean libraries to module scopes
dtumad
committed
f894fc2
ci: enforce Lean module scopes
dtumad
committed
b47f270
chore(deps): update Lean stack to v4.32.2
dtumad
committed
d952a89
ci: avoid ripgrep dependency in module checks
dtumad
committed
4ef653f
ci: drop one-time module cutover check
dtumad
committed
207e4a1
refactor: keep migration proof helpers private
dtumad
committed
9337b8e

Commits on Aug 8, 2026

refactor: define the PolyFun module boundary
dtumad
committed
b17d690