Fix LF-canonical resource digests for CI

.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

.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
@@ -154,7 +160,13 @@ jobs:
           python-version: "3.11"
           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:
@@ -181,7 +193,13 @@ jobs:
           python-version: "3.11"
           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:
@@ -242,7 +260,13 @@ jobs:
           python-version: "3.11"
           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:
@@ -259,9 +283,16 @@ jobs:
           enable-cache: true
       - 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
 

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.

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,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")
+    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
 

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,

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,
             )

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())

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

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"
 }

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

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