Repository navigation
PVL EV-5a orphan group ProvableContracts.Theorems: 55 module(s) outside the root import cone #4124
Closed as not planned
Description
Part of #4122 (PVL-001 EV-5a) and drained by EV-5c. 55 Lean module(s) under ProvableContracts.Theorems are ORPHANS: they are not in the transitive import cone of the root crates/aprender-contracts-staging/lean/ProvableContracts.lean. So lake build of the default target never compiles them, and no proof in them is checked.
They are allowlisted by EV-5a's check-orphans.sh against this issue. EV-5c's rule: bring each one into the root cone, or, if it will not compile, keep it allowlisted with an issue. Never delete one.
ProvableContracts.Theorems.AdamW.Adam_Moments
ProvableContracts.Theorems.AdamW.Adam_Variance
ProvableContracts.Theorems.AdamW.Analytic
ProvableContracts.Theorems.AdamW.Bias_Correction
ProvableContracts.Theorems.AdamW.Weight_Update
ProvableContracts.Theorems.AprCode.HarnessIrRoundtrip
ProvableContracts.Theorems.BLAS.Trmm
ProvableContracts.Theorems.BLAS.Trsm
ProvableContracts.Theorems.CrossEntropy.CoreSoftmaxInvariants
ProvableContracts.Theorems.DPO
ProvableContracts.Theorems.F16.Conversion
ProvableContracts.Theorems.FFT.Bluestein
ProvableContracts.Theorems.FFT.Fft2d
ProvableContracts.Theorems.FFT.Fft3d
ProvableContracts.Theorems.FFT.FftBatched
ProvableContracts.Theorems.Fusion.Correctness
ProvableContracts.Theorems.GPU.DimensionIndependence
ProvableContracts.Theorems.GatedDeltaNet.Recurrence
ProvableContracts.Theorems.GgufExportSymmetry.Roundtrip
ProvableContracts.Theorems.Image.Canny
ProvableContracts.Theorems.Image.ConnectedComponents
ProvableContracts.Theorems.Image.Conv2d
ProvableContracts.Theorems.Image.Histogram
ProvableContracts.Theorems.Image.HsvRoundtrip
ProvableContracts.Theorems.Image.Morphology
ProvableContracts.Theorems.Image.Resize
ProvableContracts.Theorems.Image.RgbToGray
ProvableContracts.Theorems.Image.Sobel
ProvableContracts.Theorems.LoRA.Dare_Unbiased
ProvableContracts.Theorems.LoRA.Lora_Shape
ProvableContracts.Theorems.LoRA.Shape_Preservation
ProvableContracts.Theorems.LoRA.Task_Vector
ProvableContracts.Theorems.Lora.MergeForwardEquiv
ProvableContracts.Theorems.MatMul.CooperativeTiling
ProvableContracts.Theorems.MatMul.Distributivity
ProvableContracts.Theorems.MatMul.MatVecLinearity
ProvableContracts.Theorems.MatMul.Shape
ProvableContracts.Theorems.MatMul.TransposeMul
ProvableContracts.Theorems.Metrics.Regression
ProvableContracts.Theorems.Metrics.RegressionAnalytic
ProvableContracts.Theorems.Quantization.NF4Dequant
ProvableContracts.Theorems.RMSNorm.NormalizedRMS
ProvableContracts.Theorems.Rand.Philox
ProvableContracts.Theorems.Rand.Threefry
ProvableContracts.Theorems.Rope.Rope
ProvableContracts.Theorems.Sigmoid.SiluAsymptotic
ProvableContracts.Theorems.Sigmoid.SiluSign
ProvableContracts.Theorems.Sparse.BsrSpmv
ProvableContracts.Theorems.Sparse.SellSpmv
ProvableContracts.Theorems.Sparse.Spgemm
ProvableContracts.Theorems.Sparse.Spmm
ProvableContracts.Theorems.Tensor.Einsum
ProvableContracts.Theorems.TensorLayout.IndexAlgebra
ProvableContracts.Theorems.TensorTranspose.Roundtrip
ProvableContracts.Theorems.Tokenizer
Measured on main @ 49fe19c by aprender-6c [8b6b78].
Collapsed rows (APR-EPIC-001 rule 20)
One issue per PR: tick a line when its PR merges; the PR closing the last line says Closes #4124, the others Refs #4124 row <id>.
- PVL EV-5a orphan group ProvableContracts.Defs: 4 module(s) outside the root import cone #4125: PVL EV-5a orphan group ProvableContracts.Defs: 4 module(s) outside the root import cone (PVL EV-5a orphan group ProvableContracts.Defs: 4 module(s) outside the root import cone #4125)
Activity
noahgift commentedon Sep 25, 2026
Measured at ae1887d (fold/b3-onto-main, carried by #4431): all 55 modules in this group are in the root import cone, and they compile.
check-orphans.sh:modules=162 in-cone=162 orphans=0 allowlisted=0, rc 0.--self-testPASS.orphan-allowlist.yamlis[], drained by EV-6c (PVL-001 EV-6c — 59 Lean modules (85 bound roots) are unreachable from ProvableContracts.lean: never built, never leancheck'd #4244).build.sh(lambda, Mathlib pinned by the manifest):lake build rc=0, 0 warning(s) in ProvableContracts/, gate rc 0.Nothing stays allowlisted and none were deleted. Closing is for the quorum.
noahgift commentedon Oct 12, 2026
park proposal: folded-into:#4347, the orphan allowlist on main (
lean/orphan-allowlist.yaml) now assigns all 55 of its entries to #4347 (open, 0.71.0) and no longer cites #4124, so the remaining work is tracked there.