From ec7853bd40244e586038f699438d61a72bf549c4 Mon Sep 17 00:00:00 2001 From: fraware Date: Sun, 26 Jul 2026 05:55:54 -0700 Subject: [PATCH 1/6] Fix packaged resource digests for LF-canonical CI verification. hashes.json was generated under Windows CRLF, so every Python job failed on Linux with a LeanVerifier.lean digest mismatch; normalize digests and force LF via gitattributes. --- .gitattributes | 12 ++++++++++- docs/developer_guide.md | 2 ++ scripts/regen_resource_hashes.py | 28 ++++++++++++++++++++------ src/leanverifier/resources/access.py | 11 +++++++--- src/leanverifier/resources/hashes.json | 28 +++++++++++++------------- tests/unit/test_resources.py | 16 ++++++++------- 6 files changed, 66 insertions(+), 31 deletions(-) diff --git a/.gitattributes b/.gitattributes index 3516025..6e59984 100644 --- a/.gitattributes +++ b/.gitattributes @@ -1,3 +1,13 @@ - +# Shell scripts always use LF (CI / Unix runners). *.sh text eol=lf +# Digest-checked packaged resources and Lean sources must be LF-canonical. +# hashes.json is generated from these bytes; CRLF checkouts break CI (F-007). +*.lean text eol=lf +*.json text eol=lf +*.toml text eol=lf +lean-toolchain text eol=lf +*.py text eol=lf +*.yml text eol=lf +*.yaml text eol=lf +*.md text eol=lf diff --git a/docs/developer_guide.md b/docs/developer_guide.md index 666008a..8cf0bbf 100644 --- a/docs/developer_guide.md +++ b/docs/developer_guide.md @@ -46,6 +46,8 @@ After editing checkout `schemas/` or Lean sources that ship in the wheel, refres uv run python scripts/regen_resource_hashes.py ``` +Digests are LF-canonical (see `.gitattributes`). Always regenerate on the machine that edited the files; do not hand-edit `hashes.json`. + ## Adding formal content 1. Keep definitions exact over ℚ; no `Array Float`, bang indexing, `getD`, or silent zip truncate. diff --git a/scripts/regen_resource_hashes.py b/scripts/regen_resource_hashes.py index 9ff29de..01d8cee 100644 --- a/scripts/regen_resource_hashes.py +++ b/scripts/regen_resource_hashes.py @@ -7,6 +7,9 @@ Also copies checkout ``schemas/`` mirrors into the packaged tree when present, so docs/checkout copies stay aligned with runtime resources. + +Digests are always computed over LF-normalized bytes so Windows checkouts with +``core.autocrlf`` cannot poison ``hashes.json`` (CI verifies LF blobs). """ from __future__ import annotations @@ -22,8 +25,18 @@ SKIP_NAMES = frozenset({"hashes.json", "__init__.py", "access.py"}) +def _canonical_bytes(data: bytes) -> bytes: + """Normalize newlines to LF for stable cross-platform digests.""" + return data.replace(b"\r\n", b"\n").replace(b"\r", b"\n") + + def _sha(data: bytes) -> str: - return "sha256:" + hashlib.sha256(data).hexdigest() + return "sha256:" + hashlib.sha256(_canonical_bytes(data)).hexdigest() + + +def _write_lf(path: Path, data: bytes) -> None: + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(_canonical_bytes(data)) def sync_schema_mirrors() -> None: @@ -33,7 +46,7 @@ def sync_schema_mirrors() -> None: return dest.mkdir(parents=True, exist_ok=True) for path in src.glob("*.json"): - shutil.copy2(path, dest / path.name) + _write_lf(dest / path.name, path.read_bytes()) def sync_lean_mirrors() -> None: @@ -47,14 +60,17 @@ def sync_lean_mirrors() -> None: ] for src, target in mapping: if src.is_file(): - target.parent.mkdir(parents=True, exist_ok=True) - shutil.copy2(src, target) + _write_lf(target, src.read_bytes()) lean_src = ROOT / "LeanVerifier" lean_dest = dest / "LeanVerifier" if lean_src.is_dir(): if lean_dest.exists(): shutil.rmtree(lean_dest) - shutil.copytree(lean_src, lean_dest) + for path in sorted(lean_src.rglob("*")): + if not path.is_file(): + continue + rel = path.relative_to(lean_src) + _write_lf(lean_dest / rel, path.read_bytes()) def main() -> int: @@ -76,7 +92,7 @@ def main() -> int: continue entries[rel] = _sha(path.read_bytes()) out = RES / "hashes.json" - out.write_text(json.dumps(entries, indent=2, sort_keys=True) + "\n", encoding="utf-8") + out.write_text(json.dumps(entries, indent=2, sort_keys=True) + "\n", encoding="utf-8", newline="\n") print(f"wrote {len(entries)} hashes to {out}") return 0 diff --git a/src/leanverifier/resources/access.py b/src/leanverifier/resources/access.py index 28e0548..b32daf1 100644 --- a/src/leanverifier/resources/access.py +++ b/src/leanverifier/resources/access.py @@ -37,8 +37,13 @@ def _read_text(relative: str) -> str: return _read_bytes(relative).decode("utf-8") +def _canonical_bytes(data: bytes) -> bytes: + """Normalize newlines to LF so digests match regen_resource_hashes.py.""" + return data.replace(b"\r\n", b"\n").replace(b"\r", b"\n") + + def _sha256_digest(data: bytes) -> str: - return "sha256:" + hashlib.sha256(data).hexdigest() + return "sha256:" + hashlib.sha256(_canonical_bytes(data)).hexdigest() def recorded_hashes() -> dict[str, str]: @@ -136,7 +141,7 @@ def materialize_lean_project(*, cache_root: Path | None = None) -> Path: rel_path = relative[len(_LEAN_PREFIX) :] target = tmp / rel_path target.parent.mkdir(parents=True, exist_ok=True) - target.write_bytes(data) + target.write_bytes(_canonical_bytes(data)) (tmp / ".leanverifier-resources-ok").write_text(digest + "\n", encoding="utf-8") if dest.exists(): shutil.rmtree(dest) @@ -162,5 +167,5 @@ def write_axiom_audit_script(dest_dir: Path) -> Path: ) dest_dir.mkdir(parents=True, exist_ok=True) path = dest_dir / "generated_axiom_audit.py" - path.write_bytes(data) + path.write_bytes(_canonical_bytes(data)) return path diff --git a/src/leanverifier/resources/hashes.json b/src/leanverifier/resources/hashes.json index 9511d29..d2de297 100644 --- a/src/leanverifier/resources/hashes.json +++ b/src/leanverifier/resources/hashes.json @@ -1,16 +1,16 @@ { - "lean-project/LeanVerifier.lean": "sha256:5d03208b4c827b7b332f7650a4c775516cf62cf6514089d20c286ad39f729991", - "lean-project/LeanVerifier/Audit/PublicAxioms.lean": "sha256:8bab13188fab52eec615e82122bb9eb9440e8bc9d47abaca1dffb4d1e5027215", - "lean-project/LeanVerifier/Data/Vector.lean": "sha256:94375816fa21ae679c4922df671ead671b2a810416c61b81e7df21e30a01adb8", - "lean-project/LeanVerifier/Model/AffineBinary.lean": "sha256:14cb3e376fac69d7d19400fc97811ae1fe9e3cd56b9c08f952e88ac2028756ef", - "lean-project/LeanVerifier/Property/ClassificationRobustness.lean": "sha256:b43757803c2559cc78263c2a619305c3458ec68f262741a338ca102866d5471b", - "lean-project/LeanVerifier/Property/LinfBall.lean": "sha256:6c247ba08ba692354ca233390b1410aa12f8d32e196c2d3a07c1541e36e14e31", - "lean-project/LeanVerifier/Theorem/AffineMarginRobustness.lean": "sha256:046eb8788ff0782fc1aa4ff9564c758e0c04c83018fadcf1dabbf54d0bcd7cd6", - "lean-project/lake-manifest.json": "sha256:258d6e55d45b4052f04115ce2c8edb9c8dc432f8cd89440eca91518b7d4ce710", - "lean-project/lakefile.toml": "sha256:70539f72fa6a4dfb79cfc281451c063501694a60ec804e687a11ac9af6798e31", - "lean-project/lean-toolchain": "sha256:97402b00d0468725baf4a753bf630ad69d0c588df2a7f5a849429b7926dfe000", - "schemas/model.schema.json": "sha256:92dae8ef78f5a3705af4bed5c0ef38e84f0458724b8191b61629214bd146fdf9", - "schemas/request.schema.json": "sha256:53fbea85ecde62fc324c79cb8b800ab14188ea14850ef2b19849072640ee069e", - "schemas/result.schema.json": "sha256:27fe3122976f564c6d79fcbdcb96bfa4ed949fb7225c55280116b5d7f99c4667", - "scripts/generated_axiom_audit.py": "sha256:81136467cab5d0fac1423560d7ab44fd4ace9c858e4aa80c7e58c52853b499cc" + "lean-project/LeanVerifier.lean": "sha256:19260704c50a178d7c63d85ade76933c5c2fce644cd8ab969aa44e79af9e05b9", + "lean-project/LeanVerifier/Audit/PublicAxioms.lean": "sha256:16d0758e430a0761935872faf1db4b01e518353b24f3ddaa34907fe3cc46ca7d", + "lean-project/LeanVerifier/Data/Vector.lean": "sha256:489ce1f1a1e6f60ee043dc7c5294a42483f6c4d93382517c97bc2ef709f70adc", + "lean-project/LeanVerifier/Model/AffineBinary.lean": "sha256:fa586bdbf76834f61b4efa7554bd5cb4532bf63422982207d699fe6c7053791c", + "lean-project/LeanVerifier/Property/ClassificationRobustness.lean": "sha256:de35b43a35054a2ce6044ebb2e68cddb0050d9dec7c643d53a181cfae6ea4e56", + "lean-project/LeanVerifier/Property/LinfBall.lean": "sha256:9ac5709d562c6fcf03012e7459b31127fe3444a9a60ef32c496fa67a39a1af17", + "lean-project/LeanVerifier/Theorem/AffineMarginRobustness.lean": "sha256:9c1371cf12cfe792c067dfff5bdc0a37a9687806cd49e10a4bc8dbbe03f30aaa", + "lean-project/lake-manifest.json": "sha256:e13fd1d077e8d2ff5370660c8e80b2a7656d29d4550f9fd4acae45bf83519e40", + "lean-project/lakefile.toml": "sha256:8f24e44c8a24f89695bd20066709995ae9b36bc5d3abc9743943b0ee3c6a6789", + "lean-project/lean-toolchain": "sha256:8e3538e0ab5f81a3ee04927d8838c8c674e0e112838b4b3ce87ec218143276af", + "schemas/model.schema.json": "sha256:7e3330fec5db870e090e37b250a29e2b7aaa1ad780a7da486753b1c49f7edd02", + "schemas/request.schema.json": "sha256:4707a3229f4a789ade1cf425bbb8be8cd07bfaf92e6c8c6faeea321b4d8d582d", + "schemas/result.schema.json": "sha256:37edc70bfdfdea83599343f399c911ff4198d8a4cb8819583a5d273484dde1f0", + "scripts/generated_axiom_audit.py": "sha256:681a7876da9d6c858e6511d1e45adb627d9fc9e22381190f304837e8654a7c6a" } diff --git a/tests/unit/test_resources.py b/tests/unit/test_resources.py index 6cf44b6..765e206 100644 --- a/tests/unit/test_resources.py +++ b/tests/unit/test_resources.py @@ -57,6 +57,12 @@ def test_write_axiom_audit_script(tmp_path: Path) -> None: assert "AXIOM AUDIT" in text or "Allowed" in text +def _lf_sha256(data: bytes) -> str: + """Match scripts/regen_resource_hashes.py canonical digests.""" + canonical = data.replace(b"\r\n", b"\n").replace(b"\r", b"\n") + return "sha256:" + hashlib.sha256(canonical).hexdigest() + + def test_checkout_schema_mirrors_match_packaged() -> None: """When running from a source checkout, top-level schemas/ must match package.""" checkout = Path(__file__).resolve().parents[2] @@ -66,8 +72,7 @@ def test_checkout_schema_mirrors_match_packaged() -> None: hashes = recorded_hashes() for name in ("model.schema.json", "request.schema.json", "result.schema.json"): data = (schemas / name).read_bytes() - digest = "sha256:" + hashlib.sha256(data).hexdigest() - assert hashes[f"schemas/{name}"] == digest + assert hashes[f"schemas/{name}"] == _lf_sha256(data) def test_checkout_lean_mirrors_match_packaged() -> None: @@ -82,14 +87,11 @@ def test_checkout_lean_mirrors_match_packaged() -> None: "lean-project/LeanVerifier.lean": checkout / "LeanVerifier.lean", } for key, path in mapping.items(): - digest = "sha256:" + hashlib.sha256(path.read_bytes()).hexdigest() - assert hashes[key] == digest + assert hashes[key] == _lf_sha256(path.read_bytes()) for lean in (checkout / "LeanVerifier").rglob("*.lean"): rel = lean.relative_to(checkout).as_posix() key = f"lean-project/{rel}" - digest = "sha256:" + hashlib.sha256(lean.read_bytes()).hexdigest() - assert hashes[key] == digest - + assert hashes[key] == _lf_sha256(lean.read_bytes()) def test_hashes_json_is_sorted_object() -> None: raw = json.loads( From ac585a86e72fea2907a95380f7fc90086138b5ef Mon Sep 17 00:00:00 2001 From: fraware Date: Sun, 26 Jul 2026 06:12:38 -0700 Subject: [PATCH 2/6] Fix ruff E501 in regen_resource_hashes write_text call. --- scripts/regen_resource_hashes.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/regen_resource_hashes.py b/scripts/regen_resource_hashes.py index 01d8cee..cff7dd7 100644 --- a/scripts/regen_resource_hashes.py +++ b/scripts/regen_resource_hashes.py @@ -92,7 +92,8 @@ def main() -> int: continue entries[rel] = _sha(path.read_bytes()) out = RES / "hashes.json" - out.write_text(json.dumps(entries, indent=2, sort_keys=True) + "\n", encoding="utf-8", newline="\n") + payload = json.dumps(entries, indent=2, sort_keys=True) + "\n" + out.write_text(payload, encoding="utf-8", newline="\n") print(f"wrote {len(entries)} hashes to {out}") return 0 From 194c99f061b4eba5899580df06037138911e65a1 Mon Sep 17 00:00:00 2001 From: fraware Date: Sun, 26 Jul 2026 06:31:24 -0700 Subject: [PATCH 3/6] Warm packaged Lake cache in CI and raise verify timeouts. Verify builds the materialized resource tree, not the checkout; seed .lake/packages after lean-action so Mathlib is not cold-compiled inside the default 600s budget. --- .github/workflows/ci.yml | 17 +++++++ scripts/smoke_wheel.py | 10 +++- scripts/verify_docs.py | 4 +- scripts/warm_packaged_lake.py | 79 +++++++++++++++++++++++++++++ tests/integration/test_cli_flows.py | 2 + tests/mutation/test_mutations.py | 2 + tests/unit/test_resources.py | 1 + 7 files changed, 112 insertions(+), 3 deletions(-) create mode 100644 scripts/warm_packaged_lake.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 11c6148..1c69e6e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -144,6 +144,8 @@ jobs: verify-positive: runs-on: ubuntu-latest needs: [lean-build] + env: + LEANVERIFIER_CACHE: ${{ runner.temp }}/lv-pkg-cache steps: - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -154,6 +156,8 @@ jobs: python-version: "3.11" enable-cache: true - run: uv sync --frozen --all-extras + - name: Warm packaged Lake cache + run: uv run python scripts/warm_packaged_lake.py --seed-from . - name: Positive verify + inspect (markers, not -k alone) run: uv run python -m pytest tests/integration -m "positive and lean" --maxfail=1 @@ -171,6 +175,8 @@ jobs: mutation: runs-on: ubuntu-latest needs: [lean-build] + env: + LEANVERIFIER_CACHE: ${{ runner.temp }}/lv-pkg-cache steps: - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -181,6 +187,8 @@ jobs: python-version: "3.11" enable-cache: true - run: uv sync --frozen --all-extras + - name: Warm packaged Lake cache + run: uv run python scripts/warm_packaged_lake.py --seed-from . - name: Mutation table (verify/audit/inspect) run: uv run python -m pytest tests/mutation -m mutation --maxfail=1 @@ -232,6 +240,8 @@ jobs: docs-commands: runs-on: ubuntu-latest needs: [lean-build] + env: + LEANVERIFIER_CACHE: ${{ runner.temp }}/lv-pkg-cache steps: - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -242,12 +252,17 @@ jobs: python-version: "3.11" enable-cache: true - run: uv sync --frozen --all-extras + - name: Warm packaged Lake cache + run: uv run python scripts/warm_packaged_lake.py --seed-from . - name: Execute README/user-guide CLI commands run: uv run python scripts/verify_docs.py --mode commands wheel-smoke: runs-on: ubuntu-latest needs: [lean-build] + env: + LEANVERIFIER_CACHE: ${{ runner.temp }}/lv-pkg-cache + LEANVERIFIER_VERIFY_TIMEOUT: "1800" steps: - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -259,6 +274,8 @@ jobs: enable-cache: true - name: Sync frozen deps run: uv sync --frozen --all-extras + - name: Warm packaged Lake cache + run: uv run python scripts/warm_packaged_lake.py --seed-from . - name: Build wheel and sdist run: uv build - name: Smoke install from /tmp with verify diff --git a/scripts/smoke_wheel.py b/scripts/smoke_wheel.py index 8618637..0941bf3 100644 --- a/scripts/smoke_wheel.py +++ b/scripts/smoke_wheel.py @@ -110,10 +110,16 @@ def smoke_one( "(install elan/lake or omit --require-verify)." ) - cache = work / "lv-cache" + # Reuse a pre-warmed packaged Lake cache from CI when present. + cache = ( + Path(os.environ["LEANVERIFIER_CACHE"]) + if os.environ.get("LEANVERIFIER_CACHE") + else work / "lv-cache" + ) evidence = work / "evidence" env = dict(env) env["LEANVERIFIER_CACHE"] = str(cache) + verify_timeout = os.environ.get("LEANVERIFIER_VERIFY_TIMEOUT", "1800") _run( [ str(cli), @@ -125,7 +131,7 @@ def smoke_one( "--output", str(evidence), "--timeout", - "600", + verify_timeout, ], cwd=work, env=env, diff --git a/scripts/verify_docs.py b/scripts/verify_docs.py index a3bff15..179e4af 100644 --- a/scripts/verify_docs.py +++ b/scripts/verify_docs.py @@ -208,11 +208,13 @@ def verify_commands(errors: list[str]) -> None: str(request), "--output", str(evidence), + "--timeout", + "1800", ], cwd=ROOT, capture_output=True, text=True, - timeout=900, + timeout=2400, shell=False, check=False, ) diff --git a/scripts/warm_packaged_lake.py b/scripts/warm_packaged_lake.py new file mode 100644 index 0000000..09dcde9 --- /dev/null +++ b/scripts/warm_packaged_lake.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +"""Materialize the packaged Lake project and warm ``lake build`` for CI. + +Verify always builds against the *packaged* Lake tree under ``LEANVERIFIER_CACHE`` +(not the checkout). After ``lean-action`` builds the checkout, seed ``.lake/packages`` +from that tree so Mathlib is not recompiled from scratch within the 600s default +verify budget. +""" + +from __future__ import annotations + +import argparse +import shutil +import subprocess +import sys +from pathlib import Path + +from leanverifier.resources import materialize_lean_project + + +def _seed_packages(dest_root: Path, seed_from: Path) -> None: + src = seed_from / ".lake" / "packages" + if not src.is_dir(): + print(f"no package seed at {src}", flush=True) + return + dest_lake = dest_root / ".lake" + dest = dest_lake / "packages" + dest_lake.mkdir(parents=True, exist_ok=True) + if dest.exists(): + shutil.rmtree(dest) + shutil.copytree(src, dest, symlinks=True) + print(f"seeded packages from {src} -> {dest}", flush=True) + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--seed-from", + type=Path, + default=None, + help="Checkout root with a warm .lake/packages tree (after lean-action)", + ) + parser.add_argument( + "--timeout", + type=int, + default=1800, + help="Seconds allowed for lake build in the materialized tree", + ) + args = parser.parse_args(argv) + + root = materialize_lean_project() + print(f"materialized: {root}", flush=True) + if args.seed_from is not None: + _seed_packages(root, args.seed_from.resolve()) + + if shutil.which("lake") is None: + print("lake not on PATH", file=sys.stderr) + return 1 + + print(f"+ lake build (cwd={root}, timeout={args.timeout})", flush=True) + try: + subprocess.run( + ["lake", "build"], + cwd=root, + check=True, + timeout=args.timeout, + ) + except subprocess.TimeoutExpired: + print("lake build timed out while warming packaged cache", file=sys.stderr) + return 1 + except subprocess.CalledProcessError as exc: + print(f"lake build failed with exit {exc.returncode}", file=sys.stderr) + return exc.returncode or 1 + print("warm packaged lake build ok", flush=True) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tests/integration/test_cli_flows.py b/tests/integration/test_cli_flows.py index c8a302c..63bf2ce 100644 --- a/tests/integration/test_cli_flows.py +++ b/tests/integration/test_cli_flows.py @@ -146,6 +146,8 @@ def test_positive_verify_evidence_bundle(tmp_path: Path) -> None: str(request_path), "--output", str(out), + "--timeout", + "1800", ] ) assert code == EXIT_VERIFIED diff --git a/tests/mutation/test_mutations.py b/tests/mutation/test_mutations.py index 92b6b11..771cbde 100644 --- a/tests/mutation/test_mutations.py +++ b/tests/mutation/test_mutations.py @@ -194,6 +194,8 @@ def test_mutation_evidence_tamper_fails_inspect(tmp_path: Path) -> None: str(request_path), "--output", str(out), + "--timeout", + "1800", ] ) assert code == EXIT_VERIFIED diff --git a/tests/unit/test_resources.py b/tests/unit/test_resources.py index 765e206..1bbd818 100644 --- a/tests/unit/test_resources.py +++ b/tests/unit/test_resources.py @@ -93,6 +93,7 @@ def test_checkout_lean_mirrors_match_packaged() -> None: key = f"lean-project/{rel}" assert hashes[key] == _lf_sha256(lean.read_bytes()) + def test_hashes_json_is_sorted_object() -> None: raw = json.loads( Path(__file__) From 7f9a479700ca7f769657a05b3aa12d1824f7e536 Mon Sep 17 00:00:00 2001 From: fraware Date: Sun, 26 Jul 2026 06:33:47 -0700 Subject: [PATCH 4/6] Retrigger CI after empty workflow run. From 465c3a6429cb95cbe50d747c66a2bf494fec3b7f Mon Sep 17 00:00:00 2001 From: fraware Date: Sun, 26 Jul 2026 06:35:08 -0700 Subject: [PATCH 5/6] Use step-level LEANVERIFIER_CACHE paths for CI Lake warm-up. --- .github/workflows/ci.yml | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1c69e6e..a6a37e4 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -144,8 +144,6 @@ jobs: verify-positive: runs-on: ubuntu-latest needs: [lean-build] - env: - LEANVERIFIER_CACHE: ${{ runner.temp }}/lv-pkg-cache steps: - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -157,8 +155,12 @@ jobs: enable-cache: true - run: uv sync --frozen --all-extras - name: Warm packaged Lake cache + env: + LEANVERIFIER_CACHE: /tmp/lv-pkg-cache run: uv run python scripts/warm_packaged_lake.py --seed-from . - name: Positive verify + inspect (markers, not -k alone) + env: + LEANVERIFIER_CACHE: /tmp/lv-pkg-cache run: uv run python -m pytest tests/integration -m "positive and lean" --maxfail=1 integration-negative: @@ -175,8 +177,6 @@ jobs: mutation: runs-on: ubuntu-latest needs: [lean-build] - env: - LEANVERIFIER_CACHE: ${{ runner.temp }}/lv-pkg-cache steps: - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -188,8 +188,12 @@ jobs: enable-cache: true - run: uv sync --frozen --all-extras - name: Warm packaged Lake cache + env: + LEANVERIFIER_CACHE: /tmp/lv-pkg-cache run: uv run python scripts/warm_packaged_lake.py --seed-from . - name: Mutation table (verify/audit/inspect) + env: + LEANVERIFIER_CACHE: /tmp/lv-pkg-cache run: uv run python -m pytest tests/mutation -m mutation --maxfail=1 security-tests: @@ -240,8 +244,6 @@ jobs: docs-commands: runs-on: ubuntu-latest needs: [lean-build] - env: - LEANVERIFIER_CACHE: ${{ runner.temp }}/lv-pkg-cache steps: - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -253,16 +255,17 @@ jobs: enable-cache: true - run: uv sync --frozen --all-extras - name: Warm packaged Lake cache + env: + LEANVERIFIER_CACHE: /tmp/lv-pkg-cache run: uv run python scripts/warm_packaged_lake.py --seed-from . - name: Execute README/user-guide CLI commands + env: + LEANVERIFIER_CACHE: /tmp/lv-pkg-cache run: uv run python scripts/verify_docs.py --mode commands wheel-smoke: runs-on: ubuntu-latest needs: [lean-build] - env: - LEANVERIFIER_CACHE: ${{ runner.temp }}/lv-pkg-cache - LEANVERIFIER_VERIFY_TIMEOUT: "1800" steps: - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -275,10 +278,15 @@ jobs: - name: Sync frozen deps run: uv sync --frozen --all-extras - name: Warm packaged Lake cache + env: + LEANVERIFIER_CACHE: /tmp/lv-pkg-cache run: uv run python scripts/warm_packaged_lake.py --seed-from . - name: Build wheel and sdist run: uv build - name: Smoke install from /tmp with verify + env: + LEANVERIFIER_CACHE: /tmp/lv-pkg-cache + LEANVERIFIER_VERIFY_TIMEOUT: "1800" run: | uv run python scripts/smoke_wheel.py --dist dist --artifact both --require-verify From c55cf214ec5d14a82b84c8e58e53fe070cecad64 Mon Sep 17 00:00:00 2001 From: fraware Date: Sun, 26 Jul 2026 06:51:21 -0700 Subject: [PATCH 6/6] Count security and non-lean integration tests toward the unit coverage gate. --- .github/workflows/ci.yml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a6a37e4..2553903 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -117,7 +117,13 @@ jobs: - name: Mypy run: uv run mypy src/leanverifier - name: Pytest unit + coverage - run: uv run python -m pytest tests/unit tests/schema --cov=src/leanverifier --cov-fail-under=70 + # Include security + non-lean integration so CLI/evidence paths count toward + # the gate; lake-backed verify stays in dedicated jobs. + run: > + uv run python -m pytest + tests/unit tests/schema tests/security tests/integration + -m "not lean" + --cov=src/leanverifier --cov-fail-under=70 schema-negative: runs-on: ubuntu-latest