From 39119d25ce6f40a6250b742c6b4e8d9b400af677 Mon Sep 17 00:00:00 2001 From: Jannis Limperg Date: Tue, 12 Nov 2024 20:18:02 +0100 Subject: [PATCH 01/10] RuleTactic.Tactic: disable recovery (#178) --- Aesop/RuleTac/Tactic.lean | 10 +++--- AesopTest/BigStep.lean | 69 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 74 insertions(+), 5 deletions(-) create mode 100644 AesopTest/BigStep.lean diff --git a/Aesop/RuleTac/Tactic.lean b/Aesop/RuleTac/Tactic.lean index a82f14bd..c8fb374a 100644 --- a/Aesop/RuleTac/Tactic.lean +++ b/Aesop/RuleTac/Tactic.lean @@ -7,9 +7,8 @@ Authors: Jannis Limperg, Kaiyu Yang import Aesop.RuleTac.Basic import Aesop.Script.Step -open Lean -open Lean.Meta -open Lean.Elab.Tactic (TacticM evalTactic run) +open Lean Lean.Meta Lean.Elab.Tactic +open Lean.Elab.Tactic (TacticM evalTactic withoutRecover) namespace Aesop.RuleTac @@ -17,7 +16,7 @@ namespace Aesop.RuleTac unsafe def tacticMImpl (decl : Name) : RuleTac := SingleRuleTac.toRuleTac λ input => do let tac ← evalConst (TacticM Unit) decl - let goals ← run input.goal tac |>.run' + let goals ← Elab.Tactic.run input.goal tac |>.run' let goals ← goals.mapM (mvarIdToSubgoal (parentMVarId := input.goal) · ∅) return (goals.toArray, none, none) @@ -51,7 +50,8 @@ kind `tactic` or `tacticSeq`. def tacticStx (stx : Syntax) : RuleTac := SingleRuleTac.toRuleTac λ input => do let preState ← saveState - let postGoals := (← run input.goal (evalTactic stx) |>.run').toArray + let tac := withoutRecover $ evalTactic stx + let postGoals := (← Elab.Tactic.run input.goal tac |>.run').toArray let postState ← saveState let tacticBuilder : Script.TacticBuilder := do if stx.isOfKind `tactic then diff --git a/AesopTest/BigStep.lean b/AesopTest/BigStep.lean new file mode 100644 index 00000000..ab210060 --- /dev/null +++ b/AesopTest/BigStep.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2024 Asei Inoue. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Asei Inoue, Jannis Limperg +-/ + +import Aesop + +set_option aesop.check.all true + +abbrev Variable := String + +def State := Variable → Nat + +inductive Stmt : Type where + | skip : Stmt + | assign : Variable → (State → Nat) → Stmt + | seq : Stmt → Stmt → Stmt + | ifThenElse : (State → Prop) → Stmt → Stmt → Stmt + | whileDo : (State → Prop) → Stmt → Stmt + +infix:60 ";; " => Stmt.seq + +export Stmt (skip assign seq ifThenElse whileDo) + +set_option quotPrecheck false in +notation s:70 "[" x:70 "↦" n:70 "]" => (fun v ↦ if v = x then n else s v) + +inductive BigStep : Stmt → State → State → Prop where + | protected skip (s : State) : BigStep skip s s + | protected assign (x : Variable) (a : State → Nat) (s : State) : BigStep (assign x a) s (s[x ↦ a s]) + | protected seq {S T : Stmt} {s t u : State} (hS : BigStep S s t) (hT : BigStep T t u) : + BigStep (S;; T) s u + | protected if_true {B : State → Prop} {s t : State} (hcond : B s) (S T : Stmt) (hbody : BigStep S s t) : + BigStep (ifThenElse B S T) s t + | protected if_false {B : State → Prop} {s t : State} (hcond : ¬ B s) (S T : Stmt) (hbody : BigStep T s t) : + BigStep (ifThenElse B S T) s t + | while_true {B S s t u} (hcond : B s) (hbody : BigStep S s t) (hrest : BigStep (whileDo B S) t u) : + BigStep (whileDo B S) s u + | while_false {B S s} (hcond : ¬ B s) : BigStep (whileDo B S) s s + +notation:55 "(" S:55 "," s:55 ")" " ==> " t:55 => BigStep S s t + +add_aesop_rules safe [BigStep.skip, BigStep.assign, BigStep.seq, BigStep.while_false] +add_aesop_rules 50% [apply BigStep.while_true] +add_aesop_rules safe [ + (by apply BigStep.if_true (hcond := by assumption) (hbody := by assumption)), + (by apply BigStep.if_false (hcond := by assumption) (hbody := by assumption)) +] + +namespace BigStep + +@[aesop safe destruct] +theorem cases_if_of_true {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by + intro h; cases h <;> aesop + +@[aesop safe destruct] +theorem cases_if_of_false {B S T s t} (hcond : ¬ B s) : (ifThenElse B S T, s) ==> t → (T, s) ==> t := by + intro h; cases h <;> aesop + +@[aesop 30%] +theorem and_excluded {P Q R : Prop} (hQ : P → Q) (hR : ¬ P → R) : (P ∧ Q ∨ ¬ P ∧ R) := by + by_cases h : P <;> aesop + +theorem if_iff {B S T s t} : (ifThenElse B S T, s) ==> t ↔ + (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := by + aesop + +end BigStep From de91b59101763419997026c35a41432ac8691f15 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 14 Nov 2024 13:55:40 +1100 Subject: [PATCH 02/10] chore: bump batteries, follow deprecations (#179) --- Aesop/Util/Basic.lean | 2 +- lake-manifest.json | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean index 8490ad46..233353ab 100644 --- a/Aesop/Util/Basic.lean +++ b/Aesop/Util/Basic.lean @@ -89,7 +89,7 @@ def getConclusionDiscrTreeKeys (type : Expr) (config : WhnfCoreConfig) : -- For a constant `d` with type `∀ (x₁, ..., xₙ), T`, returns keys that -- match `d * ... *` (with `n` stars). def getConstDiscrTreeKeys (decl : Name) : MetaM (Array Key) := do - let arity := (← getConstInfo decl).type.forallArity + let arity := (← getConstInfo decl).type.getNumHeadForalls let mut keys := Array.mkEmpty (arity + 1) keys := keys.push $ .const decl arity for _ in [0:arity] do diff --git a/lake-manifest.json b/lake-manifest.json index 84657908..49184961 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "76e9ebe4176d29cb9cc89c669ab9f1ce32b33c3d", + "rev": "b100ff2565805e9f30a482788b3fc66937a7f38a", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", From 5a0ec8588855265ade536f35bcdcf0fb24fd6030 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 2 Dec 2024 11:22:28 +1100 Subject: [PATCH 03/10] chore: bump toolchain to v4.14.0 (#180) --- 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 49184961..aca2ee30 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b100ff2565805e9f30a482788b3fc66937a7f38a", + "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.14.0", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index 96a10fd8..0ec77807 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,7 +6,7 @@ precompileModules = false # We would like to turn this on, but it breaks the Mat [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "main" +rev = "v4.14.0" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index 57a4710c..1e70935f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0-rc2 +leanprover/lean4:v4.14.0 From 8b6048aa0a4a4b6bcf83597802d8dee734e64b7e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 2 Dec 2024 14:06:45 +1100 Subject: [PATCH 04/10] chore: bump toolchain to v4.15.0-rc1 and merge changes from nightly-testing (#181) Co-authored-by: Jannis Limperg Co-authored-by: Kyle Miller --- Aesop/Builder/Cases.lean | 2 +- Aesop/Builder/Forward.lean | 2 +- Aesop/Frontend/RuleExpr.lean | 2 +- Aesop/Index.lean | 4 ++-- Aesop/Index/Basic.lean | 2 +- Aesop/RuleSet.lean | 4 ++-- Aesop/RuleTac/ElabRuleTerm.lean | 2 +- Aesop/RuleTac/Forward.lean | 2 +- Aesop/Search/Expansion/Simp.lean | 6 +++--- Aesop/Search/SearchM.lean | 9 ++++----- Aesop/Tree/TreeM.lean | 2 +- Aesop/Util/Basic.lean | 6 +++--- Aesop/Util/Tactic/Unfold.lean | 7 +------ AesopTest/SaturatePerformance.lean | 8 ++++---- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 17 files changed, 30 insertions(+), 36 deletions(-) diff --git a/Aesop/Builder/Cases.lean b/Aesop/Builder/Cases.lean index 914bae91..e45a4056 100644 --- a/Aesop/Builder/Cases.lean +++ b/Aesop/Builder/Cases.lean @@ -22,7 +22,7 @@ def check (decl : Name) (p : CasesPattern) : MetaM Unit := def toIndexingMode (p : CasesPattern) : MetaM IndexingMode := withoutModifyingState do - .hyps <$> DiscrTree.mkPath (← p.toExpr) discrTreeConfig + .hyps <$> (withConfigWithKey discrTreeConfig <| DiscrTree.mkPath (← p.toExpr)) end CasesPattern diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean index def5c30b..b7e8c6d5 100644 --- a/Aesop/Builder/Forward.lean +++ b/Aesop/Builder/Forward.lean @@ -34,7 +34,7 @@ private def forwardIndexingModeCore (type : Expr) match args.get? i with | some arg => let argT := (← arg.mvarId!.getDecl).type - let keys ← DiscrTree.mkPath argT discrTreeConfig + let keys ← withConfigWithKey discrTreeConfig <| DiscrTree.mkPath argT return .hyps keys | none => throwError "aesop: internal error: immediate arg for forward rule is out of range" diff --git a/Aesop/Frontend/RuleExpr.lean b/Aesop/Frontend/RuleExpr.lean index 1cc31699..63b837ab 100644 --- a/Aesop/Frontend/RuleExpr.lean +++ b/Aesop/Frontend/RuleExpr.lean @@ -173,7 +173,7 @@ def elabSingleIndexingMode (stx : Syntax) : ElabM IndexingMode := elabKeys (stx : Syntax) : ElabM (Array DiscrTree.Key) := show TermElabM _ from withoutModifyingState do let e ← elabPattern stx - DiscrTree.mkPath (← instantiateMVars e) discrTreeConfig + withConfigWithKey discrTreeConfig <| DiscrTree.mkPath (← instantiateMVars e) def IndexingMode.elab (stxs : Array Syntax) : ElabM IndexingMode := .or <$> stxs.mapM elabSingleIndexingMode diff --git a/Aesop/Index.lean b/Aesop/Index.lean index b0256dc7..65c10dd5 100644 --- a/Aesop/Index.lean +++ b/Aesop/Index.lean @@ -96,7 +96,7 @@ private def applicableByTargetRules (ri : Index α) (goal : MVarId) (include? : Rule α → Bool) : MetaM (Array (Rule α × Array IndexMatchLocation)) := goal.withContext do - let rules ← ri.byTarget.getUnify (← goal.getType) discrTreeConfig + let rules ← withConfigWithKey discrTreeConfig <| ri.byTarget.getUnify (← goal.getType) let mut rs := Array.mkEmpty rules.size -- Assumption: include? is true for most rules. for r in rules do @@ -114,7 +114,7 @@ private def applicableByHypRules (ri : Index α) (goal : MVarId) for localDecl in ← getLCtx do if localDecl.isImplementationDetail then continue - let rules ← ri.byHyp.getUnify localDecl.type discrTreeConfig + let rules ← withConfigWithKey discrTreeConfig <| ri.byHyp.getUnify localDecl.type for r in rules do if include? r then rs := rs.push (r, #[.hyp localDecl]) diff --git a/Aesop/Index/Basic.lean b/Aesop/Index/Basic.lean index a1a65a1d..30889103 100644 --- a/Aesop/Index/Basic.lean +++ b/Aesop/Index/Basic.lean @@ -14,7 +14,7 @@ namespace Aesop -- This value controls whether we use 'powerful' reductions, e.g. iota, when -- indexing Aesop rules. See the `DiscrTree` docs for details. -def discrTreeConfig : WhnfCoreConfig := { iota := false } +def discrTreeConfig : ConfigWithKey := { iota := false : Config}.toConfigWithKey inductive IndexingMode : Type | unindexed diff --git a/Aesop/RuleSet.lean b/Aesop/RuleSet.lean index ec689567..82bec298 100644 --- a/Aesop/RuleSet.lean +++ b/Aesop/RuleSet.lean @@ -367,7 +367,7 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) : Σ' a : Array (Name × SimpTheorems), a.size = rs.simpTheoremsArray.size := ⟨rs.simpTheoremsArray, rfl⟩ if let some id := f.matchesLocalNormSimpRule? then - if let some idx := localNormSimpRules.findIdx? (·.id == id) then + if let some idx := localNormSimpRules.findFinIdx? (·.id == id) then localNormSimpRules := localNormSimpRules.eraseIdx idx if let some decl := f.matchesSimpTheorem? then for h : i in [:rs.simpTheoremsArray.size] do @@ -377,7 +377,7 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) : if SimpTheorems.containsDecl simpTheorems decl then let origin := .decl decl (inv := false) simpTheoremsArray' := - ⟨simpTheoremsArray'.fst.set ⟨i, i_valid⟩ + ⟨simpTheoremsArray'.fst.set i (name, simpTheorems.eraseCore origin), by simp [simpTheoremsArray'.snd, Array.size_set]⟩ anyErased := true diff --git a/Aesop/RuleTac/ElabRuleTerm.lean b/Aesop/RuleTac/ElabRuleTerm.lean index e4aacc99..8ea79f1e 100644 --- a/Aesop/RuleTac/ElabRuleTerm.lean +++ b/Aesop/RuleTac/ElabRuleTerm.lean @@ -81,7 +81,7 @@ def elabRuleTermForSimpCore (goal : MVarId) (term : Term) (ctx : Simp.Context) elabSimpTheorems (mkSimpArgs term) ctx simprocs isSimpAll def checkElabRuleTermForSimp (term : Term) (isSimpAll : Bool) : ElabM Unit := do - let ctx := { simpTheorems := #[{}] } + let ctx ← Simp.mkContext (simpTheorems := #[{}] ) let simprocs := #[{}] discard $ elabRuleTermForSimpCore (← read).goal term ctx simprocs isSimpAll diff --git a/Aesop/RuleTac/Forward.lean b/Aesop/RuleTac/Forward.lean index 34d113fe..5c7cfc4c 100644 --- a/Aesop/RuleTac/Forward.lean +++ b/Aesop/RuleTac/Forward.lean @@ -50,7 +50,7 @@ partial def makeForwardHyps (e : Expr) (pat? : Option RulePattern) (proofTypesAcc : Std.HashSet Expr) : MetaM (Array (Expr × Nat) × Array FVarId × Std.HashSet Expr) := do if h : i < immediateMVars.size then - let mvarId := immediateMVars.get ⟨i, h⟩ + let mvarId := immediateMVars[i] let type ← mvarId.getType (← getLCtx).foldlM (init := (proofsAcc, usedHypsAcc, proofTypesAcc)) λ s@(proofsAcc, usedHypsAcc, proofTypesAcc) ldecl => do if ldecl.isImplementationDetail then diff --git a/Aesop/Search/Expansion/Simp.lean b/Aesop/Search/Expansion/Simp.lean index 5c0d6582..2e56133c 100644 --- a/Aesop/Search/Expansion/Simp.lean +++ b/Aesop/Search/Expansion/Simp.lean @@ -44,7 +44,7 @@ def addLetDeclsToSimpTheorems (ctx : Simp.Context) : MetaM Simp.Context := do if ldecl.hasValue && ! ldecl.isImplementationDetail then simpTheoremsArray := simpTheoremsArray.modify 0 λ simpTheorems => simpTheorems.addLetDeclToUnfold ldecl.fvarId - return { ctx with simpTheorems := simpTheoremsArray } + return ctx.setSimpTheorems simpTheoremsArray def addLetDeclsToSimpTheoremsUnlessZetaDelta (ctx : Simp.Context) : MetaM Simp.Context := do @@ -58,7 +58,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (stats : Simp.Stats := {}) : MetaM SimpResult := do let mvarIdOld := mvarId - let ctx := { ctx with config.failIfUnchanged := false } + let ctx := ctx.setFailIfUnchanged false let (result, { usedTheorems := usedSimps, .. }) ← Meta.simpGoal mvarId ctx simprocs discharge? simplifyTarget fvarIdsToSimp stats @@ -89,7 +89,7 @@ def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (stats : Simp.Stats := {}) : MetaM SimpResult := mvarId.withContext do - let ctx := { ctx with config.failIfUnchanged := false } + let ctx := ctx.setFailIfUnchanged false let ctx ← addLetDeclsToSimpTheoremsUnlessZetaDelta ctx match ← Lean.Meta.simpAll mvarId ctx simprocs stats with | (none, stats) => return .solved stats.usedTheorems diff --git a/Aesop/Search/SearchM.lean b/Aesop/Search/SearchM.lean index 4c0884b8..ba803bf9 100644 --- a/Aesop/Search/SearchM.lean +++ b/Aesop/Search/SearchM.lean @@ -15,7 +15,8 @@ open Lean.Meta namespace Aesop -structure NormSimpContext extends Simp.Context where +structure NormSimpContext where + toContext : Simp.Context enabled : Bool useHyps : Bool configStx? : Option Term @@ -83,10 +84,8 @@ protected def run (ruleSet : LocalRuleSet) (options : Aesop.Options') MetaM (α × State Q × Tree × Stats) := do let t ← mkInitialTree goal let normSimpContext := { - config := simpConfig - maxDischargeDepth := UInt32.ofNatTruncate simpConfig.maxDischargeDepth - simpTheorems := ruleSet.simpTheoremsArray.map (·.snd) - congrTheorems := ← getSimpCongrTheorems + toContext := ← Simp.mkContext simpConfig (simpTheorems := ruleSet.simpTheoremsArray.map (·.snd)) + (congrTheorems := ← getSimpCongrTheorems) simprocs := ruleSet.simprocsArray.map (·.snd) configStx? := simpConfigStx? enabled := options.enableSimp diff --git a/Aesop/Tree/TreeM.lean b/Aesop/Tree/TreeM.lean index 693f8937..dbf476a2 100644 --- a/Aesop/Tree/TreeM.lean +++ b/Aesop/Tree/TreeM.lean @@ -92,7 +92,7 @@ def getRootGoal : TreeM GoalRef := do let cref ← getRootMVarCluster let grefs := (← cref.get).goals if h : grefs.size = 1 then - return grefs.get ⟨0, by simp [h]⟩ + return grefs[0] else throwError "aesop: internal error: unexpected number of goals in root mvar cluster: {grefs.size}" diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean index 233353ab..fac2c16f 100644 --- a/Aesop/Util/Basic.lean +++ b/Aesop/Util/Basic.lean @@ -78,11 +78,11 @@ open DiscrTree -- For `type = ∀ (x₁, ..., xₙ), T`, returns keys that match `T * ... *` (with -- `n` stars). -def getConclusionDiscrTreeKeys (type : Expr) (config : WhnfCoreConfig) : +def getConclusionDiscrTreeKeys (type : Expr) (config : ConfigWithKey) : MetaM (Array Key) := withoutModifyingState do let (_, _, conclusion) ← forallMetaTelescope type - mkPath conclusion config + withConfigWithKey config <| mkPath conclusion -- We use a meta telescope because `DiscrTree.mkPath` ignores metas (they -- turn into `Key.star`) but not fvars. @@ -117,7 +117,7 @@ private partial def filterTrieM [Monad m] [Inhabited σ] (f : σ → α → m σ if h : i < children.size then let (key, t) := children[i]'h let (t, acc) ← filterTrieM f p acc t - go acc (i + 1) (children.set ⟨i, h⟩ (key, t)) + go acc (i + 1) (children.set i (key, t)) else return (children, acc) diff --git a/Aesop/Util/Tactic/Unfold.lean b/Aesop/Util/Tactic/Unfold.lean index 0b1b15c1..2183355a 100644 --- a/Aesop/Util/Tactic/Unfold.lean +++ b/Aesop/Util/Tactic/Unfold.lean @@ -14,12 +14,7 @@ namespace Aesop -- Lean.Meta.unfoldLocalDecl. def mkUnfoldSimpContext : MetaM Simp.Context := do - return { - simpTheorems := #[] - congrTheorems := ← getSimpCongrTheorems - config := Simp.neutralConfig - dischargeDepth := 0 - } + Simp.mkContext Simp.neutralConfig (simpTheorems := #[]) (congrTheorems := ← getSimpCongrTheorems) @[inline] def unfoldManyCore (ctx : Simp.Context) (unfold? : Name → Option (Option Name)) diff --git a/AesopTest/SaturatePerformance.lean b/AesopTest/SaturatePerformance.lean index 6c8011a9..b57ad042 100644 --- a/AesopTest/SaturatePerformance.lean +++ b/AesopTest/SaturatePerformance.lean @@ -41,11 +41,11 @@ import Aesop error: unsolved goals α : Type u_1 l0 l1 l2 : List α -fwd : (l0 ++ l1 ++ l2).length ≥ 0 -fwd_1 : l0.length ≥ 0 +fwd : (l0 ++ l1).length ≥ 0 +fwd_1 : (l0 ++ l1 ++ l2).length ≥ 0 fwd_2 : l2.length ≥ 0 -fwd_3 : l1.length ≥ 0 -fwd_4 : (l0 ++ l1).length ≥ 0 +fwd_3 : l0.length ≥ 0 +fwd_4 : l1.length ≥ 0 ⊢ (l0 ++ l1 ++ l2).length = l0.length + l1.length + l2.length -/ #guard_msgs in diff --git a/lake-manifest.json b/lake-manifest.json index aca2ee30..8f13f997 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9", + "rev": "7805acf1864ba1a2e359f86a8f092ccf1438ad83", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "v4.15.0-rc1", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index 0ec77807..c47b9238 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,7 +6,7 @@ precompileModules = false # We would like to turn this on, but it breaks the Mat [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.14.0" +rev = "v4.15.0-rc1" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index 1e70935f..cf25a981 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0 +leanprover/lean4:v4.15.0-rc1 From 1c1c651a7d523d9d8aa0ebd8a3222d710d0233cc Mon Sep 17 00:00:00 2001 From: Jannis Limperg Date: Thu, 5 Dec 2024 12:39:09 +0100 Subject: [PATCH 05/10] Fix segfault triggered by codegen bug (#183) --- Aesop/Frontend/RuleExpr.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Aesop/Frontend/RuleExpr.lean b/Aesop/Frontend/RuleExpr.lean index 63b837ab..22db05ab 100644 --- a/Aesop/Frontend/RuleExpr.lean +++ b/Aesop/Frontend/RuleExpr.lean @@ -315,6 +315,8 @@ inductive Feature namespace Feature +-- Workaround for codegen bug, see #182 +set_option compiler.extract_closed false in partial def «elab» (stx : Syntax) : ElabM Feature := withRef stx do match stx with @@ -330,7 +332,7 @@ partial def «elab» (stx : Syntax) : ElabM Feature := let nonIdentAlts := stx.getArgs.filter λ stx => ! stx.isOfKind ``Parser.featIdent if h : nonIdentAlts.size = 1 then - return ← «elab» $ nonIdentAlts[0]'(by simp [h]) + return ← «elab» $ nonIdentAlts[0] throwUnsupportedSyntax end Feature From 43bcb1964528411e47bfa4edd0c87d1face1fce4 Mon Sep 17 00:00:00 2001 From: Jannis Limperg Date: Thu, 5 Dec 2024 15:23:53 +0100 Subject: [PATCH 06/10] Use same DiscrTree config as simp for indexes (#184) --- Aesop/Builder/Cases.lean | 3 +-- Aesop/Builder/Forward.lean | 2 +- Aesop/Frontend/RuleExpr.lean | 3 +-- Aesop/Index.lean | 4 ++-- Aesop/Index/Basic.lean | 2 +- Aesop/Index/DiscrKeyConfig.lean | 28 ++++++++++++++++++++++++++++ Aesop/Index/DiscrTreeConfig.lean | 28 ++++++++++++++++++++++++++++ Aesop/Util/Basic.lean | 6 +++--- 8 files changed, 65 insertions(+), 11 deletions(-) create mode 100644 Aesop/Index/DiscrKeyConfig.lean create mode 100644 Aesop/Index/DiscrTreeConfig.lean diff --git a/Aesop/Builder/Cases.lean b/Aesop/Builder/Cases.lean index e45a4056..fcd5621a 100644 --- a/Aesop/Builder/Cases.lean +++ b/Aesop/Builder/Cases.lean @@ -21,8 +21,7 @@ def check (decl : Name) (p : CasesPattern) : MetaM Unit := throwError "expected pattern '{p}' ({toString p}) to be an application of '{decl}'" def toIndexingMode (p : CasesPattern) : MetaM IndexingMode := - withoutModifyingState do - .hyps <$> (withConfigWithKey discrTreeConfig <| DiscrTree.mkPath (← p.toExpr)) + withoutModifyingState do .hyps <$> mkDiscrTreePath (← p.toExpr) end CasesPattern diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean index b7e8c6d5..16b041d0 100644 --- a/Aesop/Builder/Forward.lean +++ b/Aesop/Builder/Forward.lean @@ -34,7 +34,7 @@ private def forwardIndexingModeCore (type : Expr) match args.get? i with | some arg => let argT := (← arg.mvarId!.getDecl).type - let keys ← withConfigWithKey discrTreeConfig <| DiscrTree.mkPath argT + let keys ← mkDiscrTreePath argT return .hyps keys | none => throwError "aesop: internal error: immediate arg for forward rule is out of range" diff --git a/Aesop/Frontend/RuleExpr.lean b/Aesop/Frontend/RuleExpr.lean index 22db05ab..9e0b90b1 100644 --- a/Aesop/Frontend/RuleExpr.lean +++ b/Aesop/Frontend/RuleExpr.lean @@ -172,8 +172,7 @@ def elabSingleIndexingMode (stx : Syntax) : ElabM IndexingMode := where elabKeys (stx : Syntax) : ElabM (Array DiscrTree.Key) := show TermElabM _ from withoutModifyingState do - let e ← elabPattern stx - withConfigWithKey discrTreeConfig <| DiscrTree.mkPath (← instantiateMVars e) + mkDiscrTreePath (← elabPattern stx) def IndexingMode.elab (stxs : Array Syntax) : ElabM IndexingMode := .or <$> stxs.mapM elabSingleIndexingMode diff --git a/Aesop/Index.lean b/Aesop/Index.lean index 65c10dd5..42233197 100644 --- a/Aesop/Index.lean +++ b/Aesop/Index.lean @@ -96,7 +96,7 @@ private def applicableByTargetRules (ri : Index α) (goal : MVarId) (include? : Rule α → Bool) : MetaM (Array (Rule α × Array IndexMatchLocation)) := goal.withContext do - let rules ← withConfigWithKey discrTreeConfig <| ri.byTarget.getUnify (← goal.getType) + let rules ← getUnify ri.byTarget (← goal.getType) let mut rs := Array.mkEmpty rules.size -- Assumption: include? is true for most rules. for r in rules do @@ -114,7 +114,7 @@ private def applicableByHypRules (ri : Index α) (goal : MVarId) for localDecl in ← getLCtx do if localDecl.isImplementationDetail then continue - let rules ← withConfigWithKey discrTreeConfig <| ri.byHyp.getUnify localDecl.type + let rules ← getUnify ri.byHyp localDecl.type for r in rules do if include? r then rs := rs.push (r, #[.hyp localDecl]) diff --git a/Aesop/Index/Basic.lean b/Aesop/Index/Basic.lean index 30889103..2ae77e1f 100644 --- a/Aesop/Index/Basic.lean +++ b/Aesop/Index/Basic.lean @@ -35,7 +35,7 @@ instance : ToFormat IndexingMode := ⟨IndexingMode.format⟩ def targetMatchingConclusion (type : Expr) : MetaM IndexingMode := do - let path ← getConclusionDiscrTreeKeys type discrTreeConfig + let path ← getConclusionDiscrTreeKeys type return target path def hypsMatchingConst (decl : Name) : MetaM IndexingMode := do diff --git a/Aesop/Index/DiscrKeyConfig.lean b/Aesop/Index/DiscrKeyConfig.lean new file mode 100644 index 00000000..fc73bd63 --- /dev/null +++ b/Aesop/Index/DiscrKeyConfig.lean @@ -0,0 +1,28 @@ +/- +Copyright (c) 2024 Jannis Limperg. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jannis Limperg +-/ + +import Lean + +open Lean Lean.Meta + +namespace Aesop + +/-- The configuration used by all Aesop indices. -/ +-- I don't really know what I'm doing here. I'm just copying the config used +-- by `simp`; see `Meta/Simp/Types.lean:mkIndexConfig`. +def indexConfig : ConfigWithKey := + ({ proj := .no, transparency := .reducible : Config }).toConfigWithKey + +def mkDiscrTreePath (e : Expr) : MetaM (Array DiscrTree.Key) := + withConfigWithKey indexConfig $ DiscrTree.mkPath e + +def getUnify (t : DiscrTree α) (e : Expr) : MetaM (Array α) := + withConfigWithKey indexConfig $ t.getUnify e + +def getMatch (t : DiscrTree α) (e : Expr) : MetaM (Array α) := + withConfigWithKey indexConfig $ t.getMatch e + +end Aesop diff --git a/Aesop/Index/DiscrTreeConfig.lean b/Aesop/Index/DiscrTreeConfig.lean new file mode 100644 index 00000000..fc73bd63 --- /dev/null +++ b/Aesop/Index/DiscrTreeConfig.lean @@ -0,0 +1,28 @@ +/- +Copyright (c) 2024 Jannis Limperg. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jannis Limperg +-/ + +import Lean + +open Lean Lean.Meta + +namespace Aesop + +/-- The configuration used by all Aesop indices. -/ +-- I don't really know what I'm doing here. I'm just copying the config used +-- by `simp`; see `Meta/Simp/Types.lean:mkIndexConfig`. +def indexConfig : ConfigWithKey := + ({ proj := .no, transparency := .reducible : Config }).toConfigWithKey + +def mkDiscrTreePath (e : Expr) : MetaM (Array DiscrTree.Key) := + withConfigWithKey indexConfig $ DiscrTree.mkPath e + +def getUnify (t : DiscrTree α) (e : Expr) : MetaM (Array α) := + withConfigWithKey indexConfig $ t.getUnify e + +def getMatch (t : DiscrTree α) (e : Expr) : MetaM (Array α) := + withConfigWithKey indexConfig $ t.getMatch e + +end Aesop diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean index fac2c16f..2c0ca677 100644 --- a/Aesop/Util/Basic.lean +++ b/Aesop/Util/Basic.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jannis Limperg, Asta Halkjær From -/ +import Aesop.Index.DiscrTreeConfig import Aesop.Nanos import Aesop.Util.UnorderedArraySet import Batteries.Lean.Expr @@ -78,11 +79,10 @@ open DiscrTree -- For `type = ∀ (x₁, ..., xₙ), T`, returns keys that match `T * ... *` (with -- `n` stars). -def getConclusionDiscrTreeKeys (type : Expr) (config : ConfigWithKey) : - MetaM (Array Key) := +def getConclusionDiscrTreeKeys (type : Expr) : MetaM (Array Key) := withoutModifyingState do let (_, _, conclusion) ← forallMetaTelescope type - withConfigWithKey config <| mkPath conclusion + mkDiscrTreePath conclusion -- We use a meta telescope because `DiscrTree.mkPath` ignores metas (they -- turn into `Key.star`) but not fvars. From a4a08d92be3de00def5298059bf707c72dfd3c66 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 19 Dec 2024 20:54:36 +1100 Subject: [PATCH 07/10] chore: remove unnecessary explicit indexing proofs (#185) --- Aesop/Builder/Forward.lean | 2 +- Aesop/RulePattern.lean | 6 +++--- Aesop/RuleTac/Forward.lean | 2 +- Aesop/Script/StructureDynamic.lean | 2 +- Aesop/Script/StructureStatic.lean | 2 +- Aesop/Script/Util.lean | 2 +- Aesop/Search/Expansion.lean | 2 +- 7 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean index 16b041d0..dd797435 100644 --- a/Aesop/Builder/Forward.lean +++ b/Aesop/Builder/Forward.lean @@ -60,7 +60,7 @@ def getImmediatePremises (type : Expr) (pat? : Option RulePattern) for h : i in [:args.size] do if isPatternInstantiated i then continue - let fvarId := (args[i]'h.2).fvarId! + let fvarId := args[i].fvarId! let ldecl ← fvarId.getDecl let isNondep : MetaM Bool := args.allM (start := i + 1) λ arg => do diff --git a/Aesop/RulePattern.lean b/Aesop/RulePattern.lean index 6de12d8e..7c73ec24 100644 --- a/Aesop/RulePattern.lean +++ b/Aesop/RulePattern.lean @@ -144,7 +144,7 @@ def openRuleType (pat : RulePattern) (inst : RulePatternInstantiation) let mut assigned := ∅ for h : i in [:mvars.size] do if let some inst ← pat.getInstantiation inst i then - let mvarId := mvars[i]'h.2 |>.mvarId! + let mvarId := mvars[i] |>.mvarId! -- We use `isDefEq` to make sure that universe metavariables occurring in -- the type of `mvarId` are assigned. if ← isDefEq (.mvar mvarId) inst then @@ -163,7 +163,7 @@ def specializeRule (pat : RulePattern) (inst : RulePatternInstantiation) if let some inst ← pat.getInstantiation inst i then args := args.push $ some inst else - let fvarId := fvarIds[i]'h.2 + let fvarId := fvarIds[i] args := args.push $ some fvarId remainingFVarIds := remainingFVarIds.push fvarId let result ← mkLambdaFVars remainingFVarIds (← mkAppOptM' rule args) @@ -207,7 +207,7 @@ where let e := s.lctx.mkLambda s.fvars e let mut mvarIdToPos := ∅ for h : i in [:s.fvars.size] do - let name := s.lctx.get! (s.fvars[i]'h.2).fvarId! |>.userName + let name := s.lctx.get! (s.fvars[i]).fvarId! |>.userName mvarIdToPos := mvarIdToPos.insert ⟨name⟩ i let result := { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e } diff --git a/Aesop/RuleTac/Forward.lean b/Aesop/RuleTac/Forward.lean index 5c7cfc4c..fd18c6f3 100644 --- a/Aesop/RuleTac/Forward.lean +++ b/Aesop/RuleTac/Forward.lean @@ -33,7 +33,7 @@ partial def makeForwardHyps (e : Expr) (pat? : Option RulePattern) let mut instMVars := Array.mkEmpty argMVars.size let mut immediateMVars := Array.mkEmpty argMVars.size for h : i in [:argMVars.size] do - let mvarId := argMVars[i]'h.2 |>.mvarId! + let mvarId := argMVars[i].mvarId! if patInstantiatedMVars.contains mvarId then continue if immediate.contains i then diff --git a/Aesop/Script/StructureDynamic.lean b/Aesop/Script/StructureDynamic.lean index dbbafb8a..751c7da9 100644 --- a/Aesop/Script/StructureDynamic.lean +++ b/Aesop/Script/StructureDynamic.lean @@ -60,7 +60,7 @@ def DynStructureM.run (x : DynStructureM α) (script : UScript) : MetaM (α × Bool) := do let mut steps : PHashMap MVarId (Nat × Step) := {} for h : i in [:script.size] do - let step := script[i]'h.2 + let step := script[i] steps := steps.insert step.preGoal (i, step) let (a, s) ← ReaderT.run x { steps } |>.run {} return (a, s.perfect) diff --git a/Aesop/Script/StructureStatic.lean b/Aesop/Script/StructureStatic.lean index ccfca1b0..b111ce10 100644 --- a/Aesop/Script/StructureStatic.lean +++ b/Aesop/Script/StructureStatic.lean @@ -22,7 +22,7 @@ protected def StaticStructureM.run (script : UScript) (x : StaticStructureM α) CoreM (α × Bool) := do let mut steps : Std.HashMap MVarId (Nat × Step) := Std.HashMap.empty script.size for h : i in [:script.size] do - let step := script[i]'h.2 + let step := script[i] if h : step.postGoals.size = 1 then if step.postGoals[0].goal == step.preGoal then continue diff --git a/Aesop/Script/Util.lean b/Aesop/Script/Util.lean index 057e8bec..56866848 100644 --- a/Aesop/Script/Util.lean +++ b/Aesop/Script/Util.lean @@ -18,7 +18,7 @@ def findFirstStep? {α β : Type} (goals : Array α) (step? : α → Option β) (stepOrder : β → Nat) : Option (Nat × α × β) := Id.run do let mut firstStep? := none for h : pos in [:goals.size] do - let g := goals[pos]'h.2 + let g := goals[pos] if let some step := step? g then if let some (_, _, currentFirstStep) := firstStep? then if stepOrder step < stepOrder currentFirstStep then diff --git a/Aesop/Search/Expansion.lean b/Aesop/Search/Expansion.lean index 729ee123..7b28ff92 100644 --- a/Aesop/Search/Expansion.lean +++ b/Aesop/Search/Expansion.lean @@ -69,7 +69,7 @@ def addRapps (parentRef : GoalRef) (rule : RegularRule) let mut rrefs := Array.mkEmpty rapps.size let mut subgoals := Array.mkEmpty $ rapps.size * 3 for h : i in [:rapps.size] do - let rapp := rapps[i]'h.2 + let rapp := rapps[i] let successProbability := parent.successProbability * (rapp.successProbability?.getD rule.successProbability) From 2689851f387bb2cef351e6825fe94a56a304ca13 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 4 Jan 2025 14:26:26 +1100 Subject: [PATCH 08/10] chore: bump toolchain to v4.15.0 (#187) --- 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 8f13f997..2141a121 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "7805acf1864ba1a2e359f86a8f092ccf1438ad83", + "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0-rc1", + "inputRev": "v4.15.0", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index c47b9238..1338d186 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,7 +6,7 @@ precompileModules = false # We would like to turn this on, but it breaks the Mat [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.15.0-rc1" +rev = "v4.15.0" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index cf25a981..d0eb99ff 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0-rc1 +leanprover/lean4:v4.15.0 From 79402ad9ab4be9a2286701a9880697e2351e4955 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 4 Jan 2025 16:19:44 +1100 Subject: [PATCH 09/10] chore: bump toolchain to v4.16.0-rc1 (#188) Co-authored-by: Jannis Limperg Co-authored-by: Kyle Miller --- Aesop/RuleSet.lean | 4 ++-- Aesop/Util/Basic.lean | 1 + AesopTest/List.lean | 2 +- AesopTest/RulePattern.lean | 2 +- AesopTest/SaturatePerformance.lean | 10 +++++----- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 8 files changed, 14 insertions(+), 13 deletions(-) diff --git a/Aesop/RuleSet.lean b/Aesop/RuleSet.lean index 82bec298..c2cc0521 100644 --- a/Aesop/RuleSet.lean +++ b/Aesop/RuleSet.lean @@ -372,7 +372,7 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) : if let some decl := f.matchesSimpTheorem? then for h : i in [:rs.simpTheoremsArray.size] do have i_valid : i < simpTheoremsArray'.fst.size := by - simp_all [Membership.mem, simpTheoremsArray'.snd] + simp_all +zetaDelta [Membership.mem, simpTheoremsArray'.snd] let (name, simpTheorems) := simpTheoremsArray'.fst[i] if SimpTheorems.containsDecl simpTheorems decl then let origin := .decl decl (inv := false) @@ -383,7 +383,7 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) : anyErased := true let simpTheoremsArray := simpTheoremsArray'.fst let simpTheoremsArrayNonempty : 0 < simpTheoremsArray.size := by - simp [simpTheoremsArray'.snd, rs.simpTheoremsArrayNonempty] + simp [simpTheoremsArray, simpTheoremsArray'.snd, rs.simpTheoremsArrayNonempty] let rs := { rs with localNormSimpRules, simpTheoremsArray, simpTheoremsArrayNonempty } diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean index 2c0ca677..b7107f89 100644 --- a/Aesop/Util/Basic.lean +++ b/Aesop/Util/Basic.lean @@ -79,6 +79,7 @@ open DiscrTree -- For `type = ∀ (x₁, ..., xₙ), T`, returns keys that match `T * ... *` (with -- `n` stars). + def getConclusionDiscrTreeKeys (type : Expr) : MetaM (Array Key) := withoutModifyingState do let (_, _, conclusion) ← forallMetaTelescope type diff --git a/AesopTest/List.lean b/AesopTest/List.lean index a841358e..e3949614 100644 --- a/AesopTest/List.lean +++ b/AesopTest/List.lean @@ -892,7 +892,7 @@ theorem last_append (l₁ l₂ : List α) (h : l₂ ≠ []) : last (l₁ ++ l₂) (append_ne_nil_of_right_ne_nil l₁ h) = last l₂ h := by induction l₁ <;> aesop -theorem last_concat {a : α} (l : List α) : last (concat l a) (concat_ne_nil a l) = a := by +theorem last_concat {a : α} (l : List α) : last (concat l a) (X.concat_ne_nil a l) = a := by aesop @[simp] theorem last_singleton (a : α) : last [a] (cons_ne_nil a []) = a := rfl diff --git a/AesopTest/RulePattern.lean b/AesopTest/RulePattern.lean index 96d22c86..66280479 100644 --- a/AesopTest/RulePattern.lean +++ b/AesopTest/RulePattern.lean @@ -23,8 +23,8 @@ example (m n : Nat) : (↑m : Int) < 0 ∧ (↑n : Int) > 0 := by set_option aesop.check.script false in aesop! all_goals - guard_hyp fwd_1 : 0 ≤ (m : Int) guard_hyp fwd_2 : 0 ≤ (n : Int) + guard_hyp fwd_1 : 0 ≤ (m : Int) falso @[aesop safe forward (pattern := min x y)] diff --git a/AesopTest/SaturatePerformance.lean b/AesopTest/SaturatePerformance.lean index b57ad042..d4dfa8ca 100644 --- a/AesopTest/SaturatePerformance.lean +++ b/AesopTest/SaturatePerformance.lean @@ -41,11 +41,11 @@ import Aesop error: unsolved goals α : Type u_1 l0 l1 l2 : List α -fwd : (l0 ++ l1).length ≥ 0 -fwd_1 : (l0 ++ l1 ++ l2).length ≥ 0 -fwd_2 : l2.length ≥ 0 -fwd_3 : l0.length ≥ 0 -fwd_4 : l1.length ≥ 0 +fwd : l1.length ≥ 0 +fwd_1 : (l0 ++ l1).length ≥ 0 +fwd_2 : (l0 ++ l1 ++ l2).length ≥ 0 +fwd_3 : l2.length ≥ 0 +fwd_4 : l0.length ≥ 0 ⊢ (l0 ++ l1 ++ l2).length = l0.length + l1.length + l2.length -/ #guard_msgs in diff --git a/lake-manifest.json b/lake-manifest.json index 2141a121..8e136383 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b", + "rev": "8ce422eb59adf557fac184f8b1678c75fa03075c", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "v4.16.0-rc1", "inherited": false, "configFile": "lakefile.toml"}], "name": "aesop", diff --git a/lakefile.toml b/lakefile.toml index 1338d186..e575c71b 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,7 +6,7 @@ precompileModules = false # We would like to turn this on, but it breaks the Mat [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.15.0" +rev = "v4.16.0-rc1" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index d0eb99ff..62ccd717 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0 +leanprover/lean4:v4.16.0-rc1 From caa2968c7b51ea680605e7d500c6739912aa0446 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 14 Jan 2025 13:40:20 +1100 Subject: [PATCH 10/10] chore: bump to v4.16.0-rc2 (#189) --- lakefile.toml | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lakefile.toml b/lakefile.toml index e575c71b..63e0d875 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,7 +6,7 @@ precompileModules = false # We would like to turn this on, but it breaks the Mat [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.16.0-rc1" +rev = "v4.16.0-rc2" [[lean_lib]] name = "Aesop" diff --git a/lean-toolchain b/lean-toolchain index 62ccd717..a3edb8fc 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.16.0-rc1 +leanprover/lean4:v4.16.0-rc2