Proof for perfect_completeness_k (#27) #243
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Lean Action CI | |
| on: | |
| push: | |
| pull_request: | |
| workflow_dispatch: | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Reject proof-term `sorry` and user-declared `axiom` in the umbrella | |
| run: | | |
| python3 - <<'PY' | |
| import pathlib, re, sys | |
| # Strip Lean `/- ... -/` block comments (non-greedy, DOTALL) and `--` line comments, | |
| # then scan for forbidden tokens. Comment-aware because docstrings and header | |
| # comments legitimately mention the words "sorry" / "axiom". | |
| BLOCK = re.compile(r"/-.*?-/", re.DOTALL) | |
| LINE = re.compile(r"--[^\n]*") | |
| SORRY = re.compile(r"(?<![A-Za-z0-9_])sorry(?![A-Za-z0-9_])") | |
| # `axiom Foo : ...` (a new user-declared axiom). Allows `axiomName`, | |
| # `axioms`, and references inside `#print axioms ...` (which is not a | |
| # declaration but a query). | |
| AXIOM = re.compile(r"^\s*axiom\s+[A-Za-z_]", re.MULTILINE) | |
| roots = [pathlib.Path("LinearCodes"), | |
| pathlib.Path("Upstream"), | |
| pathlib.Path("SumcheckProtocol"), | |
| pathlib.Path("InteractiveProtocol")] | |
| sorry_offenders, axiom_offenders = [], [] | |
| for root in roots: | |
| if not root.exists(): | |
| continue | |
| for path in root.rglob("*.lean"): | |
| src = path.read_text(encoding="utf-8") | |
| stripped = LINE.sub("", BLOCK.sub("", src)) | |
| if SORRY.search(stripped): | |
| sorry_offenders.append(str(path)) | |
| if AXIOM.search(stripped): | |
| axiom_offenders.append(str(path)) | |
| failed = False | |
| if sorry_offenders: | |
| print("::error::Proof-term `sorry` found in:") | |
| for f in sorry_offenders: | |
| print(f" - {f}") | |
| failed = True | |
| if axiom_offenders: | |
| print("::error::User-declared `axiom` found in:") | |
| for f in axiom_offenders: | |
| print(f" - {f}") | |
| failed = True | |
| if failed: | |
| sys.exit(1) | |
| print("Clean: no proof-term `sorry`, no user-declared `axiom` in LinearCodes/, " | |
| "Upstream/, SumcheckProtocol/, or InteractiveProtocol/.") | |
| PY | |
| - uses: leanprover/lean-action@v1 | |
| - name: Encoder smoke check (native_decide on a fixed vector) | |
| run: | | |
| # The Reed-Solomon encoder is exercised end-to-end at build time | |
| # via `native_decide` examples in `LinearCodes/Examples/RSSmokeTest.lean` | |
| # (encoded as `lean_lib LinearCodes.Examples` in lakefile.lean). If the | |
| # encoder's output drifts from the hand-computed expected vectors — | |
| # e.g. `reedSolomonEncode cfg #[3, 1] = #[3, 4, 5, 6]` over ZMod 17 — | |
| # the `lean-action` step above will have failed before reaching here. | |
| # This step just records the assertion in the workflow log for audit. | |
| echo "Encoder smoke tests pinned in LinearCodes/Examples/RSSmokeTest.lean." | |
| echo " - reedSolomonEncode cfg82 .proven 3 0 17 = clipped to 1 (toy field)" | |
| echo " - reedSolomonEncode cfg82 .proven 3 0 1009 = 256/1009 (non-vacuous)" |