Benchmark / HighlyAbundant

HighlyAbundant: Mathlib v4.31.0 → v4.35.0

lake build passes after repair. The bump spans 4 Mathlib releases and produced 8 raw build errors in 2 files; an alias rewrite resolves 0 of them.

Project: b-mehta/HighlyAbundant. First build after the bump: 20.6 s, 0 deprecation warnings (0 with a replacement an alias rewrite would apply).

Repairs

Arm	lake build	Rebuilds	Agent min	Labelled changes
Arm A (diagnosing session, not blind)	green	4	20	2 signature change, 2 reproof

The diff

diff --git a/HighlyAbundant/Basic.lean b/HighlyAbundant/Basic.lean

index 89c8dce..495982c 100644

--- a/HighlyAbundant/Basic.lean

+++ b/HighlyAbundant/Basic.lean

@@ -63,7 +63,8 @@ lemma factorization_eq {n p k : ℕ} (h₁ : p ^ k ∣ n) (h₂ : ¬ p ^ (k + 1)

contrapose! h₂

simp [h₂]

suffices k ≤ Nat.factorization n p ∧ ¬ (k + 1 ≤ Nat.factorization n p) by lia

- simp [← hp.pow_dvd_iff_le_factorization hn, *]

+ rw [← hp.pow_dvd_iff_le_factorization hn, ← hp.pow_dvd_iff_le_factorization hn]

+ exact ⟨h₁, h₂⟩

lemma Nat.factorization_finsetLcm {α : Type*} {p : ℕ} {s : Finset α} {f : α → ℕ}

(h : ∀ x ∈ s, f x ≠ 0) :

diff --git a/HighlyAbundant/PrepareLadder.lean b/HighlyAbundant/PrepareLadder.lean

index 3f53eb2..351f70f 100644

--- a/HighlyAbundant/PrepareLadder.lean

+++ b/HighlyAbundant/PrepareLadder.lean

@@ -115,10 +115,10 @@ lemma h_div_K {i : ℕ} (hi : i ∈ Finset.Icc d.lo d.hi) : d.div ∣ d.K i := b

exact dvd_lcmRange_of_le (d.h_divs p hp).ne_zero

(by have := d.h_divs_lo; grind)

have : p ∉ d.muls.map (·.1) := by have := d.h_disjoint; grind

- convert_to p ^ (lcmRange i).factorization p ∣ d.K i

- · rfl

- · rw [d.h_divs_i hi _ hp, Nat.pow_one]

- exact Finset.dvd_prod_of_mem _ (by simp [hpl, this])

+ have hf : (lcmRange i).factorization p = 1 := d.h_divs_i hi _ hp

+ have hK : p ^ (lcmRange i).factorization p ∣ d.K i :=

+ Finset.dvd_prod_of_mem _ (by simp [hpl, this])

+ rwa [hf, Nat.pow_one] at hK

lemma L_eq {i : ℕ} :

lcmRange i = (∏ pki ∈ d.muls.toFinset, pki.1 ^ (lcmRange i).factorization pki.1) * d.K i := by

diff --git a/HighlyAbundant/Prime/PowMod.lean b/HighlyAbundant/Prime/PowMod.lean

index 778c2e1..0808175 100644

--- a/HighlyAbundant/Prime/PowMod.lean

+++ b/HighlyAbundant/Prime/PowMod.lean

@@ -92,15 +92,15 @@ lemma powModTR_aux_eq (n a b c fuel) (hfuel : b < fuel) :

congr! 3

lia

-lemma powModTR_eq (a b n : ℕ) : powModTR a b n = powMod a b n := by

+lemma powModTR_eq (a b n : ℕ) : powModTR a b n = _root_.powMod a b n := by

rw [powModTR, powModTR_aux_eq _ _ _ _ _ (by omega)]

- rw [powModAux, mul_one, powMod, mod_eq_mod, ← Nat.pow_mod]

+ rw [powModAux, mul_one, _root_.powMod, mod_eq_mod, ← Nat.pow_mod]

-lemma powMod_eq_of_powModTR (a b n m : ℕ) (h : (powModTR a b n).beq m) : powMod a b n = m := by

+lemma powMod_eq_of_powModTR (a b n m : ℕ) (h : (powModTR a b n).beq m) : _root_.powMod a b n = m := by

rwa [powModTR_eq, beq_eq] at h

lemma powMod_ne_of_powModTR (a b n m : ℕ) (h : (powModTR a b n).beq m = false) :

- powMod a b n ≠ m := by

+ _root_.powMod a b n ≠ m := by

have := Nat.ne_of_beq_eq_false h

rwa [powModTR_eq] at this

@@ -132,7 +132,7 @@ def prove_pow_mod_tac (g : MVarId) : MetaM Unit := do

| Eq ty lhsE rhsE =>

unless (← whnfR ty).isConstOf ``Nat do throwError "not an equality of naturals"

let some rhs := rhsE.nat? | throwError "rhs is not a numeral"

- let some (aE, bE, nE) := lhsE.app3? ``powMod | throwError "lhs is not a pow-mod"

+ let some (aE, bE, nE) := lhsE.app3? ``_root_.powMod | throwError "lhs is not a pow-mod"

let some a := aE.nat? | throwError "base is not a numeral"

let some b := bE.nat? | throwError "exponent is not a numeral"

let some n := nE.nat? | throwError "modulus is not a numeral"

@@ -141,7 +141,7 @@ def prove_pow_mod_tac (g : MVarId) : MetaM Unit := do

| Ne ty lhsE rhsE =>

unless (← whnfR ty).isConstOf ``Nat do throwError "not an equality of naturals"

let some rhs := rhsE.nat? | throwError "rhs is not a numeral"

- let some (aE, bE, nE) := lhsE.app3? ``powMod | throwError "lhs is not a pow-mod"

+ let some (aE, bE, nE) := lhsE.app3? ``_root_.powMod | throwError "lhs is not a pow-mod"

let some a := aE.nat? | throwError "base is not a numeral"

let some b := bE.nat? | throwError "exponent is not a numeral"

let some n := nE.nat? | throwError "modulus is not a numeral"

diff --git a/HighlyAbundant/Prime/Pratt.lean b/HighlyAbundant/Prime/Pratt.lean

index 0d78240..0358255 100644

--- a/HighlyAbundant/Prime/Pratt.lean

+++ b/HighlyAbundant/Prime/Pratt.lean

@@ -7,11 +7,11 @@ Authors: Bhavik Mehta

import HighlyAbundant.Prime.PowMod

import Mathlib.NumberTheory.LucasPrimality

-def pratt_predicate (p a x : ℕ) : Prop := ∀ q ∈ x.primeFactors, powMod a ((p - 1) / q) p ≠ 1

+def pratt_predicate (p a x : ℕ) : Prop := ∀ q ∈ x.primeFactors, _root_.powMod a ((p - 1) / q) p ≠ 1

@[simp]

lemma pratt_predicate_iff (p a x : ℕ) :

- pratt_predicate p a x ↔ ∀ q ∈ x.primeFactors, powMod a ((p - 1) / q) p ≠ 1 :=

+ pratt_predicate p a x ↔ ∀ q ∈ x.primeFactors, _root_.powMod a ((p - 1) / q) p ≠ 1 :=

Iff.rfl

def pratt_zero (p a : ℕ) : pratt_predicate p a 0 := by simp!

@@ -20,7 +20,7 @@ def pratt_axiom (p a : ℕ) : pratt_predicate p a 1 := by simp!

open Nat

lemma pratt_rule_1 {p a x q : ℕ} (h : pratt_predicate p a x) (hq : q.Prime)

- (h' : powMod a ((p - 1) / q) p ≠ 1) : pratt_predicate p a (q * x) := by

+ (h' : _root_.powMod a ((p - 1) / q) p ≠ 1) : pratt_predicate p a (q * x) := by

rcases eq_or_ne x 0 with rfl | hx

· rwa [mul_zero]

intro r hr

@@ -32,13 +32,13 @@ lemma pratt_rule_1 {p a x q : ℕ} (h : pratt_predicate p a x) (hq : q.Prime)

lemma pratt_rule_1' (q x : ℕ) {p a y : ℕ} (hq : q.Prime)

(hy : q * x = y)

- (h' : powMod a ((p - 1) / q) p ≠ 1) (h : pratt_predicate p a x) : pratt_predicate p a y := by

+ (h' : _root_.powMod a ((p - 1) / q) p ≠ 1) (h : pratt_predicate p a x) : pratt_predicate p a y := by

rw [← hy]

exact pratt_rule_1 h hq h'

lemma pratt_rule_2 (a : ℕ) {p : ℕ} (hp : p ≠ 0) (h : pratt_predicate p a (p - 1))

- (h' : powMod a (p - 1) p = 1) : p.Prime := by

- rw [powMod] at h'

+ (h' : _root_.powMod a (p - 1) p = 1) : p.Prime := by

+ rw [_root_.powMod] at h'

rcases p with rfl | rfl | p

· cases hp rfl

· simp at h'

@@ -52,11 +52,11 @@ lemma pratt_rule_2 (a : ℕ) {p : ℕ} (hp : p ≠ 0) (h : pratt_predicate p a (

· rw [← ZMod.natCast_mod, succ_sub_one, h', Nat.cast_one]

rw [← ZMod.natCast_mod, ←@Nat.cast_one (ZMod (p+2)), ne_eq, ZMod.natCast_eq_natCast_iff,

Nat.ModEq, mod_mod, one_mod]

- simp only [powMod] at h

+ simp only [_root_.powMod] at h

exact h _ hq hq'

lemma pratt_rule_2' (a : ℕ) {p : ℕ} (hp : p ≠ 0)

- (h' : powMod a (p - 1) p = 1)

+ (h' : _root_.powMod a (p - 1) p = 1)

(h : pratt_predicate p a (p - 1)) : p.Prime :=

pratt_rule_2 a hp h h'

Re-run it

source bench/env.sh
python3 bench/lbbench.py setup highlyabundant      # clone b-mehta/HighlyAbundant at v4.31.0, bump the Mathlib pin to v4.35.0
python3 bench/lbbench.py build highlyabundant      # cache get + lake build; writes the raw errors to bench/runs/highlyabundant/v4.35.0/errors.json
git -C bench/work/highlyabundant/proj apply ../../../runs/highlyabundant/v4.35.0/armA.diff   # replay the recorded repair
python3 bench/lbbench.py build highlyabundant --pass replay        # a green replay prints "build rc=0"

Files

Correct this page

Something wrong on this row, or you maintain this project and want it off the benchmark? Correct this row or remove my project.