From 1ed669608deefac8da8487cf245e18f17e657048 Mon Sep 17 00:00:00 2001 From: Shaw Date: Tue, 21 Jul 2026 23:24:55 -0400 Subject: [PATCH] ci: harden validation workflows --- .github/workflows/ci.yml | 28 +++++------ .github/workflows/summary.yml | 8 ++++ .../HigherOrderMDSOrderThreeFail.lean | 2 +- .../ProximityGap/LineDecoding.lean | 8 ++-- .../Quarantine/DisproofFoldedRS.lean | 8 ++-- .../CodingTheory/Quarantine/Hypotheses.lean | 14 +++--- .../Quarantine/HypothesesRefutations.lean | 10 ++-- .../CodingTheory/SubspaceDesign/Basic.lean | 20 ++++---- ArkLib/Interaction/Oracle/Core.lean | 2 +- ArkLib/Interaction/Oracle/Spec.lean | 2 +- ArkLib/Interaction/Reduction.lean | 2 +- .../AppendRbrKnowledgePerRoundDischarge.lean | 2 +- .../Security/CacheProvenance.lean | 2 +- .../DuplexSponge/Security/Correspondence.lean | 2 +- .../DuplexSponge/Security/Extraction.lean | 2 +- .../Security/Lemma58CacheProvenance.lean | 2 +- .../Security/Lemma58Correspondence.lean | 2 +- .../Security/Lemma58Extraction.lean | 2 +- .../FiatShamir/HVZKLazyVerifier.lean | 2 +- .../FiatShamirRunCollapseProof.lean | 6 +-- .../RingSwitching/SumcheckPhase.lean | 2 +- ArkLib/ToMathlib/KoalaBearAttackInstance.lean | 2 +- scripts/lintWhitespace.sh | 46 ++++++++----------- 23 files changed, 90 insertions(+), 86 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 39d41ac6ef..cab4e1d377 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -26,21 +26,23 @@ jobs: fetch-depth: 0 - name: Initialize timing paths + env: + BUILD_SOURCE_BRANCH: ${{ github.head_ref || github.ref_name }} run: | - echo "BUILD_TIMING_RESULTS=$RUNNER_TEMP/build-timing.jsonl" >> "$GITHUB_ENV" - echo "BUILD_TIMING_LOG_DIR=$RUNNER_TEMP/build-timing-logs" >> "$GITHUB_ENV" - echo "BUILD_TIMING_ARTIFACT_DIR=$RUNNER_TEMP/build-timing-artifact" >> "$GITHUB_ENV" - echo "BUILD_TIMING_ARTIFACT_NAME=arklib-build-timing-data" >> "$GITHUB_ENV" - echo "BUILD_TIMING_BASELINE_DIR=$RUNNER_TEMP/build-timing-baseline" >> "$GITHUB_ENV" - echo "BUILD_TIMING_REPORT=$RUNNER_TEMP/build-timing.md" >> "$GITHUB_ENV" - echo "BUILD_TIMING_COMMENT=$RUNNER_TEMP/build-timing-comment.md" >> "$GITHUB_ENV" - echo "BUILD_TIMING_SOURCE_SHA=$GITHUB_SHA" >> "$GITHUB_ENV" - echo "BUILD_TIMING_SOURCE_BRANCH=${{ github.head_ref || github.ref_name }}" >> "$GITHUB_ENV" - echo "BUILD_TIMING_BASE_REF=" >> "$GITHUB_ENV" - echo "BUILD_TIMING_MERGE_BASE_SHA=" >> "$GITHUB_ENV" - echo "BUILD_TIMING_TEST_NAME=Validation wrapper" >> "$GITHUB_ENV" - echo "BUILD_TIMING_TEST_COMMAND=./scripts/validate.sh" >> "$GITHUB_ENV" { + echo "BUILD_TIMING_RESULTS=$RUNNER_TEMP/build-timing.jsonl" + echo "BUILD_TIMING_LOG_DIR=$RUNNER_TEMP/build-timing-logs" + echo "BUILD_TIMING_ARTIFACT_DIR=$RUNNER_TEMP/build-timing-artifact" + echo "BUILD_TIMING_ARTIFACT_NAME=arklib-build-timing-data" + echo "BUILD_TIMING_BASELINE_DIR=$RUNNER_TEMP/build-timing-baseline" + echo "BUILD_TIMING_REPORT=$RUNNER_TEMP/build-timing.md" + echo "BUILD_TIMING_COMMENT=$RUNNER_TEMP/build-timing-comment.md" + echo "BUILD_TIMING_SOURCE_SHA=$GITHUB_SHA" + echo "BUILD_TIMING_SOURCE_BRANCH=$BUILD_SOURCE_BRANCH" + echo "BUILD_TIMING_BASE_REF=" + echo "BUILD_TIMING_MERGE_BASE_SHA=" + echo "BUILD_TIMING_TEST_NAME=Validation wrapper" + echo "BUILD_TIMING_TEST_COMMAND=./scripts/validate.sh" echo "BUILD_TIMING_SOURCE_SUBJECT< 2. -------------------------------------------------------------------------------- @[reducible] def ShatteredBundle (U : Finset (Fin n → F)) : Prop := @@ -40,7 +40,7 @@ def hyp_SpinGlass_shattering (e : ℕ) (center : Fin n → F) -------------------------------------------------------------------------------- -- Hypothesis 2: Quantum Information (QLDPC Algebraic Adaptation) -- In QLDPC codes, low-weight stabilizers force errors to be highly degenerate. --- Adapted here: The intersection of the supports of any large bundle of close codewords +-- Adapted here: The intersection of the supports of any large bundle of close codewords -- must be empty to prevent trivial decoding collapse. -------------------------------------------------------------------------------- def hyp_QLDPC_degeneracy (e : ℕ) (center : Fin n → F) @@ -51,7 +51,7 @@ def hyp_QLDPC_degeneracy (e : ℕ) (center : Fin n → F) -------------------------------------------------------------------------------- -- Hypothesis 3: Algebraic Geometry (Hasse-Weil Polynomial Adaptation) -- The number of points on a curve over a finite field is bounded by the Hasse-Weil theorem. --- Translated to RS codes: The number of codewords agreeing on exactly `t` coordinates +-- Translated to RS codes: The number of codewords agreeing on exactly `t` coordinates -- is polynomially bounded. -------------------------------------------------------------------------------- def hyp_HasseWeil_agreement_bound (t : ℕ) (x : Fin n → F) : Prop := @@ -61,9 +61,9 @@ def hyp_HasseWeil_agreement_bound (t : ℕ) (x : Fin n → F) : Prop := -------------------------------------------------------------------------------- -- Hypothesis 4: Additive Combinatorics (Sum-Product Correlation Limits) --- By the sum-product phenomenon over finite fields, highly correlated errors +-- By the sum-product phenomenon over finite fields, highly correlated errors -- cannot grow multiplicatively without escaping the code space. --- If we take the pointwise product of two distinct words in the code, their weight +-- If we take the pointwise product of two distinct words in the code, their weight -- is bounded away from zero. -------------------------------------------------------------------------------- def hyp_SumProduct_escape (u1 u2 : Fin n → F) (h1 : C H_matrix u1) diff --git a/ArkLib/Data/CodingTheory/Quarantine/HypothesesRefutations.lean b/ArkLib/Data/CodingTheory/Quarantine/HypothesesRefutations.lean index dac36d1111..970e045c17 100644 --- a/ArkLib/Data/CodingTheory/Quarantine/HypothesesRefutations.lean +++ b/ArkLib/Data/CodingTheory/Quarantine/HypothesesRefutations.lean @@ -10,8 +10,8 @@ set_option maxRecDepth 4096 /-! # Refutations of Interdisciplinary Candidate Hypotheses -We use the generic GF(3) counterexample (n=4, k=2) to formally refute -the candidate bounds from statistical mechanics, quantum information, +We use the generic GF(3) counterexample (n=4, k=2) to formally refute +the candidate bounds from statistical mechanics, quantum information, and additive combinatorics. -/ @@ -54,7 +54,7 @@ theorem survives_SpinGlass_shattering : -------------------------------------------------------------------------------- -- Refuting Hypothesis 2: Quantum Information (QLDPC Degeneracy) -- The intersection of the supports of any large bundle (>2) is empty. --- But the support of w0 is empty! Wait, if w0 is in U, then the intersection +-- But the support of w0 is empty! Wait, if w0 is in U, then the intersection -- is indeed empty. Let's shift the bundle so 0 is not in it. -------------------------------------------------------------------------------- def v0 : Fin 4 → F := ![1, 1, 2, 0] @@ -72,7 +72,7 @@ theorem refute_QLDPC_degeneracy : -- Refuting Hypothesis 4: Additive Combinatorics (Sum-Product Escape) -- The weight of the pointwise product is bounded by n - 1. -- Let's take w1 * w1 (pointwise). Wait, w1 = [1, 1, 2, 0], w1*w1 = [1, 1, 1, 0]. --- Weight is 3. But n - 1 = 3, so it's bounded. +-- Weight is 3. But n - 1 = 3, so it's bounded. -- What if we use a different code? Actually, we just need the weight of u1 * u2. -- If u1 = [1, 1, 2, 0] and u2 = [2, 1, 0, 1], u1*u2 = [2, 1, 0, 0]. Weight is 2. -- Let's find u1, u2 where weight is n = 4. @@ -86,7 +86,7 @@ def c4 : Fin 3 → F := ![2, 2, 2] -- pointwise: c3 * c4 = [2, 2, 2]. weight is 3. -- So over n=3, weight is 3, which is not <= 2. theorem refute_SumProduct_escape : - ¬ (∀ (u1 u2 : Fin 3 → F), C H_MDS u1 → C H_MDS u2 → u1 ≠ u2 → + ¬ (∀ (u1 u2 : Fin 3 → F), C H_MDS u1 → C H_MDS u2 → u1 ≠ u2 → weight (fun i => u1 i * u2 i) ≤ 2) := by intro h have h_bound : weight (fun i => c3 i * c4 i) ≤ 2 := h c3 c4 (by decide) (by decide) (by decide) diff --git a/ArkLib/Data/CodingTheory/SubspaceDesign/Basic.lean b/ArkLib/Data/CodingTheory/SubspaceDesign/Basic.lean index 1399ed2a46..e77d8dd86a 100644 --- a/ArkLib/Data/CodingTheory/SubspaceDesign/Basic.lean +++ b/ArkLib/Data/CodingTheory/SubspaceDesign/Basic.lean @@ -6,21 +6,21 @@ import Mathlib.Algebra.BigOperators.Group.Finset.Basic # Subspace Designs This file provides the basic definitions and geometric properties of subspace designs. -A collection of subspaces `H` is called an `(s, τ)`-strong subspace design if every -subspace `W` of dimension at most `s` intersects the subspaces in `H` with total -dimension bounded by `τ`. These structures are fundamental in the construction of +A collection of subspaces `H` is called an `(s, τ)`-strong subspace design if every +subspace `W` of dimension at most `s` intersects the subspaces in `H` with total +dimension bounded by `τ`. These structures are fundamental in the construction of list-decodable codes, such as in the Guruswami-Guo 2025 bounds for Reed-Solomon codes. ## Main definitions -* `intersectionMultiplicity`: The sum of dimensions of the intersections of a subspace `W` +* `intersectionMultiplicity`: The sum of dimensions of the intersections of a subspace `W` with a family of subspaces `H`. -* `IsTauSubspaceDesign`: The property that a family `H` forms a `τ`-subspace design +* `IsTauSubspaceDesign`: The property that a family `H` forms a `τ`-subspace design for a given dimension bound `s`. ## Main theorems -* `intersectionMultiplicity_mono`: The intersection multiplicity is monotonically +* `intersectionMultiplicity_mono`: The intersection multiplicity is monotonically increasing with respect to subspace inclusion. -* `intersectionMultiplicity_bound`: A geometric lemma bounding the intersection +* `intersectionMultiplicity_bound`: A geometric lemma bounding the intersection multiplicity of a larger subspace `W` based on a smaller subspace `W'`. -/ @@ -34,9 +34,9 @@ variable {ι : Type*} [Fintype ι] (H : ι → Submodule F V) noncomputable def intersectionMultiplicity (W : Submodule F V) : ℕ := ∑ i, Module.finrank F ↥(H i ⊓ W) -/-- The definition of a strong `τ`-subspace design. -A family `H` of subspaces is an `(s, τ)`-strong subspace design if for every -subspace `W` of dimension at most `s`, its intersection multiplicity with `H` +/-- The definition of a strong `τ`-subspace design. +A family `H` of subspaces is an `(s, τ)`-strong subspace design if for every +subspace `W` of dimension at most `s`, its intersection multiplicity with `H` is bounded by `τ`. -/ def IsTauSubspaceDesign (s τ : ℕ) : Prop := ∀ W : Submodule F V, Module.finrank F W ≤ s → intersectionMultiplicity H W ≤ τ diff --git a/ArkLib/Interaction/Oracle/Core.lean b/ArkLib/Interaction/Oracle/Core.lean index 7c4f7c0dfd..31ba24a0bf 100644 --- a/ArkLib/Interaction/Oracle/Core.lean +++ b/ArkLib/Interaction/Oracle/Core.lean @@ -7,7 +7,7 @@ imports it. Parked to keep the root build green; un-park by migrating to the Ov (see issue #60 for the full diagnosis). -/ /- -/- +/- Copyright (c) 2026 ArkLib Contributors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Quang Dao diff --git a/ArkLib/Interaction/Oracle/Spec.lean b/ArkLib/Interaction/Oracle/Spec.lean index 4b1f99c70f..caf27699f9 100644 --- a/ArkLib/Interaction/Oracle/Spec.lean +++ b/ArkLib/Interaction/Oracle/Spec.lean @@ -7,7 +7,7 @@ imports it. Parked to keep the root build green; un-park by migrating to the Ov (see issue #60 for the full diagnosis). -/ /- -/- +/- Copyright (c) 2026 ArkLib Contributors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Quang Dao diff --git a/ArkLib/Interaction/Reduction.lean b/ArkLib/Interaction/Reduction.lean index 60b0fb1403..4dff88486c 100644 --- a/ArkLib/Interaction/Reduction.lean +++ b/ArkLib/Interaction/Reduction.lean @@ -7,7 +7,7 @@ imports it. Parked to keep the root build green; un-park by migrating to the Ov (see issue #60 for the full diagnosis). -/ /- -/- +/- Copyright (c) 2026 ArkLib Contributors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Quang Dao diff --git a/ArkLib/OracleReduction/Composition/Sequential/AppendRbrKnowledgePerRoundDischarge.lean b/ArkLib/OracleReduction/Composition/Sequential/AppendRbrKnowledgePerRoundDischarge.lean index 01f738376b..ef5547ced4 100644 --- a/ArkLib/OracleReduction/Composition/Sequential/AppendRbrKnowledgePerRoundDischarge.lean +++ b/ArkLib/OracleReduction/Composition/Sequential/AppendRbrKnowledgePerRoundDischarge.lean @@ -103,4 +103,4 @@ theorem appendRbrKnowledgeSoundnessPerRoundResidual_msg_subsingleton [Subsinglet end Verifier -- Axiom audit: must report only `[propext, Classical.choice, Quot.sound]` (no `sorryAx`). -#print axioms Verifier.appendRbrKnowledgeSoundnessPerRoundResidual_msg_subsingleton \ No newline at end of file +#print axioms Verifier.appendRbrKnowledgeSoundnessPerRoundResidual_msg_subsingleton diff --git a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/CacheProvenance.lean b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/CacheProvenance.lean index cbafad6766..a714fedd35 100644 --- a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/CacheProvenance.lean +++ b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/CacheProvenance.lean @@ -273,4 +273,4 @@ end DuplexSpongeFS.EagerLazyDS #print axioms DuplexSpongeFS.EagerLazyDS.cacheFold_pair_mem #print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_hash #print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_pair_fst -#print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_pair_snd \ No newline at end of file +#print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_pair_snd diff --git a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Correspondence.lean b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Correspondence.lean index 403fc2d552..16d00298e8 100644 --- a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Correspondence.lean +++ b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Correspondence.lean @@ -1561,7 +1561,7 @@ theorem anchored_of_E_pinv hbj.symm.trans (heq ▸ hb') have hq : sO = q := Sum.inr.inj (Sum.inr.inj (congrArg Sigma.fst hbeq)) exact Or.inr (by rw [hcapseg, ← hc5, hq]) - + open DuplexSpongeFS.Paper in /-- **E_func arm.** A function violation among dedup entries is impossible in a non-anchored consistent log: the earlier entry caches the forward key, contradicting the freshness of the diff --git a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Extraction.lean b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Extraction.lean index f38d824d3e..679514ddcf 100644 --- a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Extraction.lean +++ b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Extraction.lean @@ -501,4 +501,4 @@ end DuplexSpongeFS.EagerLazyDS #print axioms DuplexSpongeFS.EagerLazyDS.pairRecord_take_of_le #print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_permInv_anchor #print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_hash_anchor -#print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_perm_anchor \ No newline at end of file +#print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_perm_anchor diff --git a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58CacheProvenance.lean b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58CacheProvenance.lean index 834ad490e6..c93c85c14f 100644 --- a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58CacheProvenance.lean +++ b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58CacheProvenance.lean @@ -273,4 +273,4 @@ end DuplexSpongeFS.EagerLazyDS #print axioms DuplexSpongeFS.EagerLazyDS.cacheFold_pair_mem #print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_hash #print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_pair_fst -#print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_pair_snd \ No newline at end of file +#print axioms DuplexSpongeFS.EagerLazyDS.mem_slotList_of_pair_snd diff --git a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58Correspondence.lean b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58Correspondence.lean index 684343a27b..c25b004e80 100644 --- a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58Correspondence.lean +++ b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58Correspondence.lean @@ -1561,7 +1561,7 @@ theorem anchored_of_E_pinv hbj.symm.trans (heq ▸ hb') have hq : sO = q := Sum.inr.inj (Sum.inr.inj (congrArg Sigma.fst hbeq)) exact Or.inr (by rw [hcapseg, ← hc5, hq]) - + open DuplexSpongeFS.Paper in /-- **E_func arm.** A function violation among dedup entries is impossible in a non-anchored consistent log: the earlier entry caches the forward key, contradicting the freshness of the diff --git a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58Extraction.lean b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58Extraction.lean index 16e4d691ce..70c7be67ff 100644 --- a/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58Extraction.lean +++ b/ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58Extraction.lean @@ -501,4 +501,4 @@ end DuplexSpongeFS.EagerLazyDS #print axioms DuplexSpongeFS.EagerLazyDS.pairRecord_take_of_le #print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_permInv_anchor #print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_hash_anchor -#print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_perm_anchor \ No newline at end of file +#print axioms DuplexSpongeFS.EagerLazyDS.anchored_of_perm_anchor diff --git a/ArkLib/OracleReduction/FiatShamir/HVZKLazyVerifier.lean b/ArkLib/OracleReduction/FiatShamir/HVZKLazyVerifier.lean index 8d096f1234..38b4a15265 100644 --- a/ArkLib/OracleReduction/FiatShamir/HVZKLazyVerifier.lean +++ b/ArkLib/OracleReduction/FiatShamir/HVZKLazyVerifier.lean @@ -434,4 +434,4 @@ theorem deriveTranscriptFS_lazy_run_of_runOutput #print axioms runToRoundFS_lazy_cached #print axioms deriveTranscriptFS_lazy_run_of_runOutput -end Reduction \ No newline at end of file +end Reduction diff --git a/ArkLib/OracleReduction/FiatShamirRunCollapseProof.lean b/ArkLib/OracleReduction/FiatShamirRunCollapseProof.lean index c87372a665..79df05de7c 100644 --- a/ArkLib/OracleReduction/FiatShamirRunCollapseProof.lean +++ b/ArkLib/OracleReduction/FiatShamirRunCollapseProof.lean @@ -28,10 +28,10 @@ namespace FiatShamirCollapse open scoped NNReal ProbabilityTheory open ProtocolSpec -/-- **Issue #116 Resolution:** The Fiat-Shamir Collapse Kernel. -This theorem reduces the unproven residual to the State-Separation probability bounds +/-- **Issue #116 Resolution:** The Fiat-Shamir Collapse Kernel. +This theorem reduces the unproven residual to the State-Separation probability bounds over the Random Oracle queries. -/ -theorem fiat_shamir_collapse_breakthrough +theorem fiat_shamir_collapse_breakthrough {ι : Type} {oSpec : OracleSpec ι} {StmtIn : Type} {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {WitIn : Type} {StmtOut : Type} {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {WitOut : Type} diff --git a/ArkLib/ProofSystem/RingSwitching/SumcheckPhase.lean b/ArkLib/ProofSystem/RingSwitching/SumcheckPhase.lean index 2258d1fe31..f4731c97dd 100644 --- a/ArkLib/ProofSystem/RingSwitching/SumcheckPhase.lean +++ b/ArkLib/ProofSystem/RingSwitching/SumcheckPhase.lean @@ -804,7 +804,7 @@ def iteratedSumcheckKStateProp (i : Fin ℓ') (m : Fin (2 + 1)) (localChecks := let explicitVCheck := (∑ b ∈ (boolDomain L ℓ').points i, h_i.val.eval b) = stmt.sumcheck_target - + explicitVCheck ) diff --git a/ArkLib/ToMathlib/KoalaBearAttackInstance.lean b/ArkLib/ToMathlib/KoalaBearAttackInstance.lean index 29c193b2f5..9fd0b8816d 100644 --- a/ArkLib/ToMathlib/KoalaBearAttackInstance.lean +++ b/ArkLib/ToMathlib/KoalaBearAttackInstance.lean @@ -325,4 +325,4 @@ end ArkLib #print axioms ArkLib.KoalaBearAttack.instance_violates #print axioms ArkLib.KoalaBearAttack.fenziSanso_upperBound_attack_concrete_residual_holds #print axioms ArkLib.KoalaBearAttack.fenziSanso_upperBound_attack_residual_holds -#print axioms ArkLib.KoalaBearAttack.attackUpperBound \ No newline at end of file +#print axioms ArkLib.KoalaBearAttack.attackUpperBound diff --git a/scripts/lintWhitespace.sh b/scripts/lintWhitespace.sh index ab2073eab3..fdd995bd22 100755 --- a/scripts/lintWhitespace.sh +++ b/scripts/lintWhitespace.sh @@ -1,43 +1,35 @@ #!/usr/bin/env bash -tmpfile=$(mktemp) -issues_found=0 +set -u validate_spaces () { - find ArkLib -type f -name "*.lean" | while IFS= read -r file; do + local issues_found=0 + while IFS= read -r -d '' file; do # Check for trailing whitespace and print line number if found while IFS=: read -r line_num line; do echo "Trailing whitespace found in $file at line $line_num: $line" - echo 1 > "$tmpfile" + issues_found=1 done < <(grep -n "[[:blank:]]$" "$file") # Check if the last line ends with a new line - if [ "$(tail -c 1 "$file" | od -c | awk 'NR==1 {print $2}')" != "\n" ]; then + if [ -s "$file" ] && [ "$(tail -c 1 "$file" | od -An -t x1 | tr -d '[:space:]')" != "0a" ]; then echo "Last line does not end with a new line in: $file" - echo 1 > "$tmpfile" + issues_found=1 fi - done + done < <(find ArkLib -type f -name '*.lean' -print0) - if [ -f "$tmpfile" ]; then - issues_found=$(<"$tmpfile") + if [ "$issues_found" -ne 0 ]; then + echo "Run \`bash ./scripts/lintWhitespace.sh -i\` to fix whitespace issues." fi - rm -f "$tmpfile" - if [ $issues_found ]; then - echo "Run \`bash ./scripts/lintWhitespace.sh -i\` to fix whitespace issues."; - fi - - exit $issues_found + return "$issues_found" } fix_spaces_inplace() { - for file in $(find ArkLib -type f -name "*.lean") - do - # Remove trailing `\t` and ` `. - sed -i 's/[ \t]*$//' "$file" - # Add trailing '\n' to the file - sed -i -e '$a\' "$file" - done + while IFS= read -r -d '' file; do + # Perl's in-place mode has the same syntax on GNU/Linux and macOS. + perl -0777 -pi -e 's/[ \t]+(?=\n)//g; s/[ \t]+\z//; s/\z/\n/ unless /\n\z/' "$file" + done < <(find ArkLib -type f -name '*.lean' -print0) } is_inplace=0 @@ -47,13 +39,15 @@ while getopts ":i" option; do i) is_inplace=1 ;; *) - echo "Usage: $0 [-i]" + echo "Usage: $0 [-i]" exit 1 ;; esac done -if [ $is_inplace -eq 1 ]; then fix_spaces_inplace; else validate_spaces; fi - - +if [ "$is_inplace" -eq 1 ]; then + fix_spaces_inplace +else + validate_spaces +fi