From f642a64c76df8ba9cb53dba3b919425a0c2aeaf1 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 17 Feb 2026 00:49:34 +1100 Subject: [PATCH 01/17] chore: bump toolchain to v4.28.0 (#309) --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 512ad905c..c04efe55c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7", + "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0-rc1", + "inputRev": "v4.28.0", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index c73bf88b1..d80ac4a0d 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,7 @@ platformIndependent = true [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.28.0-rc1" +rev = "v4.28.0" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index 4bafde205..4c685fa08 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.28.0-rc1 +leanprover/lean4:v4.28.0 From eb165126bfb2988738792c9ae37e09d58e2fec83 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Wed, 18 Feb 2026 07:31:11 +1100 Subject: [PATCH 02/17] chore: bump toolchain to v4.29.0-rc1 (#310) Co-authored-by: Jannis Limperg Co-authored-by: Kyle Miller Co-authored-by: Sebastian Ullrich Co-authored-by: Jannis Limperg Co-authored-by: Anne C.A. Baanen Co-authored-by: Marc Huisinga Co-authored-by: Markus Himmel Co-authored-by: Joachim Breitner Co-authored-by: Claude Opus 4.5 Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> --- Aesop/Forward/RuleInfo.lean | 4 +++- Aesop/Frontend/Command.lean | 4 ++-- Aesop/Frontend/Extension.lean | 2 +- AesopTest/205.lean | 12 ++++++------ AesopTest/List.lean | 2 -- AesopTest/RulePattern.lean | 18 ++++++++++-------- AesopTest/SeqCalcProver.lean | 2 +- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 10 files changed, 27 insertions(+), 25 deletions(-) diff --git a/Aesop/Forward/RuleInfo.lean b/Aesop/Forward/RuleInfo.lean index ebefe01f5..cf31c14df 100644 --- a/Aesop/Forward/RuleInfo.lean +++ b/Aesop/Forward/RuleInfo.lean @@ -162,7 +162,9 @@ where compareOn (·.deps.size) x y |>.then (compareOn (·.premiseIndex) x y) ⟩ - let firstSlot := slots.maxI + -- Needed after https://github.com/leanprover/lean4/pull/11936 + have : Max Slot := ⟨fun a b => if compare a b == .lt then b else a⟩ + let firstSlot := slots.rangeMaxI let mut unseen := slots |>.erase firstSlot let firstSlotForwardDeps : Std.HashSet PremiseIndex := unseen.foldl (init := ∅) λ deps s => deps.insertMany s.deps diff --git a/Aesop/Frontend/Command.lean b/Aesop/Frontend/Command.lean index 761eebba7..e7fe401d2 100644 --- a/Aesop/Frontend/Command.lean +++ b/Aesop/Frontend/Command.lean @@ -43,7 +43,7 @@ elab (name := addRules) e.buildAdditionalGlobalRules none for (rule, rsNames) in rules do for rsName in rsNames do - addGlobalRule rsName rule attrKind (checkNotExists := true) + liftCoreM $ addGlobalRule rsName rule attrKind (checkNotExists := true) initialize Batteries.Linter.UnreachableTactic.addIgnoreTacticKind ``addRules @@ -56,7 +56,7 @@ elab (name := eraseRules) e.toGlobalRuleFilters for fs in filters do for (rsFilter, rFilter) in fs do - eraseGlobalRules rsFilter rFilter (checkExists := true) + liftCoreM $ eraseGlobalRules rsFilter rFilter (checkExists := true) syntax (name := showRules) withPosition("#aesop_rules" (colGt ppSpace ident)*) : command diff --git a/Aesop/Frontend/Extension.lean b/Aesop/Frontend/Extension.lean index a64758527..aea1ee04a 100644 --- a/Aesop/Frontend/Extension.lean +++ b/Aesop/Frontend/Extension.lean @@ -40,7 +40,7 @@ def declareRuleSetUnchecked (rsName : RuleSetName) (isDefault : Bool) : def isRuleSetDeclared (rsName : RuleSetName) : IO Bool := return (← getDeclaredRuleSets).contains rsName -variable [Monad m] [MonadError m] [MonadLiftT IO m] +variable [Monad m] [MonadError m] [MonadLiftT IO m] [MonadLiftT CoreM m] [MonadLiftT (ST IO.RealWorld) m] [MonadEnv m] [MonadResolveName m] def checkRuleSetNotDeclared (rsName : RuleSetName) : m Unit := do diff --git a/AesopTest/205.lean b/AesopTest/205.lean index ee93daa92..3bfc06d7a 100644 --- a/AesopTest/205.lean +++ b/AesopTest/205.lean @@ -16,12 +16,12 @@ axiom R {α} : α → α → Prop /-- info: Try this: - [apply] have fwd : R b y := sym h₃ - have fwd_1 : R a x := sym h₂ - have fwd_2 : R b b := tran fwd h₃ - have fwd_3 : R y y := tran h₃ fwd - have fwd_4 : R a a := tran fwd_1 h₂ - have fwd_5 : R x x := tran h₂ fwd_1 + [apply] have fwd : R a x := sym h₂ + have fwd_1 : R b y := sym h₃ + have fwd_2 : R a a := tran fwd h₂ + have fwd_3 : R y y := tran h₃ fwd_1 + have fwd_4 : R b b := tran fwd_1 h₃ + have fwd_5 : R x x := tran h₂ fwd sorry --- warning: declaration uses `sorry` diff --git a/AesopTest/List.lean b/AesopTest/List.lean index 4cffb4360..5963d9032 100644 --- a/AesopTest/List.lean +++ b/AesopTest/List.lean @@ -807,8 +807,6 @@ attribute [-simp] reverseAux_eq theorem reverse_cons' (a : α) (l : List α) : reverse (a::l) = concat (reverse l) a := by aesop -@[simp] theorem reverse_singleton (a : α) : reverse [a] = [a] := rfl - -- TODO: after nightly-2024-08-27, `aesop` can not prove this anymore! attribute [-simp] reverse_append in @[simp] theorem X.reverse_append (s t : List α) : reverse (s ++ t) = (reverse t) ++ (reverse s) := diff --git a/AesopTest/RulePattern.lean b/AesopTest/RulePattern.lean index c8a4928bd..c2d5ea7fb 100644 --- a/AesopTest/RulePattern.lean +++ b/AesopTest/RulePattern.lean @@ -18,14 +18,16 @@ macro "falso" : tactic => `(tactic| exact falso) @[aesop norm -100 forward (pattern := (↑n : Int))] axiom nat_pos (n : Nat) : 0 ≤ (↑n : Int) -example (m n : Nat) : (↑m : Int) < 0 ∧ (↑n : Int) > 0 := by - set_option aesop.check.script.steps false in -- TODO lean4#4315 - set_option aesop.check.script false in - aesop (config := { enableSimp := false, warnOnNonterminal := false }) - all_goals - guard_hyp fwd : 0 ≤ (m : Int) - guard_hyp fwd_1 : 0 ≤ (n : Int) - falso +-- This test is non-deterministic and caused havoc in CI. +-- Please do not restore without first find a reproducer for the non-determinism, and an identified fix. +-- example (m n : Nat) : (↑m : Int) < 0 ∧ (↑n : Int) > 0 := by +-- set_option aesop.check.script.steps false in -- TODO lean4#4315 +-- set_option aesop.check.script false in +-- aesop (config := { enableSimp := false, warnOnNonterminal := false }) +-- all_goals +-- guard_hyp fwd : 0 ≤ (m : Int) +-- guard_hyp fwd_1 : 0 ≤ (n : Int) +-- falso @[aesop safe forward (pattern := min x y)] axiom foo : ∀ {x y : Nat} (_ : 0 < x) (_ : 0 < y), 0 < min x y diff --git a/AesopTest/SeqCalcProver.lean b/AesopTest/SeqCalcProver.lean index b91f6be21..b22ba5bd4 100644 --- a/AesopTest/SeqCalcProver.lean +++ b/AesopTest/SeqCalcProver.lean @@ -246,7 +246,7 @@ def Cal (l r : List Φ) : (Γ Δ : List (Form Φ)) → Prop | Γ, φ ⇒ ψ :: Δ => Cal l r (φ :: Γ) (ψ :: Δ) termination_by Γ Δ => sum (Γ.map sizeOf) + sum (Δ.map sizeOf) -instance Cal.instDecidable [DecidableEq Φ] (l r : List Φ) (Γ Δ : List (Form Φ)) +def Cal.instDecidable [DecidableEq Φ] (l r : List Φ) (Γ Δ : List (Form Φ)) : Decidable (Cal l r Γ Δ) := by match Γ, Δ with | [], [] => unfold Cal; apply Common.instDecidable l r diff --git a/lake-manifest.json b/lake-manifest.json index c04efe55c..0462cea41 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", + "rev": "965500ff9171556698ec2714b936739d5da438c2", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0", + "inputRev": "v4.29.0-rc1", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index d80ac4a0d..ebebabfaa 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,7 @@ platformIndependent = true [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.28.0" +rev = "v4.29.0-rc1" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index 4c685fa08..c7ad81a70 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.28.0 +leanprover/lean4:v4.29.0-rc1 From de5caa559acfd0a1577b3bc49c33887a91c4792e Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 24 Feb 2026 16:04:09 +1100 Subject: [PATCH 03/17] chore: bump toolchain to v4.29.0-rc2 (#312) --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 0462cea41..10497be25 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "965500ff9171556698ec2714b936739d5da438c2", + "rev": "07be181c4f3c157e385eaa0259ac248bc3eb3626", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0-rc1", + "inputRev": "v4.29.0-rc2", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index ebebabfaa..95adc8968 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,7 @@ platformIndependent = true [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.29.0-rc1" +rev = "v4.29.0-rc2" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index c7ad81a70..283f574d1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0-rc1 +leanprover/lean4:v4.29.0-rc2 From 6f8999a4e31701d2c905262d3788a8c0d21b3f1f Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Mon, 2 Mar 2026 08:28:44 +1100 Subject: [PATCH 04/17] chore: bump toolchain to v4.29.0-rc3 (#314) --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 10497be25..0dc89ed00 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "07be181c4f3c157e385eaa0259ac248bc3eb3626", + "rev": "ed250d06b33e67aa5dc5f2cc349a5a35e8b6b390", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0-rc2", + "inputRev": "v4.29.0-rc3", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index 95adc8968..226a16ef1 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,7 @@ platformIndependent = true [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.29.0-rc2" +rev = "v4.29.0-rc3" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index 283f574d1..f08aa7fb5 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0-rc2 +leanprover/lean4:v4.29.0-rc3 From 6d5ec850924e710ea67881e3ca9d1e920c929dbe Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Wed, 4 Mar 2026 22:42:42 +1100 Subject: [PATCH 05/17] chore: bump toolchain to v4.29.0-rc4 (#315) --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 0dc89ed00..c01dcb98d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ed250d06b33e67aa5dc5f2cc349a5a35e8b6b390", + "rev": "ac3fb7297326c5429ce2844712fb54ba9dd20198", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0-rc3", + "inputRev": "v4.29.0-rc4", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index 226a16ef1..74255f9f5 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,7 @@ platformIndependent = true [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.29.0-rc3" +rev = "v4.29.0-rc4" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index f08aa7fb5..5e4f37067 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0-rc3 +leanprover/lean4:v4.29.0-rc4 From c3361708f266893de5d1769192b60d4b1831f2bb Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 10 Mar 2026 11:46:35 +1100 Subject: [PATCH 06/17] chore: bump toolchain to v4.29.0-rc6 (#316) --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index c01dcb98d..f95b3b16c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ac3fb7297326c5429ce2844712fb54ba9dd20198", + "rev": "bd58e3506632241b59e406902d5e42b73cdeccce", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0-rc4", + "inputRev": "v4.29.0-rc6", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index 74255f9f5..7861ed7d0 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,7 @@ platformIndependent = true [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.29.0-rc4" +rev = "v4.29.0-rc6" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index 5e4f37067..87b20aaf8 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0-rc4 +leanprover/lean4:v4.29.0-rc6 From a90cba993b699ba1a83f96644ed074c1bea86617 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Mon, 23 Mar 2026 17:37:18 +1100 Subject: [PATCH 07/17] chore: bump toolchain to v4.29.0-rc7 (#319) Co-authored-by: Claude Opus 4.6 (1M context) --- Aesop/ElabM.lean | 2 +- Aesop/Forward/State.lean | 6 +++--- Aesop/Saturate.lean | 10 +++++----- Aesop/Script/Step.lean | 2 +- Aesop/Script/StructureDynamic.lean | 6 +++--- Aesop/Script/UScriptToSScript.lean | 2 +- Aesop/Search/SearchM.lean | 8 ++++---- Aesop/Tracing.lean | 8 ++++---- Aesop/Tree/ExtractScript.lean | 4 ++-- Aesop/Tree/TreeM.lean | 2 +- Aesop/Util/EqualUpToIds.lean | 2 +- AesopTest/EqualUpToIds.lean | 2 ++ lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 15 files changed, 32 insertions(+), 30 deletions(-) diff --git a/Aesop/ElabM.lean b/Aesop/ElabM.lean index 48f9fcc3f..a139c4cb2 100644 --- a/Aesop/ElabM.lean +++ b/Aesop/ElabM.lean @@ -47,7 +47,7 @@ abbrev ElabM := ReaderT ElabM.Context $ TermElabM -- Generate specialized pure/bind implementations so we don't need to optimise -- them on the fly at each use site. instance : Monad ElabM := - { inferInstanceAs (Monad ElabM) with } + { (inferInstance : Monad ElabM) with } protected def ElabM.run (ctx : Context) (x : ElabM α) : TermElabM α := do ReaderT.run x ctx diff --git a/Aesop/Forward/State.lean b/Aesop/Forward/State.lean index 96f077fb1..e6543c2ac 100644 --- a/Aesop/Forward/State.lean +++ b/Aesop/Forward/State.lean @@ -11,7 +11,7 @@ public import Aesop.EMap public section open Lean Lean.Meta -open ExceptToEmoji (toEmoji) + set_option linter.missingDocs true @@ -698,7 +698,7 @@ def eraseHyp (h : FVarId) (pi : PremiseIndex) (rs : RuleState) : RuleState := /-- Add any enqueued hyps to the rule state, potentially generating new complete matches in the process. -/ def update (goal : MVarId) (rs : RuleState) : BaseM (RuleState × Array ForwardRuleMatch) := - withAesopTraceNode .forward (fun r => return m!"{exceptEmoji r} update rule state {rs.rule.name}") do + withAesopTraceNode .forward (fun _ => return m!"update rule state {rs.rule.name}") do if ! rs.clusterStates.all (·.haveHypForEachSlot) then aesop_trace[forward] "skipping update since some cluster states cannot yet have complete matches" return (rs, #[]) @@ -895,7 +895,7 @@ def update (goal : MVarId) (fs : ForwardState) (phase? : Option PhaseName) : match phase? with | none => "all phases" | some phase => s!"{phase} phase" - withAesopTraceNode .forward (fun r => return m!"{exceptEmoji r} update forward state for {phaseStr}") do + withAesopTraceNode .forward (fun _ => return m!"update forward state for {phaseStr}") do let toUpdate : Array RuleName := match phase? with | none => fs.ruleStates.foldl (init := #[]) fun toUpdate rule _ => toUpdate.push rule diff --git a/Aesop/Saturate.lean b/Aesop/Saturate.lean index b19b9ecd7..880e44446 100644 --- a/Aesop/Saturate.lean +++ b/Aesop/Saturate.lean @@ -68,9 +68,9 @@ where tryNormRules (goal : MVarId) (mvars : UnorderedArraySet MVarId) (preState : Meta.SavedState) : SaturateM (Option GoalDiff) := - withTraceNode `saturate (λ res => return m!"{exceptOptionEmoji res} trying normalisation rules") do + withTraceNode `saturate (fun _ => return m!"trying normalisation rules") do let matchResults ← - withTraceNode `saturate (λ res => return m!"{exceptEmoji res} selecting normalisation rules") do + withTraceNode `saturate (fun _ => return m!"selecting normalisation rules") do profilingRuleSelection do rs.applicableNormalizationRulesWith ∅ goal (include? := (isForwardOrDestructRuleName ·.name)) @@ -78,9 +78,9 @@ where trySafeRules (goal : MVarId) (mvars : UnorderedArraySet MVarId) (preState : Meta.SavedState) : SaturateM (Option GoalDiff) := - withTraceNode `saturate (λ res => return m!"{exceptOptionEmoji res} trying safe rules") do + withTraceNode `saturate (fun _ => return m!"trying safe rules") do let matchResults ← - withTraceNode `saturate (λ res => return m!"{exceptEmoji res} selecting safe rules") do + withTraceNode `saturate (fun _ => return m!"selecting safe rules") do profilingRuleSelection do rs.applicableSafeRulesWith ∅ goal (include? := (isForwardOrDestructRuleName ·.name)) @@ -89,7 +89,7 @@ where runRule {α} (goal : MVarId) (mvars : UnorderedArraySet MVarId) (preState : Meta.SavedState) (matchResult : IndexMatchResult (Rule α)) : SaturateM (Option (GoalDiff × Option (Array Script.LazyStep))) := do - withTraceNode `saturate (λ res => return m!"{exceptOptionEmoji res} running rule {matchResult.rule.name}") do + withTraceNode `saturate (fun _ => return m!"running rule {matchResult.rule.name}") do profilingRule matchResult.rule.name (·.isSome) do let input := { indexMatchLocations := matchResult.locations diff --git a/Aesop/Script/Step.lean b/Aesop/Script/Step.lean index b6202d7c9..227b2c89a 100644 --- a/Aesop/Script/Step.lean +++ b/Aesop/Script/Step.lean @@ -127,7 +127,7 @@ def runFirstSuccessfulTacticBuilder (s : LazyStep) : MetaM Tactic := where tryTacticBuilder (b : TacticBuilder) : MetaM (Option Tactic) := do let tactic ← b - withAesopTraceNode .script (λ res => return m!"{exceptOptionEmoji res} {tactic}") do + withAesopTraceNode .script (fun _ => return m!"{tactic}") do let tacticResult ← observing? do runTacticCapturingPostState tactic.uTactic s.preState [s.preGoal] let some (actualPostState, actualPostGoals) := tacticResult diff --git a/Aesop/Script/StructureDynamic.lean b/Aesop/Script/StructureDynamic.lean index af5d727b3..9786b7495 100644 --- a/Aesop/Script/StructureDynamic.lean +++ b/Aesop/Script/StructureDynamic.lean @@ -82,7 +82,7 @@ structure DynStructureResult where partial def structureDynamicCore (preState : Meta.SavedState) (preGoal : MVarId) (uscript : UScript) : MetaM (Option (UScript × Bool)) := - withAesopTraceNode .script (λ r => return m!"{exceptOptionEmoji r} Dynamically structuring the script") do + withAesopTraceNode .script (fun _ => return m!"Dynamically structuring the script") do aesop_trace[script] "unstructured script:{indentD $ MessageData.joinSep (uscript.map toMessageData |>.toList) "\n"}" let (result?, perfect) ← go preState #[preGoal] |>.run uscript let some result := result? @@ -95,7 +95,7 @@ where if h : 0 < preGoals.size then -- Try to apply the step for the main goal, then solve the remaining goals. let firstGoal := preGoals[0] - let result? ← withAesopTraceNode .script (λ r => return m!"{exceptOptionEmoji r} Focusing main goal {firstGoal.name}") do + let result? ← withAesopTraceNode .script (fun _ => return m!"Focusing main goal {firstGoal.name}") do aesop_trace[script] "goal: {firstGoal.name}{← preState.runMetaM' $ addMessageContext $ indentD firstGoal}" goStructured preState preGoals preGoals[0] match result? with @@ -103,7 +103,7 @@ where | none => -- If this fails, apply the chronologically next step and solve the remaining goals. modify ({ · with perfect := false }) - withAesopTraceNode .script (λ r => return m!"{exceptOptionEmoji r} Applying step to chronologically first goal") do + withAesopTraceNode .script (fun _ => return m!"Applying step to chronologically first goal") do goUnstructured preState preGoals else return some { script := [], postState := preState } diff --git a/Aesop/Script/UScriptToSScript.lean b/Aesop/Script/UScriptToSScript.lean index 1b7f112c0..9195fc097 100644 --- a/Aesop/Script/UScriptToSScript.lean +++ b/Aesop/Script/UScriptToSScript.lean @@ -93,7 +93,7 @@ where end StepTree partial def orderedUScriptToSScript (uscript : UScript) (tacticState : TacticState) : CoreM SScript := - withAesopTraceNode .script (λ e => return m!"{exceptEmoji e} Converting ordered unstructured script to structured script") do + withAesopTraceNode .script (fun _ => return m!"Converting ordered unstructured script to structured script") do aesop_trace[script] "unstructured script:{indentD $ MessageData.joinSep (uscript.map toMessageData |>.toList) "\n"}" let stepTree := uscript.toStepTree aesop_trace[script] "step tree:{indentD $ toMessageData stepTree}" diff --git a/Aesop/Search/SearchM.lean b/Aesop/Search/SearchM.lean index 911cdb90a..8c2000730 100644 --- a/Aesop/Search/SearchM.lean +++ b/Aesop/Search/SearchM.lean @@ -53,19 +53,19 @@ namespace SearchM -- Generate specialized pure/bind implementations so we don't need to optimise -- them on the fly at each use site. instance : Monad (SearchM Q) := - { inferInstanceAs (Monad (SearchM Q)) with } + { (inferInstance : Monad (SearchM Q)) with } instance : MonadRef (SearchM Q) := - { inferInstanceAs (MonadRef (SearchM Q)) with } + { (inferInstance : MonadRef (SearchM Q)) with } instance : Inhabited (SearchM Q α) where default := failure instance : MonadState (State Q) (SearchM Q) := - { inferInstanceAs (MonadStateOf (State Q) (SearchM Q)) with } + { (inferInstance : MonadStateOf (State Q) (SearchM Q)) with } instance : MonadReader Context (SearchM Q) := - { inferInstanceAs (MonadReaderOf Context (SearchM Q)) with } + { (inferInstance : MonadReaderOf Context (SearchM Q)) with } instance : MonadLift TreeM (SearchM Q) where monadLift x := do diff --git a/Aesop/Tracing.lean b/Aesop/Tracing.lean index 1bf0ad868..4cab9d4e3 100644 --- a/Aesop/Tracing.lean +++ b/Aesop/Tracing.lean @@ -146,18 +146,18 @@ variable [Monad m] [MonadTrace m] [MonadLiftT BaseIO m] [MonadLiftT IO m] [MonadRef m] [AddMessageContext m] [MonadOptions m] [MonadAlwaysExcept ε m] @[inline, always_inline] -def withAesopTraceNode (opt : TraceOption) +def withAesopTraceNode [ExceptToTraceResult ε α] (opt : TraceOption) (msg : Except ε α → m MessageData) (k : m α) (collapsed := true) : m α := withTraceNode opt.traceClass msg k collapsed @[inline, always_inline] -def withAesopTraceNodeBefore [ExceptToEmoji ε α] (opt : TraceOption) +def withAesopTraceNodeBefore [ExceptToTraceResult ε α] (opt : TraceOption) (msg : m MessageData) (k : m α) (collapsed := true) : m α := withTraceNodeBefore opt.traceClass (fun _ => msg) k collapsed @[inline, always_inline] -def withConstAesopTraceNode (opt : TraceOption) (msg : m MessageData) (k : m α) - (collapsed := true) : m α := +def withConstAesopTraceNode [ExceptToTraceResult ε α] (opt : TraceOption) + (msg : m MessageData) (k : m α) (collapsed := true) : m α := withAesopTraceNode opt (λ _ => msg) k collapsed end diff --git a/Aesop/Tree/ExtractScript.lean b/Aesop/Tree/ExtractScript.lean index 6e915244b..ff3364afc 100644 --- a/Aesop/Tree/ExtractScript.lean +++ b/Aesop/Tree/ExtractScript.lean @@ -95,7 +95,7 @@ end @[inline] def extractScript : TreeM (UScript × Bool) := - withAesopTraceNode .script (λ r => return m!"{exceptEmoji r} Extract script") do + withAesopTraceNode .script (fun _ => return m!"Extract script") do (← getRootGoal).extractScriptCore.run mutual @@ -131,7 +131,7 @@ mutual end def extractSafePrefixScript : TreeM (UScript × Bool) := do - withAesopTraceNode .script (λ r => return m!"{exceptEmoji r} Extract safe prefix script") do + withAesopTraceNode .script (fun _ => return m!"Extract safe prefix script") do (← getRootGoal).extractSafePrefixScriptCore.run end Aesop diff --git a/Aesop/Tree/TreeM.lean b/Aesop/Tree/TreeM.lean index f81d7d42f..bea085d71 100644 --- a/Aesop/Tree/TreeM.lean +++ b/Aesop/Tree/TreeM.lean @@ -83,7 +83,7 @@ namespace TreeM -- Generate specialized pure/bind implementations so we don't need to optimise -- them on the fly at each use site. instance : Monad TreeM := - { inferInstanceAs (Monad TreeM) with } + { (inferInstance : Monad TreeM) with } instance (priority := low) : MonadStateOf Tree TreeM where get := return (← getThe State).tree diff --git a/Aesop/Util/EqualUpToIds.lean b/Aesop/Util/EqualUpToIds.lean index 146d2b528..2acf719da 100644 --- a/Aesop/Util/EqualUpToIds.lean +++ b/Aesop/Util/EqualUpToIds.lean @@ -50,7 +50,7 @@ abbrev EqualUpToIdsM := -- whole monad stack at every use site. May eventually be covered by `deriving`. @[inline, always_inline] instance : Monad EqualUpToIdsM := - { inferInstanceAs (Monad EqualUpToIdsM) with } + { (inferInstance : Monad EqualUpToIdsM) with } protected def EqualUpToIdsM.run' (x : EqualUpToIdsM α) (commonMCtx? : Option MetavarContext) (mctx₁ mctx₂ : MetavarContext) diff --git a/AesopTest/EqualUpToIds.lean b/AesopTest/EqualUpToIds.lean index 070aa6950..96cadc991 100644 --- a/AesopTest/EqualUpToIds.lean +++ b/AesopTest/EqualUpToIds.lean @@ -8,6 +8,8 @@ import Aesop.Util.Basic import Aesop.Util.EqualUpToIds import Aesop.Tree.RunMetaM +set_option linter.unreachableTactic false + -- Some simple test cases for the EqualUpToIds module. The module is mostly -- tested by using it in script validation, which is run on almost all Aesop -- calls in the test suite. diff --git a/lake-manifest.json b/lake-manifest.json index f95b3b16c..ec34a4d7d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "bd58e3506632241b59e406902d5e42b73cdeccce", + "rev": "46f6618b9942c1f67ebe3b8051163ddb8d8ff496", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0-rc6", + "inputRev": "v4.29.0-rc7", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index 7861ed7d0..4eb5c7e2e 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,7 @@ platformIndependent = true [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.29.0-rc6" +rev = "v4.29.0-rc7" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index 87b20aaf8..4d6fa16ed 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0-rc6 +leanprover/lean4:v4.29.0-rc7 From 3426969888a264d3f69b6f30ab50aa11f28eb38d Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Wed, 25 Mar 2026 11:10:17 +1100 Subject: [PATCH 08/17] chore: bump toolchain to v4.29.0-rc8 (#320) --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index ec34a4d7d..c0154d4a6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "46f6618b9942c1f67ebe3b8051163ddb8d8ff496", + "rev": "bce25af79ec73f5e63240d4399a4cd8a6a227fcb", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0-rc7", + "inputRev": "v4.29.0-rc8", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index 4eb5c7e2e..bb20f2381 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,7 @@ platformIndependent = true [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.29.0-rc7" +rev = "v4.29.0-rc8" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index 4d6fa16ed..ccec351f4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0-rc7 +leanprover/lean4:v4.29.0-rc8 From 7152850e7b216a0d409701617721b6e469d34bf6 Mon Sep 17 00:00:00 2001 From: Garmelon Date: Sat, 28 Mar 2026 12:25:57 +0100 Subject: [PATCH 09/17] chore: bump toolchain to v4.29.0 (#321) --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index c0154d4a6..e137cd78c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "bce25af79ec73f5e63240d4399a4cd8a6a227fcb", + "rev": "756e3321fd3b02a85ffda19fef789916223e578c", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0-rc8", + "inputRev": "v4.29.0", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index bb20f2381..d24154ed4 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,7 @@ platformIndependent = true [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.29.0-rc8" +rev = "v4.29.0" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index ccec351f4..14791d727 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0-rc8 +leanprover/lean4:v4.29.0 From f74c7555aaa94eadd7b7bff9170f7983f92aac21 Mon Sep 17 00:00:00 2001 From: Garmelon Date: Thu, 2 Apr 2026 20:24:20 +0200 Subject: [PATCH 10/17] chore: bump toolchain to v4.30.0-rc1 (#322) --- Aesop/Util/Basic.lean | 2 +- AesopTest/27.lean | 58 ++++++++++++++++--------------------------- AesopTest/Filter.lean | 4 +-- lake-manifest.json | 9 ++++--- lakefile.toml | 2 +- lean-toolchain | 2 +- 6 files changed, 32 insertions(+), 45 deletions(-) diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean index 4b6e203f3..a0585ebb0 100644 --- a/Aesop/Util/Basic.lean +++ b/Aesop/Util/Basic.lean @@ -449,7 +449,7 @@ where (acc, lctx) dummyLDecl (name : Name) : LocalDecl := - .cdecl 0 ⟨`_⟩ name (.sort levelZero) .default .default + .cdecl 0 ⟨`_⟩ name (.sort Level.zero) .default .default def Name.ofComponents (cs : List Name) : Name := cs.foldl (init := .anonymous) λ diff --git a/AesopTest/27.lean b/AesopTest/27.lean index 533b03df5..2da025915 100644 --- a/AesopTest/27.lean +++ b/AesopTest/27.lean @@ -20,24 +20,17 @@ inductive All (P : α → Prop) : List α → Prop /-- trace: [aesop.proof] Final proof: - (fun (h_1 : All P (x :: xs)) => - ((fun (h_2 : All P (x :: xs)) => - (casesOn (P := P) (motive := fun a x_1 => x :: xs = a → h ≍ x_1 → P x ∧ All P xs) h_2 - (fun h_3 => False.elim (noConfusion_of_Nat List.ctorIdx h_3)) fun {x_1} {xs_1} a a_1 h_3 => - List.cons.noConfusion h_3 fun head_eq => - Eq.ndrec (motive := fun {x_1} => - ∀ (a : P x_1), xs ≍ xs_1 → h ≍ cons (P := P) a a_1 → P x ∧ All P xs) - (fun a tail_eq => - Eq.ndrec (motive := fun {xs_1} => - ∀ (a_1 : All P xs_1), h ≍ cons (P := P) a a_1 → P x ∧ All P xs) - (fun a_1 h => - of_eq_true (Eq.trans (congr (congrArg And (eq_true a)) (eq_true a_1)) (and_self True))) - (eq_of_heq tail_eq) a_1) - (eq_of_heq head_eq) a : - x :: xs = x :: xs → h ≍ h_2 → P x ∧ All P xs)) - h_1 : - x :: xs = x :: xs → h ≍ h_1 → P x ∧ All P xs)) - h (Eq.refl (x :: xs)) (HEq.refl h) + casesOn (P := P) (motive := fun a x_1 => x :: xs = a → h ≍ x_1 → P x ∧ All P xs) h + (fun h_1 => False.elim (noConfusion_of_Nat List.ctorIdx h_1)) + (fun {x_1} {xs_1} a a_1 h_1 => + List.cons.noConfusion h_1 fun head_eq => + Eq.ndrec (motive := fun {x_1} => ∀ (a : P x_1), xs ≍ xs_1 → h ≍ cons (P := P) a a_1 → P x ∧ All P xs) + (fun a tail_eq => + Eq.ndrec (motive := fun {xs_1} => ∀ (a_1 : All P xs_1), h ≍ cons (P := P) a a_1 → P x ∧ All P xs) + (fun a_1 h => of_eq_true (Eq.trans (congr (congrArg And (eq_true a)) (eq_true a_1)) (and_self True))) + (eq_of_heq tail_eq) a_1) + (eq_of_heq head_eq) a) + (Eq.refl (x :: xs)) (HEq.refl h) -/ #guard_msgs in theorem All.split_cons (P : α → Prop) (x : α) (xs : List α) (h : All P (x :: xs)) @@ -47,21 +40,14 @@ theorem All.split_cons (P : α → Prop) (x : α) (xs : List α) (h : All P (x : theorem All.split_cons₂ (P : α → Prop) (x : α) (xs : List α) (h : All P (x :: xs)) : P x ∧ All P xs := - (fun (h_1 : All P (x :: xs)) => - ((fun (h_2 : All P (x :: xs)) => - (casesOn (P := P) (motive := fun a x_1 => x :: xs = a → h ≍ x_1 → P x ∧ All P xs) h_2 - (fun h_3 => False.elim (noConfusion_of_Nat List.ctorIdx h_3)) fun {x_1} {xs_1} a a_1 h_3 => - List.cons.noConfusion h_3 fun head_eq => - Eq.ndrec (motive := fun {x_1} => - ∀ (a : P x_1), xs ≍ xs_1 → h ≍ cons (P := P) a a_1 → P x ∧ All P xs) - (fun a tail_eq => - Eq.ndrec (motive := fun {xs_1} => - ∀ (a_1 : All P xs_1), h ≍ cons (P := P) a a_1 → P x ∧ All P xs) - (fun a_1 h => - of_eq_true (Eq.trans (congr (congrArg And (eq_true a)) (eq_true a_1)) (and_self True))) - (eq_of_heq tail_eq) a_1) - (eq_of_heq head_eq) a : - x :: xs = x :: xs → h ≍ h_2 → P x ∧ All P xs)) - h_1 : - x :: xs = x :: xs → h ≍ h_1 → P x ∧ All P xs)) - h (Eq.refl (x :: xs)) (HEq.refl h) + casesOn (P := P) (motive := fun a x_1 => x :: xs = a → h ≍ x_1 → P x ∧ All P xs) h + (fun h_1 => False.elim (noConfusion_of_Nat List.ctorIdx h_1)) + (fun {x_1} {xs_1} a a_1 h_1 => + List.cons.noConfusion h_1 fun head_eq => + Eq.ndrec (motive := fun {x_1} => ∀ (a : P x_1), xs ≍ xs_1 → h ≍ cons (P := P) a a_1 → P x ∧ All P xs) + (fun a tail_eq => + Eq.ndrec (motive := fun {xs_1} => ∀ (a_1 : All P xs_1), h ≍ cons (P := P) a a_1 → P x ∧ All P xs) + (fun a_1 h => of_eq_true (Eq.trans (congr (congrArg And (eq_true a)) (eq_true a_1)) (and_self True))) + (eq_of_heq tail_eq) a_1) + (eq_of_heq head_eq) a) + (Eq.refl (x :: xs)) (HEq.refl h) diff --git a/AesopTest/Filter.lean b/AesopTest/Filter.lean index 99271d0cb..2eb87727e 100644 --- a/AesopTest/Filter.lean +++ b/AesopTest/Filter.lean @@ -34,8 +34,8 @@ theorem filter_cons_false (h : ¬ p a) : filter p (a :: as) = filter p as := by @[aesop 50% [constructors, cases]] inductive Mem (a : α) : List α → Prop where - | head {as} : Mem a (a::as) - | tail {as} : Mem a as → Mem a (a'::as) + | head {as : _} : Mem a (a::as) + | tail {as : _} : Mem a as → Mem a (a'::as) infix:50 " ∈ " => Mem diff --git a/lake-manifest.json b/lake-manifest.json index e137cd78c..c672bbce1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,15 +1,16 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "", - "rev": "756e3321fd3b02a85ffda19fef789916223e578c", + "rev": "bf597c77bf9b8e66720d724928207f5911533113", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "v4.30.0-rc1", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml index d24154ed4..b8aa17fb3 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,7 @@ platformIndependent = true [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.29.0" +rev = "v4.30.0-rc1" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index 14791d727..2210cba4f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 +leanprover/lean4:v4.30.0-rc1 From 6ce76d33bd557bb60718198447ecfda621617502 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Thu, 9 Apr 2026 06:33:23 +0000 Subject: [PATCH 11/17] chore: adapt to new do elaborator --- Aesop/Builder/Forward.lean | 2 +- Aesop/Frontend/Command.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean index 83feedab1..92e2f68ea 100644 --- a/Aesop/Builder/Forward.lean +++ b/Aesop/Builder/Forward.lean @@ -28,7 +28,7 @@ namespace RuleBuilder def getForwardIndexingMode (type : Expr) (immediate : UnorderedArraySet PremiseIndex) : MetaM IndexingMode := do - let immediate := immediate.toArray.map (·.toNat) + let immediate := immediate.toArray.map PremiseIndex.toNat match immediate.max? with | some i => withoutModifyingState do diff --git a/Aesop/Frontend/Command.lean b/Aesop/Frontend/Command.lean index e7fe401d2..ce96ea74f 100644 --- a/Aesop/Frontend/Command.lean +++ b/Aesop/Frontend/Command.lean @@ -78,7 +78,7 @@ elab_rules : command def evalStatsReport? (name : Name) : CoreM (Option StatsReport) := do try - unsafe evalConstCheck StatsReport ``StatsReport name + unsafe some <$> evalConstCheck StatsReport ``StatsReport name catch _ => return none From f0c6e183ea26531e82773feb4b73ab6595ca17a5 Mon Sep 17 00:00:00 2001 From: Garmelon Date: Fri, 17 Apr 2026 17:14:07 +0200 Subject: [PATCH 12/17] chore: bump toolchain to v4.30.0-rc2 (#325) --- lake-manifest.json | 6 +++--- lakefile.toml | 4 ++-- lean-toolchain | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index c672bbce1..67b8ed581 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,11 +4,11 @@ [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "scope": "", - "rev": "bf597c77bf9b8e66720d724928207f5911533113", + "scope": "leanprover-community", + "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc1", + "inputRev": "v4.30.0-rc2", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index b8aa17fb3..4e3f80798 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,8 +6,8 @@ platformIndependent = true [[require]] name = "batteries" -git = "https://github.com/leanprover-community/batteries" -rev = "v4.30.0-rc1" +scope = "leanprover-community" +rev = "v4.30.0-rc2" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index 2210cba4f..6c7e31fff 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0-rc1 +leanprover/lean4:v4.30.0-rc2 From 8d606366c43e7c677abe3930d74f20c1ce7a5be4 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 21 Apr 2026 12:48:56 +1000 Subject: [PATCH 13/17] chore: silence some tests (#311) Co-authored-by: Claude Opus 4.6 --- AesopTest/EqualUpToIds.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/AesopTest/EqualUpToIds.lean b/AesopTest/EqualUpToIds.lean index 96cadc991..ba4f78294 100644 --- a/AesopTest/EqualUpToIds.lean +++ b/AesopTest/EqualUpToIds.lean @@ -14,6 +14,8 @@ set_option linter.unreachableTactic false -- tested by using it in script validation, which is run on almost all Aesop -- calls in the test suite. +set_option linter.unreachableTactic false + open Aesop Lean Lean.Elab.Tactic def assertEqualTactics (t₁ t₂ : TacticM Unit) : TacticM Unit := do From ddd9ea80aa79c50d84e2643d59af674798a77770 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 21 Apr 2026 14:37:06 +1000 Subject: [PATCH 14/17] feat: minimize Batteries and Lean imports (#317) --- Aesop/BaseM.lean | 1 + Aesop/Builder/Apply.lean | 2 ++ Aesop/Builder/Basic.lean | 1 + Aesop/Builder/Cases.lean | 1 + Aesop/Builder/Constructors.lean | 1 + Aesop/Builder/Default.lean | 1 + Aesop/Builder/Forward.lean | 1 + Aesop/Builder/NormSimp.lean | 1 + Aesop/Builder/Tactic.lean | 1 + Aesop/Builder/Unfold.lean | 1 + Aesop/BuiltinRules/DestructProducts.lean | 1 + Aesop/EMap.lean | 1 + Aesop/ElabM.lean | 5 ++++- Aesop/Exception.lean | 2 +- Aesop/Forward/Match.lean | 4 ++-- Aesop/Forward/Match/Types.lean | 1 + Aesop/Forward/RuleInfo.lean | 2 ++ Aesop/Frontend/Basic.lean | 4 +++- Aesop/Frontend/Tactic.lean | 1 + Aesop/Index.lean | 4 ++-- Aesop/Index/Basic.lean | 1 + Aesop/Index/DiscrTreeConfig.lean | 4 +++- Aesop/Index/Forward.lean | 3 ++- Aesop/Index/RulePattern.lean | 3 ++- Aesop/Options/Public.lean | 3 ++- Aesop/Rule.lean | 1 + Aesop/Rule/Basic.lean | 1 + Aesop/Rule/Forward.lean | 1 + Aesop/RulePattern.lean | 1 + Aesop/RuleSet.lean | 2 ++ Aesop/RuleSet/Member.lean | 1 + Aesop/RuleSet/Name.lean | 2 +- Aesop/RuleTac/Basic.lean | 2 +- Aesop/RuleTac/Descr.lean | 1 + Aesop/RuleTac/ElabRuleTerm.lean | 4 ++++ Aesop/RuleTac/FVarIdSubst.lean | 4 +++- Aesop/RuleTac/Forward.lean | 3 ++- Aesop/RuleTac/Forward/Basic.lean | 1 + Aesop/RuleTac/GoalDiff.lean | 1 + Aesop/RuleTac/Tactic.lean | 1 + Aesop/Saturate.lean | 4 ++-- Aesop/Script/Check.lean | 1 + Aesop/Script/CtorNames.lean | 1 + Aesop/Script/GoalWithMVars.lean | 3 ++- Aesop/Script/Main.lean | 2 ++ Aesop/Script/OptimizeSyntax.lean | 3 ++- Aesop/Script/SScript.lean | 1 + Aesop/Script/ScriptM.lean | 1 + Aesop/Script/SpecificTactics.lean | 4 +++- Aesop/Script/Step.lean | 3 ++- Aesop/Script/StructureDynamic.lean | 2 ++ Aesop/Script/StructureStatic.lean | 1 + Aesop/Script/Tactic.lean | 3 ++- Aesop/Script/TacticState.lean | 3 ++- Aesop/Script/UScript.lean | 2 ++ Aesop/Script/UScriptToSScript.lean | 1 + Aesop/Script/Util.lean | 2 +- Aesop/Search/Expansion/Basic.lean | 1 + Aesop/Search/Expansion/Norm.lean | 3 ++- Aesop/Stats/Basic.lean | 1 + Aesop/Stats/Extension.lean | 1 + Aesop/Stats/File.lean | 1 + Aesop/Stats/Report.lean | 1 + Aesop/Tracing.lean | 2 +- Aesop/Tree/AddRapp.lean | 1 + Aesop/Tree/Check.lean | 3 ++- Aesop/Tree/ExtractProof.lean | 3 ++- Aesop/Tree/Tracing.lean | 1 + Aesop/Tree/UnsafeQueue.lean | 1 + Aesop/Util/Basic.lean | 8 +++++--- Aesop/Util/Tactic.lean | 4 ++-- Aesop/Util/Tactic/Ext.lean | 1 + Aesop/Util/Tactic/Unfold.lean | 1 + Aesop/Util/Unfold.lean | 3 ++- 74 files changed, 115 insertions(+), 34 deletions(-) diff --git a/Aesop/BaseM.lean b/Aesop/BaseM.lean index c51dc0619..59d068aed 100644 --- a/Aesop/BaseM.lean +++ b/Aesop/BaseM.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Stats.Basic public import Aesop.RulePattern.Cache diff --git a/Aesop/Builder/Apply.lean b/Aesop/Builder/Apply.lean index 891f03e4f..6fc36ac49 100644 --- a/Aesop/Builder/Apply.lean +++ b/Aesop/Builder/Apply.lean @@ -5,7 +5,9 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Builder.Basic +import Batteries.Lean.Expr public section diff --git a/Aesop/Builder/Basic.lean b/Aesop/Builder/Basic.lean index ad6e27d8d..f2d8eea38 100644 --- a/Aesop/Builder/Basic.lean +++ b/Aesop/Builder/Basic.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.ElabM public import Aesop.Rule.Name public import Aesop.RuleSet.Member diff --git a/Aesop/Builder/Cases.lean b/Aesop/Builder/Cases.lean index 7e75a6e9e..2ad7003a5 100644 --- a/Aesop/Builder/Cases.lean +++ b/Aesop/Builder/Cases.lean @@ -7,6 +7,7 @@ module public import Aesop.Builder.Basic public import Aesop.RuleTac.Cases +import Batteries.Lean.Expr public section diff --git a/Aesop/Builder/Constructors.lean b/Aesop/Builder/Constructors.lean index e7a525987..a8d3b9088 100644 --- a/Aesop/Builder/Constructors.lean +++ b/Aesop/Builder/Constructors.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Builder.Basic public section diff --git a/Aesop/Builder/Default.lean b/Aesop/Builder/Default.lean index ecc91aee2..9aad7cddc 100644 --- a/Aesop/Builder/Default.lean +++ b/Aesop/Builder/Default.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Builder.Constructors public import Aesop.Builder.NormSimp public import Aesop.Builder.Tactic diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean index 83feedab1..04510f6c2 100644 --- a/Aesop/Builder/Forward.lean +++ b/Aesop/Builder/Forward.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Builder.Basic public section diff --git a/Aesop/Builder/NormSimp.lean b/Aesop/Builder/NormSimp.lean index b04b38e17..3eda4f868 100644 --- a/Aesop/Builder/NormSimp.lean +++ b/Aesop/Builder/NormSimp.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Builder.Basic public section diff --git a/Aesop/Builder/Tactic.lean b/Aesop/Builder/Tactic.lean index 5641f34fb..85bbd31d2 100644 --- a/Aesop/Builder/Tactic.lean +++ b/Aesop/Builder/Tactic.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Builder.Basic public section diff --git a/Aesop/Builder/Unfold.lean b/Aesop/Builder/Unfold.lean index 0ef77aba9..8df2c434a 100644 --- a/Aesop/Builder/Unfold.lean +++ b/Aesop/Builder/Unfold.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Builder.Basic public import Aesop.Util.Unfold diff --git a/Aesop/BuiltinRules/DestructProducts.lean b/Aesop/BuiltinRules/DestructProducts.lean index 71e039e35..e70736bcf 100644 --- a/Aesop/BuiltinRules/DestructProducts.lean +++ b/Aesop/BuiltinRules/DestructProducts.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +public meta import Lean.Meta.Tactic.Apply public import Aesop.Frontend.Attribute public import Aesop.Frontend.Extension public import Aesop.Frontend.RuleExpr diff --git a/Aesop/EMap.lean b/Aesop/EMap.lean index a0940a829..3cafa5e42 100644 --- a/Aesop/EMap.lean +++ b/Aesop/EMap.lean @@ -6,6 +6,7 @@ Authors: Jannis Limperg module +meta import Lean.Parser.Do public import Aesop.Tracing public import Aesop.Util.Basic diff --git a/Aesop/ElabM.lean b/Aesop/ElabM.lean index a139c4cb2..63edae9d4 100644 --- a/Aesop/ElabM.lean +++ b/Aesop/ElabM.lean @@ -5,7 +5,10 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Lean.Expr +public import Lean.Meta.Basic +public import Lean.Elab.Term.TermElabM public section diff --git a/Aesop/Exception.lean b/Aesop/Exception.lean index fa0d891aa..c9e4b50cd 100644 --- a/Aesop/Exception.lean +++ b/Aesop/Exception.lean @@ -5,7 +5,7 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean.Exception public section diff --git a/Aesop/Forward/Match.lean b/Aesop/Forward/Match.lean index 5efcd179e..ac521c1a0 100644 --- a/Aesop/Forward/Match.lean +++ b/Aesop/Forward/Match.lean @@ -5,6 +5,7 @@ Authors: Xavier Généreux, Jannis Limperg -/ module +import Lean.Meta.Tactic.Apply public import Aesop.Forward.Match.Types public import Aesop.Forward.PremiseIndex public import Aesop.Forward.SlotIndex @@ -14,9 +15,8 @@ public import Aesop.RuleTac.Descr public import Aesop.RuleTac.ElabRuleTerm public import Aesop.RuleTac.Forward.Basic public import Aesop.Script.SpecificTactics -public import Batteries.Lean.Meta.UnusedNames +import Batteries.Lean.Meta.UnusedNames public import Aesop.Util.Basic -public import Lean public section diff --git a/Aesop/Forward/Match/Types.lean b/Aesop/Forward/Match/Types.lean index 69750aff3..cfe70533d 100644 --- a/Aesop/Forward/Match/Types.lean +++ b/Aesop/Forward/Match/Types.lean @@ -1,5 +1,6 @@ module +meta import Lean.Parser.Do public import Aesop.Forward.PremiseIndex public import Aesop.Forward.SlotIndex public import Aesop.Forward.Substitution diff --git a/Aesop/Forward/RuleInfo.lean b/Aesop/Forward/RuleInfo.lean index cf31c14df..94c3a8688 100644 --- a/Aesop/Forward/RuleInfo.lean +++ b/Aesop/Forward/RuleInfo.lean @@ -5,11 +5,13 @@ Authors: Xavier Généreux, Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Forward.PremiseIndex public import Aesop.Forward.SlotIndex public import Aesop.RulePattern public import Aesop.Util.Basic public import Aesop.Util.UnionFind +public import Batteries.Data.Array.Basic public section diff --git a/Aesop/Frontend/Basic.lean b/Aesop/Frontend/Basic.lean index 4ef121244..89ca55575 100644 --- a/Aesop/Frontend/Basic.lean +++ b/Aesop/Frontend/Basic.lean @@ -5,7 +5,9 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Lean.Exception +public import Lean.Elab.Exception public section diff --git a/Aesop/Frontend/Tactic.lean b/Aesop/Frontend/Tactic.lean index eb0a61f64..f4b4bef9e 100644 --- a/Aesop/Frontend/Tactic.lean +++ b/Aesop/Frontend/Tactic.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +import Lean public import Aesop.Frontend.RuleExpr public import Aesop.Options public import Batteries.Linter.UnreachableTactic diff --git a/Aesop/Index.lean b/Aesop/Index.lean index 6f276ca24..fbfb46107 100644 --- a/Aesop/Index.lean +++ b/Aesop/Index.lean @@ -12,8 +12,8 @@ public import Aesop.RulePattern public import Aesop.Rule.Basic public import Aesop.Tracing public import Batteries.Lean.Meta.InstantiateMVars -public import Batteries.Lean.PersistentHashSet -public import Batteries.Lean.Meta.DiscrTree +import Batteries.Lean.PersistentHashSet +import Batteries.Lean.Meta.DiscrTree public section diff --git a/Aesop/Index/Basic.lean b/Aesop/Index/Basic.lean index 15d05eebe..2258446d6 100644 --- a/Aesop/Index/Basic.lean +++ b/Aesop/Index/Basic.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Util.Basic public import Aesop.Rule.Name public import Aesop.RulePattern diff --git a/Aesop/Index/DiscrTreeConfig.lean b/Aesop/Index/DiscrTreeConfig.lean index 1e7146592..7994bd61e 100644 --- a/Aesop/Index/DiscrTreeConfig.lean +++ b/Aesop/Index/DiscrTreeConfig.lean @@ -5,7 +5,9 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Lean.Meta.Basic +public import Lean.Meta.DiscrTree.Types public section diff --git a/Aesop/Index/Forward.lean b/Aesop/Index/Forward.lean index ad15d0759..ec32d2ddd 100644 --- a/Aesop/Index/Forward.lean +++ b/Aesop/Index/Forward.lean @@ -5,10 +5,11 @@ Authors: Xavier Généreux, Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Forward.Match.Types public import Aesop.Rule.Forward public import Aesop.Index.Basic -public import Batteries.Lean.Meta.DiscrTree +import Batteries.Lean.Meta.DiscrTree public section diff --git a/Aesop/Index/RulePattern.lean b/Aesop/Index/RulePattern.lean index aea54dbd5..bf045fd04 100644 --- a/Aesop/Index/RulePattern.lean +++ b/Aesop/Index/RulePattern.lean @@ -5,10 +5,11 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Index.Basic public import Aesop.Util.OrderedHashSet public import Aesop.RuleTac.GoalDiff -public import Batteries.Lean.Meta.DiscrTree +import Batteries.Lean.Meta.DiscrTree public section diff --git a/Aesop/Options/Public.lean b/Aesop/Options/Public.lean index 0e8352d27..9646121a0 100644 --- a/Aesop/Options/Public.lean +++ b/Aesop/Options/Public.lean @@ -1,6 +1,7 @@ module -public import Lean +import Lean +public import Lean.Data.Options public section diff --git a/Aesop/Rule.lean b/Aesop/Rule.lean index 2df2bfeda..3095d4c3c 100644 --- a/Aesop/Rule.lean +++ b/Aesop/Rule.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg, Asta Halkjær From -/ module +meta import Lean.Parser.Do public import Aesop.Rule.Basic public import Aesop.Percent diff --git a/Aesop/Rule/Basic.lean b/Aesop/Rule/Basic.lean index 2233a9002..0afa47e1d 100644 --- a/Aesop/Rule/Basic.lean +++ b/Aesop/Rule/Basic.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Index.Basic public import Aesop.Rule.Name public import Aesop.RuleTac.Basic diff --git a/Aesop/Rule/Forward.lean b/Aesop/Rule/Forward.lean index 59a93eede..8547ae97d 100644 --- a/Aesop/Rule/Forward.lean +++ b/Aesop/Rule/Forward.lean @@ -5,6 +5,7 @@ Authors: Xavier Généreux, Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Forward.RuleInfo public import Aesop.Percent public import Aesop.Rule.Name diff --git a/Aesop/RulePattern.lean b/Aesop/RulePattern.lean index ec27c82c6..d04d1380d 100644 --- a/Aesop/RulePattern.lean +++ b/Aesop/RulePattern.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Forward.Substitution public import Aesop.BaseM public import Aesop.Rule.Name diff --git a/Aesop/RuleSet.lean b/Aesop/RuleSet.lean index 66b338064..887ccabbd 100644 --- a/Aesop/RuleSet.lean +++ b/Aesop/RuleSet.lean @@ -10,6 +10,8 @@ public import Aesop.Index.Forward public import Aesop.RuleSet.Filter public import Aesop.RuleSet.Member public import Aesop.Tree.Data.ForwardRuleMatches +import Batteries.Lean.PersistentHashMap +import Batteries.Lean.PersistentHashSet public section diff --git a/Aesop/RuleSet/Member.lean b/Aesop/RuleSet/Member.lean index 6deab9e1c..33d704fa7 100644 --- a/Aesop/RuleSet/Member.lean +++ b/Aesop/RuleSet/Member.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Rule public import Aesop.Rule.Forward diff --git a/Aesop/RuleSet/Name.lean b/Aesop/RuleSet/Name.lean index 62c5792e6..9de22f5c3 100644 --- a/Aesop/RuleSet/Name.lean +++ b/Aesop/RuleSet/Name.lean @@ -5,7 +5,7 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean public section diff --git a/Aesop/RuleTac/Basic.lean b/Aesop/RuleTac/Basic.lean index d3d69eaa8..6c736b5e6 100644 --- a/Aesop/RuleTac/Basic.lean +++ b/Aesop/RuleTac/Basic.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Forward.Match.Types public import Aesop.Index.Basic public import Aesop.Percent @@ -13,7 +14,6 @@ public import Aesop.RuleTac.GoalDiff public import Aesop.RuleTac.FVarIdSubst public import Aesop.Script.CtorNames public import Aesop.Script.Step -public import Batteries.Lean.Meta.SavedState public import Aesop.Options.Internal public section diff --git a/Aesop/RuleTac/Descr.lean b/Aesop/RuleTac/Descr.lean index 0a51f5a9e..716ebef3b 100644 --- a/Aesop/RuleTac/Descr.lean +++ b/Aesop/RuleTac/Descr.lean @@ -1,5 +1,6 @@ module +meta import Lean.Parser.Do public import Aesop.RuleTac.Basic public import Aesop.Forward.Match.Types diff --git a/Aesop/RuleTac/ElabRuleTerm.lean b/Aesop/RuleTac/ElabRuleTerm.lean index 55535d1c7..b8d509462 100644 --- a/Aesop/RuleTac/ElabRuleTerm.lean +++ b/Aesop/RuleTac/ElabRuleTerm.lean @@ -5,6 +5,10 @@ Authors: Jannis Limperg -/ module +import Lean +public import Lean.Elab.Tactic.Basic +public import Lean.Meta.Tactic.Simp.Types +public import Lean.Meta.Tactic.Simp.Simproc public import Aesop.ElabM public section diff --git a/Aesop/RuleTac/FVarIdSubst.lean b/Aesop/RuleTac/FVarIdSubst.lean index 8f0130d6c..5b4595fb8 100644 --- a/Aesop/RuleTac/FVarIdSubst.lean +++ b/Aesop/RuleTac/FVarIdSubst.lean @@ -5,7 +5,9 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Std.Data.HashMap.Basic +public import Lean.Meta.Tactic.FVarSubst public section diff --git a/Aesop/RuleTac/Forward.lean b/Aesop/RuleTac/Forward.lean index 4e031c64a..c9c19a819 100644 --- a/Aesop/RuleTac/Forward.lean +++ b/Aesop/RuleTac/Forward.lean @@ -5,12 +5,13 @@ Authors: Jannis Limperg -/ module +import Lean public import Aesop.Forward.Match public import Aesop.RuleTac.Basic public import Aesop.RuleTac.ElabRuleTerm public import Aesop.RuleTac.Forward.Basic public import Aesop.Script.SpecificTactics -public import Batteries.Lean.Meta.UnusedNames +import Batteries.Lean.Meta.UnusedNames public section diff --git a/Aesop/RuleTac/Forward/Basic.lean b/Aesop/RuleTac/Forward/Basic.lean index 0d5038afb..56f08a3a3 100644 --- a/Aesop/RuleTac/Forward/Basic.lean +++ b/Aesop/RuleTac/Forward/Basic.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +import Lean public import Aesop.Util.Basic public import Aesop.Util.EqualUpToIds diff --git a/Aesop/RuleTac/GoalDiff.lean b/Aesop/RuleTac/GoalDiff.lean index 82966013a..0bcf12cd2 100644 --- a/Aesop/RuleTac/GoalDiff.lean +++ b/Aesop/RuleTac/GoalDiff.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.BaseM public import Aesop.RuleTac.FVarIdSubst public import Aesop.Util.Basic diff --git a/Aesop/RuleTac/Tactic.lean b/Aesop/RuleTac/Tactic.lean index 40029a091..8596f4bad 100644 --- a/Aesop/RuleTac/Tactic.lean +++ b/Aesop/RuleTac/Tactic.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg, Kaiyu Yang -/ module +meta import Lean.Parser.Do public import Aesop.RuleTac.Basic public import Aesop.Script.Step diff --git a/Aesop/Saturate.lean b/Aesop/Saturate.lean index 880e44446..a4e28d400 100644 --- a/Aesop/Saturate.lean +++ b/Aesop/Saturate.lean @@ -11,7 +11,7 @@ public import Aesop.RuleSet public import Aesop.RuleTac public import Aesop.Search.Expansion.Basic public import Aesop.Script.Check -public import Batteries.Data.BinomialHeap.Basic +import Batteries.Data.BinomialHeap.Basic public section @@ -124,7 +124,7 @@ where namespace Stateful -abbrev Queue := BinomialHeap ForwardRuleMatch ForwardRuleMatch.le +private abbrev Queue := BinomialHeap ForwardRuleMatch ForwardRuleMatch.le partial def saturateCore (rs : LocalRuleSet) (goal : MVarId) : SaturateM MVarId := withExceptionPrefix "saturate: internal error: " do diff --git a/Aesop/Script/Check.lean b/Aesop/Script/Check.lean index af8d83b79..cbbe96f82 100644 --- a/Aesop/Script/Check.lean +++ b/Aesop/Script/Check.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Check public import Aesop.Script.UScript diff --git a/Aesop/Script/CtorNames.lean b/Aesop/Script/CtorNames.lean index 34a0dd308..2e2826dc6 100644 --- a/Aesop/Script/CtorNames.lean +++ b/Aesop/Script/CtorNames.lean @@ -1,5 +1,6 @@ module +public import Lean.Meta.Tactic.Induction public import Aesop.Util.Basic public section diff --git a/Aesop/Script/GoalWithMVars.lean b/Aesop/Script/GoalWithMVars.lean index 48a13ab4a..ede01d73e 100644 --- a/Aesop/Script/GoalWithMVars.lean +++ b/Aesop/Script/GoalWithMVars.lean @@ -1,6 +1,7 @@ module -public import Lean +import Lean +public import Lean.Meta.Basic public section diff --git a/Aesop/Script/Main.lean b/Aesop/Script/Main.lean index e4cc6d05f..7836a6b43 100644 --- a/Aesop/Script/Main.lean +++ b/Aesop/Script/Main.lean @@ -5,12 +5,14 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Script.Check public import Aesop.Script.StructureDynamic public import Aesop.Script.StructureStatic public import Aesop.Script.OptimizeSyntax public import Aesop.Stats.Basic public import Aesop.Options.Internal +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Script/OptimizeSyntax.lean b/Aesop/Script/OptimizeSyntax.lean index f580dc2cb..653645076 100644 --- a/Aesop/Script/OptimizeSyntax.lean +++ b/Aesop/Script/OptimizeSyntax.lean @@ -5,7 +5,8 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Std.Data.HashSet.Basic public section diff --git a/Aesop/Script/SScript.lean b/Aesop/Script/SScript.lean index c306bf3d0..2b0aa0fcd 100644 --- a/Aesop/Script/SScript.lean +++ b/Aesop/Script/SScript.lean @@ -1,6 +1,7 @@ module public import Aesop.Script.Step +import Batteries.Tactic.PermuteGoals public section diff --git a/Aesop/Script/ScriptM.lean b/Aesop/Script/ScriptM.lean index cbad6b7c9..a9796b1b0 100644 --- a/Aesop/Script/ScriptM.lean +++ b/Aesop/Script/ScriptM.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.BaseM public import Aesop.Script.Step public import Aesop.Script.Tactic diff --git a/Aesop/Script/SpecificTactics.lean b/Aesop/Script/SpecificTactics.lean index 8ff45503c..ac16f310d 100644 --- a/Aesop/Script/SpecificTactics.lean +++ b/Aesop/Script/SpecificTactics.lean @@ -5,13 +5,15 @@ Authors: Jannis Limperg -/ module +import Lean +public import Lean.Meta.Tactic.Cases public import Aesop.Util.Tactic public import Aesop.Util.Tactic.Ext public import Aesop.Util.Tactic.Unfold public import Aesop.Util.Unfold public import Aesop.Script.CtorNames public import Aesop.Script.ScriptM -public import Batteries.Lean.Meta.Inaccessible +import Batteries.Lean.Meta.Inaccessible public section diff --git a/Aesop/Script/Step.lean b/Aesop/Script/Step.lean index 227b2c89a..257cb9d21 100644 --- a/Aesop/Script/Step.lean +++ b/Aesop/Script/Step.lean @@ -10,7 +10,8 @@ public import Aesop.Script.Tactic public import Aesop.Script.TacticState public import Aesop.Script.Util public import Aesop.Tracing -public import Batteries.Tactic.PermuteGoals +import Batteries.Tactic.PermuteGoals +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Script/StructureDynamic.lean b/Aesop/Script/StructureDynamic.lean index 9786b7495..5c8eb98b5 100644 --- a/Aesop/Script/StructureDynamic.lean +++ b/Aesop/Script/StructureDynamic.lean @@ -5,11 +5,13 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Script.UScript public import Aesop.Script.UScriptToSScript public import Aesop.Script.Util public import Aesop.Script.SScript public import Aesop.Tracing +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Script/StructureStatic.lean b/Aesop/Script/StructureStatic.lean index 3d434cf52..4faaf7f90 100644 --- a/Aesop/Script/StructureStatic.lean +++ b/Aesop/Script/StructureStatic.lean @@ -1,5 +1,6 @@ module +meta import Lean.Parser.Do public import Aesop.Script.UScriptToSScript public import Aesop.Script.Util diff --git a/Aesop/Script/Tactic.lean b/Aesop/Script/Tactic.lean index e0d4849d2..ac3a45799 100644 --- a/Aesop/Script/Tactic.lean +++ b/Aesop/Script/Tactic.lean @@ -5,7 +5,8 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Lean.Meta.Basic public section diff --git a/Aesop/Script/TacticState.lean b/Aesop/Script/TacticState.lean index 28d1402da..299b0c544 100644 --- a/Aesop/Script/TacticState.lean +++ b/Aesop/Script/TacticState.lean @@ -5,7 +5,8 @@ Authors: Jannis Limperg -/ module -public import Batteries.Lean.Meta.Basic +import Lean +import Batteries.Lean.Meta.Basic public import Aesop.Script.GoalWithMVars public section diff --git a/Aesop/Script/UScript.lean b/Aesop/Script/UScript.lean index d638db983..9cca11f80 100644 --- a/Aesop/Script/UScript.lean +++ b/Aesop/Script/UScript.lean @@ -5,7 +5,9 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Script.Step +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Script/UScriptToSScript.lean b/Aesop/Script/UScriptToSScript.lean index 9195fc097..e63d65bad 100644 --- a/Aesop/Script/UScriptToSScript.lean +++ b/Aesop/Script/UScriptToSScript.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Script.UScript public import Aesop.Script.SScript public import Aesop.Tracing diff --git a/Aesop/Script/Util.lean b/Aesop/Script/Util.lean index 440276eeb..055d3c263 100644 --- a/Aesop/Script/Util.lean +++ b/Aesop/Script/Util.lean @@ -7,7 +7,7 @@ module public import Aesop.Util.Basic public import Aesop.Util.EqualUpToIds -public import Batteries.Lean.Meta.SavedState +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Search/Expansion/Basic.lean b/Aesop/Search/Expansion/Basic.lean index 801e86f22..5e6573521 100644 --- a/Aesop/Search/Expansion/Basic.lean +++ b/Aesop/Search/Expansion/Basic.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.RuleTac.Basic public section diff --git a/Aesop/Search/Expansion/Norm.lean b/Aesop/Search/Expansion/Norm.lean index 697e93ee4..941e41ae0 100644 --- a/Aesop/Search/Expansion/Norm.lean +++ b/Aesop/Search/Expansion/Norm.lean @@ -14,7 +14,8 @@ public import Aesop.Search.Expansion.Simp public import Aesop.Search.RuleSelection public import Aesop.Search.SearchM public import Aesop.Tree.State -public import Batteries.Lean.HashSet +import Batteries.Lean.HashSet +public import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Stats/Basic.lean b/Aesop/Stats/Basic.lean index db7818d44..87f70112f 100644 --- a/Aesop/Stats/Basic.lean +++ b/Aesop/Stats/Basic.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Nanos public import Aesop.Rule.Name public import Aesop.Tracing diff --git a/Aesop/Stats/Extension.lean b/Aesop/Stats/Extension.lean index 21a2ebccb..525e91c44 100644 --- a/Aesop/Stats/Extension.lean +++ b/Aesop/Stats/Extension.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Stats.Basic public section diff --git a/Aesop/Stats/File.lean b/Aesop/Stats/File.lean index f865fe503..167faca51 100644 --- a/Aesop/Stats/File.lean +++ b/Aesop/Stats/File.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Stats.Basic public import Lean.Data.Position diff --git a/Aesop/Stats/Report.lean b/Aesop/Stats/Report.lean index 0a93379d3..1cf1984b9 100644 --- a/Aesop/Stats/Report.lean +++ b/Aesop/Stats/Report.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Percent public import Aesop.Stats.Extension diff --git a/Aesop/Tracing.lean b/Aesop/Tracing.lean index 4cab9d4e3..f7b4da832 100644 --- a/Aesop/Tracing.lean +++ b/Aesop/Tracing.lean @@ -6,9 +6,9 @@ Authors: Jannis Limperg module public import Aesop.Util.Basic -public import Batteries.Data.Array.Basic public import Lean.Elab.Term public import Lean.Meta.Tactic.Simp +meta import Lean.Parser.Do public section diff --git a/Aesop/Tree/AddRapp.lean b/Aesop/Tree/AddRapp.lean index 9bda8e2c1..d20bc1ea8 100644 --- a/Aesop/Tree/AddRapp.lean +++ b/Aesop/Tree/AddRapp.lean @@ -10,6 +10,7 @@ public import Aesop.Forward.State.ApplyGoalDiff public import Aesop.Tree.Traversal public import Aesop.Tree.TreeM public import Aesop.Util.UnionFind +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Tree/Check.lean b/Aesop/Tree/Check.lean index 58a820200..537d90194 100644 --- a/Aesop/Tree/Check.lean +++ b/Aesop/Tree/Check.lean @@ -9,8 +9,9 @@ public import Aesop.Check public import Aesop.Tree.State public import Aesop.Tree.Traversal public import Aesop.Tree.TreeM -public import Batteries.Lean.HashSet public import Aesop.Tree.RunMetaM +import Batteries.Lean.HashSet +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Tree/ExtractProof.lean b/Aesop/Tree/ExtractProof.lean index e1f50da63..52a247891 100644 --- a/Aesop/Tree/ExtractProof.lean +++ b/Aesop/Tree/ExtractProof.lean @@ -8,7 +8,8 @@ module public import Lean.Replay public import Aesop.Tracing public import Aesop.Tree.TreeM -public import Batteries.Lean.Meta.InstantiateMVars +import Batteries.Lean.Meta.InstantiateMVars +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Tree/Tracing.lean b/Aesop/Tree/Tracing.lean index e51bf8827..98c1e17b9 100644 --- a/Aesop/Tree/Tracing.lean +++ b/Aesop/Tree/Tracing.lean @@ -2,6 +2,7 @@ module public import Aesop.Tree.RunMetaM public import Aesop.Tracing +import Batteries.Lean.Meta.SavedState public section diff --git a/Aesop/Tree/UnsafeQueue.lean b/Aesop/Tree/UnsafeQueue.lean index 79f26c72e..c8b09c306 100644 --- a/Aesop/Tree/UnsafeQueue.lean +++ b/Aesop/Tree/UnsafeQueue.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +meta import Lean.Parser.Do public import Aesop.Constants public import Aesop.Rule diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean index a0585ebb0..310b4f9a4 100644 --- a/Aesop/Util/Basic.lean +++ b/Aesop/Util/Basic.lean @@ -8,9 +8,11 @@ module public import Aesop.Index.DiscrTreeConfig public import Aesop.Nanos public import Aesop.Util.UnorderedArraySet -public import Batteries.Lean.Expr -public import Batteries.Data.String.Basic -public import Lean +import Lean +public import Lean.Meta.DiscrTree.Util +public import Lean.Meta.Tactic.Simp.SimpTheorems +public import Lean.Util.ForEachExpr +public import Lean.Elab.Tactic.Basic public import Std.Data.HashSet.Basic public section diff --git a/Aesop/Util/Tactic.lean b/Aesop/Util/Tactic.lean index b1e3b4956..db5aeb9ba 100644 --- a/Aesop/Util/Tactic.lean +++ b/Aesop/Util/Tactic.lean @@ -5,8 +5,8 @@ Authors: Jannis Limperg -/ module -public import Lean -public import Batteries.Tactic.OpenPrivate +import Lean +public import Lean.Meta.Basic public section diff --git a/Aesop/Util/Tactic/Ext.lean b/Aesop/Util/Tactic/Ext.lean index d8ced83d0..aee2c3c7e 100644 --- a/Aesop/Util/Tactic/Ext.lean +++ b/Aesop/Util/Tactic/Ext.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +import Lean public import Aesop.Tracing public section diff --git a/Aesop/Util/Tactic/Unfold.lean b/Aesop/Util/Tactic/Unfold.lean index 3fb6e5f9b..7081571c4 100644 --- a/Aesop/Util/Tactic/Unfold.lean +++ b/Aesop/Util/Tactic/Unfold.lean @@ -5,6 +5,7 @@ Authors: Jannis Limperg -/ module +public import Lean.Elab.Tactic.Basic public meta import Aesop.Util.Unfold public section diff --git a/Aesop/Util/Unfold.lean b/Aesop/Util/Unfold.lean index 1c86afb05..81da7b531 100644 --- a/Aesop/Util/Unfold.lean +++ b/Aesop/Util/Unfold.lean @@ -5,7 +5,8 @@ Authors: Jannis Limperg -/ module -public import Lean +import Lean +public import Lean.Meta.Tactic.Simp.Main public section From 7f1693468a9e6276b614a2cc52f77dd46fb6244a Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Wed, 22 Apr 2026 13:28:12 +1000 Subject: [PATCH 15/17] refactor: remove transitive meta import of Lean.Parser.Do (#327) Co-authored-by: Claude Opus 4.7 (1M context) --- Aesop/BaseM.lean | 1 - Aesop/Builder/Apply.lean | 1 - Aesop/Builder/Basic.lean | 1 - Aesop/Builder/Constructors.lean | 1 - Aesop/Builder/Default.lean | 1 - Aesop/Builder/Forward.lean | 1 - Aesop/Builder/NormSimp.lean | 1 - Aesop/Builder/Tactic.lean | 1 - Aesop/Builder/Unfold.lean | 1 - Aesop/EMap.lean | 1 - Aesop/Forward/Match/Types.lean | 1 - Aesop/Forward/RuleInfo.lean | 1 - Aesop/Index/Basic.lean | 1 - Aesop/Index/Forward.lean | 1 - Aesop/Index/RulePattern.lean | 1 - Aesop/Rule.lean | 1 - Aesop/Rule/Basic.lean | 1 - Aesop/Rule/Forward.lean | 1 - Aesop/RulePattern.lean | 1 - Aesop/RuleSet/Member.lean | 1 - Aesop/RuleTac/Basic.lean | 1 - Aesop/RuleTac/Descr.lean | 1 - Aesop/RuleTac/GoalDiff.lean | 1 - Aesop/RuleTac/Tactic.lean | 1 - Aesop/Script/Check.lean | 1 - Aesop/Script/Main.lean | 1 - Aesop/Script/ScriptM.lean | 1 - Aesop/Script/StructureDynamic.lean | 1 - Aesop/Script/StructureStatic.lean | 1 - Aesop/Script/UScript.lean | 1 - Aesop/Script/UScriptToSScript.lean | 1 - Aesop/Search/Expansion/Basic.lean | 1 - Aesop/Stats/Basic.lean | 1 - Aesop/Stats/Extension.lean | 1 - Aesop/Stats/File.lean | 1 - Aesop/Stats/Report.lean | 1 - Aesop/Tracing.lean | 3 +-- Aesop/Tree/UnsafeQueue.lean | 1 - 38 files changed, 1 insertion(+), 39 deletions(-) diff --git a/Aesop/BaseM.lean b/Aesop/BaseM.lean index 59d068aed..c51dc0619 100644 --- a/Aesop/BaseM.lean +++ b/Aesop/BaseM.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Stats.Basic public import Aesop.RulePattern.Cache diff --git a/Aesop/Builder/Apply.lean b/Aesop/Builder/Apply.lean index 6fc36ac49..817046225 100644 --- a/Aesop/Builder/Apply.lean +++ b/Aesop/Builder/Apply.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Builder.Basic import Batteries.Lean.Expr diff --git a/Aesop/Builder/Basic.lean b/Aesop/Builder/Basic.lean index f2d8eea38..ad6e27d8d 100644 --- a/Aesop/Builder/Basic.lean +++ b/Aesop/Builder/Basic.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.ElabM public import Aesop.Rule.Name public import Aesop.RuleSet.Member diff --git a/Aesop/Builder/Constructors.lean b/Aesop/Builder/Constructors.lean index a8d3b9088..e7a525987 100644 --- a/Aesop/Builder/Constructors.lean +++ b/Aesop/Builder/Constructors.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Builder.Basic public section diff --git a/Aesop/Builder/Default.lean b/Aesop/Builder/Default.lean index 9aad7cddc..ecc91aee2 100644 --- a/Aesop/Builder/Default.lean +++ b/Aesop/Builder/Default.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Builder.Constructors public import Aesop.Builder.NormSimp public import Aesop.Builder.Tactic diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean index 04510f6c2..83feedab1 100644 --- a/Aesop/Builder/Forward.lean +++ b/Aesop/Builder/Forward.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Builder.Basic public section diff --git a/Aesop/Builder/NormSimp.lean b/Aesop/Builder/NormSimp.lean index 3eda4f868..b04b38e17 100644 --- a/Aesop/Builder/NormSimp.lean +++ b/Aesop/Builder/NormSimp.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Builder.Basic public section diff --git a/Aesop/Builder/Tactic.lean b/Aesop/Builder/Tactic.lean index 85bbd31d2..5641f34fb 100644 --- a/Aesop/Builder/Tactic.lean +++ b/Aesop/Builder/Tactic.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Builder.Basic public section diff --git a/Aesop/Builder/Unfold.lean b/Aesop/Builder/Unfold.lean index 8df2c434a..0ef77aba9 100644 --- a/Aesop/Builder/Unfold.lean +++ b/Aesop/Builder/Unfold.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Builder.Basic public import Aesop.Util.Unfold diff --git a/Aesop/EMap.lean b/Aesop/EMap.lean index 3cafa5e42..a0940a829 100644 --- a/Aesop/EMap.lean +++ b/Aesop/EMap.lean @@ -6,7 +6,6 @@ Authors: Jannis Limperg module -meta import Lean.Parser.Do public import Aesop.Tracing public import Aesop.Util.Basic diff --git a/Aesop/Forward/Match/Types.lean b/Aesop/Forward/Match/Types.lean index cfe70533d..69750aff3 100644 --- a/Aesop/Forward/Match/Types.lean +++ b/Aesop/Forward/Match/Types.lean @@ -1,6 +1,5 @@ module -meta import Lean.Parser.Do public import Aesop.Forward.PremiseIndex public import Aesop.Forward.SlotIndex public import Aesop.Forward.Substitution diff --git a/Aesop/Forward/RuleInfo.lean b/Aesop/Forward/RuleInfo.lean index 94c3a8688..a6dcef131 100644 --- a/Aesop/Forward/RuleInfo.lean +++ b/Aesop/Forward/RuleInfo.lean @@ -5,7 +5,6 @@ Authors: Xavier Généreux, Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Forward.PremiseIndex public import Aesop.Forward.SlotIndex public import Aesop.RulePattern diff --git a/Aesop/Index/Basic.lean b/Aesop/Index/Basic.lean index 2258446d6..15d05eebe 100644 --- a/Aesop/Index/Basic.lean +++ b/Aesop/Index/Basic.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Util.Basic public import Aesop.Rule.Name public import Aesop.RulePattern diff --git a/Aesop/Index/Forward.lean b/Aesop/Index/Forward.lean index ec32d2ddd..565797c00 100644 --- a/Aesop/Index/Forward.lean +++ b/Aesop/Index/Forward.lean @@ -5,7 +5,6 @@ Authors: Xavier Généreux, Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Forward.Match.Types public import Aesop.Rule.Forward public import Aesop.Index.Basic diff --git a/Aesop/Index/RulePattern.lean b/Aesop/Index/RulePattern.lean index bf045fd04..6681ce565 100644 --- a/Aesop/Index/RulePattern.lean +++ b/Aesop/Index/RulePattern.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Index.Basic public import Aesop.Util.OrderedHashSet public import Aesop.RuleTac.GoalDiff diff --git a/Aesop/Rule.lean b/Aesop/Rule.lean index 3095d4c3c..2df2bfeda 100644 --- a/Aesop/Rule.lean +++ b/Aesop/Rule.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg, Asta Halkjær From -/ module -meta import Lean.Parser.Do public import Aesop.Rule.Basic public import Aesop.Percent diff --git a/Aesop/Rule/Basic.lean b/Aesop/Rule/Basic.lean index 0afa47e1d..2233a9002 100644 --- a/Aesop/Rule/Basic.lean +++ b/Aesop/Rule/Basic.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Index.Basic public import Aesop.Rule.Name public import Aesop.RuleTac.Basic diff --git a/Aesop/Rule/Forward.lean b/Aesop/Rule/Forward.lean index 8547ae97d..59a93eede 100644 --- a/Aesop/Rule/Forward.lean +++ b/Aesop/Rule/Forward.lean @@ -5,7 +5,6 @@ Authors: Xavier Généreux, Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Forward.RuleInfo public import Aesop.Percent public import Aesop.Rule.Name diff --git a/Aesop/RulePattern.lean b/Aesop/RulePattern.lean index d04d1380d..ec27c82c6 100644 --- a/Aesop/RulePattern.lean +++ b/Aesop/RulePattern.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Forward.Substitution public import Aesop.BaseM public import Aesop.Rule.Name diff --git a/Aesop/RuleSet/Member.lean b/Aesop/RuleSet/Member.lean index 33d704fa7..6deab9e1c 100644 --- a/Aesop/RuleSet/Member.lean +++ b/Aesop/RuleSet/Member.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Rule public import Aesop.Rule.Forward diff --git a/Aesop/RuleTac/Basic.lean b/Aesop/RuleTac/Basic.lean index 6c736b5e6..c68ea47ff 100644 --- a/Aesop/RuleTac/Basic.lean +++ b/Aesop/RuleTac/Basic.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Forward.Match.Types public import Aesop.Index.Basic public import Aesop.Percent diff --git a/Aesop/RuleTac/Descr.lean b/Aesop/RuleTac/Descr.lean index 716ebef3b..0a51f5a9e 100644 --- a/Aesop/RuleTac/Descr.lean +++ b/Aesop/RuleTac/Descr.lean @@ -1,6 +1,5 @@ module -meta import Lean.Parser.Do public import Aesop.RuleTac.Basic public import Aesop.Forward.Match.Types diff --git a/Aesop/RuleTac/GoalDiff.lean b/Aesop/RuleTac/GoalDiff.lean index 0bcf12cd2..82966013a 100644 --- a/Aesop/RuleTac/GoalDiff.lean +++ b/Aesop/RuleTac/GoalDiff.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.BaseM public import Aesop.RuleTac.FVarIdSubst public import Aesop.Util.Basic diff --git a/Aesop/RuleTac/Tactic.lean b/Aesop/RuleTac/Tactic.lean index 8596f4bad..40029a091 100644 --- a/Aesop/RuleTac/Tactic.lean +++ b/Aesop/RuleTac/Tactic.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg, Kaiyu Yang -/ module -meta import Lean.Parser.Do public import Aesop.RuleTac.Basic public import Aesop.Script.Step diff --git a/Aesop/Script/Check.lean b/Aesop/Script/Check.lean index cbbe96f82..af8d83b79 100644 --- a/Aesop/Script/Check.lean +++ b/Aesop/Script/Check.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Check public import Aesop.Script.UScript diff --git a/Aesop/Script/Main.lean b/Aesop/Script/Main.lean index 7836a6b43..f01fbae34 100644 --- a/Aesop/Script/Main.lean +++ b/Aesop/Script/Main.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Script.Check public import Aesop.Script.StructureDynamic public import Aesop.Script.StructureStatic diff --git a/Aesop/Script/ScriptM.lean b/Aesop/Script/ScriptM.lean index a9796b1b0..cbad6b7c9 100644 --- a/Aesop/Script/ScriptM.lean +++ b/Aesop/Script/ScriptM.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.BaseM public import Aesop.Script.Step public import Aesop.Script.Tactic diff --git a/Aesop/Script/StructureDynamic.lean b/Aesop/Script/StructureDynamic.lean index 5c8eb98b5..bc83dd6ec 100644 --- a/Aesop/Script/StructureDynamic.lean +++ b/Aesop/Script/StructureDynamic.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Script.UScript public import Aesop.Script.UScriptToSScript public import Aesop.Script.Util diff --git a/Aesop/Script/StructureStatic.lean b/Aesop/Script/StructureStatic.lean index 4faaf7f90..3d434cf52 100644 --- a/Aesop/Script/StructureStatic.lean +++ b/Aesop/Script/StructureStatic.lean @@ -1,6 +1,5 @@ module -meta import Lean.Parser.Do public import Aesop.Script.UScriptToSScript public import Aesop.Script.Util diff --git a/Aesop/Script/UScript.lean b/Aesop/Script/UScript.lean index 9cca11f80..91e720bbe 100644 --- a/Aesop/Script/UScript.lean +++ b/Aesop/Script/UScript.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Script.Step import Batteries.Lean.Meta.SavedState diff --git a/Aesop/Script/UScriptToSScript.lean b/Aesop/Script/UScriptToSScript.lean index e63d65bad..9195fc097 100644 --- a/Aesop/Script/UScriptToSScript.lean +++ b/Aesop/Script/UScriptToSScript.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Script.UScript public import Aesop.Script.SScript public import Aesop.Tracing diff --git a/Aesop/Search/Expansion/Basic.lean b/Aesop/Search/Expansion/Basic.lean index 5e6573521..801e86f22 100644 --- a/Aesop/Search/Expansion/Basic.lean +++ b/Aesop/Search/Expansion/Basic.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.RuleTac.Basic public section diff --git a/Aesop/Stats/Basic.lean b/Aesop/Stats/Basic.lean index 87f70112f..db7818d44 100644 --- a/Aesop/Stats/Basic.lean +++ b/Aesop/Stats/Basic.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Nanos public import Aesop.Rule.Name public import Aesop.Tracing diff --git a/Aesop/Stats/Extension.lean b/Aesop/Stats/Extension.lean index 525e91c44..21a2ebccb 100644 --- a/Aesop/Stats/Extension.lean +++ b/Aesop/Stats/Extension.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Stats.Basic public section diff --git a/Aesop/Stats/File.lean b/Aesop/Stats/File.lean index 167faca51..f865fe503 100644 --- a/Aesop/Stats/File.lean +++ b/Aesop/Stats/File.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Stats.Basic public import Lean.Data.Position diff --git a/Aesop/Stats/Report.lean b/Aesop/Stats/Report.lean index 1cf1984b9..0a93379d3 100644 --- a/Aesop/Stats/Report.lean +++ b/Aesop/Stats/Report.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Percent public import Aesop.Stats.Extension diff --git a/Aesop/Tracing.lean b/Aesop/Tracing.lean index f7b4da832..ec9f4556e 100644 --- a/Aesop/Tracing.lean +++ b/Aesop/Tracing.lean @@ -8,7 +8,6 @@ module public import Aesop.Util.Basic public import Lean.Elab.Term public import Lean.Meta.Tactic.Simp -meta import Lean.Parser.Do public section @@ -110,7 +109,7 @@ macro "aesop_trace![" opt:ident "] " msg:(interpolatedStr(term) <|> term) : `(doElem| Lean.addTrace (Aesop.TraceOption.traceClass $opt) $msg) macro "aesop_trace[" opt:ident "] " - msg:(interpolatedStr(term) <|> Parser.Term.do <|> term) : doElem => do + msg:(interpolatedStr(term) <|> term) : doElem => do let msg := msg.raw let opt ← mkIdent <$> resolveTraceOption opt match msg with diff --git a/Aesop/Tree/UnsafeQueue.lean b/Aesop/Tree/UnsafeQueue.lean index c8b09c306..79f26c72e 100644 --- a/Aesop/Tree/UnsafeQueue.lean +++ b/Aesop/Tree/UnsafeQueue.lean @@ -5,7 +5,6 @@ Authors: Jannis Limperg -/ module -meta import Lean.Parser.Do public import Aesop.Constants public import Aesop.Rule From 558915ae105bfd8074e22d597613d1961822adc2 Mon Sep 17 00:00:00 2001 From: Garmelon Date: Tue, 26 May 2026 16:18:50 +0100 Subject: [PATCH 16/17] chore: bump toolchain to v4.30.0 (#328) --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 67b8ed581..f2bae4b6a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", + "rev": "32dc18cde3684679f3c003de608743b57498c56f", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "v4.30.0", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index 4e3f80798..84f1816eb 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,7 @@ platformIndependent = true [[require]] name = "batteries" scope = "leanprover-community" -rev = "v4.30.0-rc2" +rev = "v4.30.0" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index 6c7e31fff..af9e5d339 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0-rc2 +leanprover/lean4:v4.30.0 From fafca80479ff95e041d84373dda7122adf1295f2 Mon Sep 17 00:00:00 2001 From: Garmelon Date: Thu, 28 May 2026 17:38:44 +0100 Subject: [PATCH 17/17] chore: bump toolchain to v4.31.0-rc1 (#329) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Kim Morrison Co-authored-by: Jannis Limperg Co-authored-by: Kyle Miller Co-authored-by: Sebastian Ullrich Co-authored-by: Jannis Limperg Co-authored-by: Anne C.A. Baanen Co-authored-by: Marc Huisinga Co-authored-by: Markus Himmel Co-authored-by: Joachim Breitner Co-authored-by: Claude Opus 4.5 Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Wojciech Różowski --- Aesop/Util/Basic.lean | 2 +- Aesop/Util/EqualUpToIds.lean | 2 +- AesopTest/IncompleteScript.lean | 1 - AesopTest/List.lean | 2 +- AesopTest/SafePrefixExpansionRappLimit.lean | 2 -- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- lean_packages/std | 1 + 9 files changed, 8 insertions(+), 10 deletions(-) create mode 160000 lean_packages/std diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean index 310b4f9a4..f8e2c3b96 100644 --- a/Aesop/Util/Basic.lean +++ b/Aesop/Util/Basic.lean @@ -451,7 +451,7 @@ where (acc, lctx) dummyLDecl (name : Name) : LocalDecl := - .cdecl 0 ⟨`_⟩ name (.sort Level.zero) .default .default + .cdecl 0 ⟨`_⟩ name (.sort .zero) .default .default def Name.ofComponents (cs : List Name) : Name := cs.foldl (init := .anonymous) λ diff --git a/Aesop/Util/EqualUpToIds.lean b/Aesop/Util/EqualUpToIds.lean index 2acf719da..0a2c96db4 100644 --- a/Aesop/Util/EqualUpToIds.lean +++ b/Aesop/Util/EqualUpToIds.lean @@ -87,7 +87,7 @@ def equalCommonLMVars? (lmvarId₁ lmvarId₂ : LMVarId) : match ← readCommonMCtx? with | none => return none | some mctx => - if mctx.lDepth.contains lmvarId₁ || mctx.lDepth.contains lmvarId₂ then + if mctx.lDecls.contains lmvarId₁ || mctx.lDecls.contains lmvarId₂ then return some $ lmvarId₁ == lmvarId₂ else return none diff --git a/AesopTest/IncompleteScript.lean b/AesopTest/IncompleteScript.lean index 38d814372..bf34238d1 100644 --- a/AesopTest/IncompleteScript.lean +++ b/AesopTest/IncompleteScript.lean @@ -57,7 +57,6 @@ info: Try this: warning: aesop: failed to prove the goal after exhaustive search. --- error: unsolved goals -case a.a ⊢ Even 1 -/ #guard_msgs in diff --git a/AesopTest/List.lean b/AesopTest/List.lean index 5963d9032..f1856ebb2 100644 --- a/AesopTest/List.lean +++ b/AesopTest/List.lean @@ -178,7 +178,7 @@ theorem subset_trans {l₁ l₂ l₃ : List α} : l₁ ⊆ l₂ → l₂ ⊆ l -- END PRELUDE -instance unique_of_is_empty [IsEmpty α] : Unique (List α) := by +def unique_of_is_empty [IsEmpty α] : Unique (List α) := by aesop (add 1% cases List) -- instance : is_left_id (list α) has_append.append [] := diff --git a/AesopTest/SafePrefixExpansionRappLimit.lean b/AesopTest/SafePrefixExpansionRappLimit.lean index b8a4e82be..3dd6927de 100644 --- a/AesopTest/SafePrefixExpansionRappLimit.lean +++ b/AesopTest/SafePrefixExpansionRappLimit.lean @@ -15,7 +15,6 @@ warning: aesop: failed to prove the goal. Some goals were not explored because t warning: aesop: safe prefix was not fully expanded because the maximum number of rule applications (50) was reached. --- error: unsolved goals -case a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a ⊢ False -/ #guard_msgs in @@ -27,7 +26,6 @@ error: tactic 'aesop' failed, failed to prove the goal. Some goals were not expl Initial goal: ⊢ False Remaining goals after safe rules: - case a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a.a ⊢ False The safe prefix was not fully expanded because the maximum number of rule applications (50) was reached. -/ diff --git a/lake-manifest.json b/lake-manifest.json index f2bae4b6a..99eddc844 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "32dc18cde3684679f3c003de608743b57498c56f", + "rev": "708b057842c4cd0845fba132bd94b08493f6fc42", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", + "inputRev": "v4.31.0-rc1", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index 84f1816eb..dba0fef22 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -7,7 +7,7 @@ platformIndependent = true [[require]] name = "batteries" scope = "leanprover-community" -rev = "v4.30.0" +rev = "v4.31.0-rc1" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index af9e5d339..8c7e931aa 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0 +leanprover/lean4:v4.31.0-rc1 diff --git a/lean_packages/std b/lean_packages/std new file mode 160000 index 000000000..c2130e653 --- /dev/null +++ b/lean_packages/std @@ -0,0 +1 @@ +Subproject commit c2130e653bc1057f8f21196a9b89987d84fe247b