chore: run lake exe shake (and then repair) (#160)

Aesop.lean

@@ -1,3 +1,4 @@
 import Aesop.Main
 import Aesop.Frontend.Command
 import Aesop.Frontend.Saturate
+import Aesop.BuiltinRules

Aesop/Builder/Constructors.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Aesop.Builder.Apply
+import Aesop.Builder.Basic
 
 open Lean
 open Lean.Meta

Aesop/Builder/Default.lean

@@ -7,6 +7,7 @@ Authors: Jannis Limperg
 import Aesop.Builder.Constructors
 import Aesop.Builder.NormSimp
 import Aesop.Builder.Tactic
+import Aesop.Builder.Apply
 
 open Lean
 open Lean.Meta

Aesop/Frontend/Command.lean

@@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Aesop.Frontend.Attribute
 import Aesop.Frontend.Basic
 import Aesop.Stats.Report
 import Batteries.Linter.UnreachableTactic
+import Aesop.Frontend.Extension
+import Aesop.Frontend.RuleExpr
 
 open Lean Lean.Elab Lean.Elab.Command
 

Aesop/Frontend/RuleExpr.lean

@@ -5,11 +5,13 @@ Authors: Jannis Limperg
 -/
 
 import Aesop.ElabM
-import Aesop.Frontend.Basic
 import Aesop.Percent
 import Aesop.Rule.Name
-import Aesop.Builder
-import Aesop.RuleSet
+import Aesop.Builder.Cases
+import Aesop.Builder.Default
+import Aesop.Builder.Forward
+import Aesop.Builder.Unfold
+import Aesop.RuleSet.Filter
 
 open Lean
 open Lean.Meta

Aesop/Frontend/Saturate.lean

@@ -6,6 +6,7 @@ Authors: Jannis Limperg
 
 import Aesop.Saturate
 import Aesop.Frontend.Extension
+import Aesop.Builder.Forward
 
 open Lean Lean.Meta Lean.Elab Lean.Elab.Term Lean.PrettyPrinter
 

Aesop/Frontend/Tactic.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Aesop.Frontend.Attribute
 import Aesop.Frontend.RuleExpr
 import Aesop.Options
 import Batteries.Linter.UnreachableTactic
+import Aesop.Frontend.Extension
 
 open Lean
 open Lean.Meta

Aesop/Index.lean

@@ -9,6 +9,8 @@ import Aesop.RulePattern
 import Aesop.Rule.Basic
 import Aesop.Tracing
 import Batteries.Lean.Meta.InstantiateMVars
+import Batteries.Lean.PersistentHashSet
+import Batteries.Lean.Meta.DiscrTree
 
 open Lean
 open Lean.Meta

Aesop/Main.lean

@@ -5,7 +5,6 @@ Authors: Jannis Limperg
 -/
 
 import Aesop.Search.Main
-import Aesop.BuiltinRules -- ensures that the builtin rules are registered
 import Aesop.Frontend.Tactic
 import Aesop.Stats.Extension
 

Aesop/Rule.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg, Asta Halkjær From
 -/
 
-import Aesop.Index
 import Aesop.Rule.Basic
 import Aesop.Percent
 

Aesop/Rule/Name.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Aesop.Util.Basic
+import Lean.Meta.Basic
 
 open Lean
 open Lean.Meta

Aesop/RuleSet.lean

@@ -3,8 +3,9 @@ Copyright (c) 2021-2024 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
+import Aesop.Index
 import Aesop.RuleSet.Filter
+import Aesop.RuleSet.Member
 
 open Lean Lean.Meta
 

Aesop/RuleSet/Filter.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Aesop.RuleSet.Member
 import Aesop.RuleSet.Name
+import Aesop.Rule.Name
 
 open Lean
 

Aesop/RuleTac/Basic.lean

@@ -5,13 +5,13 @@ Authors: Jannis Limperg
 -/
 
 import Aesop.Index.Basic
-import Aesop.Options
 import Aesop.Percent
 import Aesop.RuleTac.GoalDiff
 import Aesop.RuleTac.FVarIdSubst
 import Aesop.Script.CtorNames
 import Aesop.Script.Step
 import Batteries.Lean.Meta.SavedState
+import Aesop.Options.Internal
 
 open Lean
 open Lean.Elab.Tactic

Aesop/Saturate.lean

@@ -4,11 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Aesop.Builder.Forward
 import Aesop.RuleSet
 import Aesop.RuleTac
-import Aesop.Script.Main
 import Aesop.Search.Expansion.Basic
+import Aesop.Script.Check
 
 open Lean Lean.Meta
 

Aesop/Script/Main.lean

@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Aesop.Options
 import Aesop.Script.Check
 import Aesop.Script.StructureDynamic
 import Aesop.Script.StructureStatic
 import Aesop.Script.OptimizeSyntax
 import Aesop.Stats.Basic
+import Aesop.Options.Internal
 
 open Lean
 open Lean.Parser.Tactic (tacticSeq)

Aesop/Script/OptimizeSyntax.lean

@@ -5,7 +5,6 @@ Authors: Jannis Limperg
 -/
 
 import Lean
-import Std
 
 namespace Aesop
 

Aesop/Script/StructureStatic.lean

@@ -1,6 +1,5 @@
 import Aesop.Script.UScriptToSScript
 import Aesop.Script.Util
-import Aesop.Stats.Basic
 
 open Lean Lean.Meta
 

Aesop/Script/TacticState.lean

@@ -5,7 +5,6 @@ Authors: Jannis Limperg
 -/
 import Batteries.Lean.Meta.Basic
 import Aesop.Script.GoalWithMVars
-import Aesop.Util.Basic
 
 open Lean
 

Aesop/Script/Util.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Aesop.RuleTac.Forward.Basic
 import Aesop.Util.Basic
 import Aesop.Util.EqualUpToIds
+import Batteries.Lean.Meta.SavedState
 
 open Lean Std Lean.Meta
 

Aesop/Search/ExpandSafePrefix.lean

@@ -3,7 +3,6 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
 import Aesop.Exception
 import Aesop.Search.Expansion
 

Aesop/Search/Expansion.lean

@@ -5,6 +5,7 @@ Authors: Jannis Limperg
 -/
 
 import Aesop.Search.Expansion.Norm
+import Aesop.Tree.AddRapp
 
 open Lean
 open Lean.Meta

Aesop/Search/Expansion/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Aesop.Rule.Basic
+import Aesop.RuleTac.Basic
 
 open Lean
 open Lean.Meta

Aesop/Search/Expansion/Norm.lean

@@ -10,6 +10,8 @@ import Aesop.Search.Expansion.Basic
 import Aesop.Search.Expansion.Simp
 import Aesop.Search.RuleSelection
 import Aesop.Search.SearchM
+import Aesop.Tree.State
+import Batteries.Lean.HashSet
 
 open Lean Lean.Meta Aesop.Script
 

Aesop/Search/Expansion/Simp.lean

@@ -3,13 +3,9 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-import Lean.Elab.Tactic.Simp
-import Aesop.Options
-import Aesop.RuleSet
-import Lean.Elab.Tactic.Simp
+import Lean.Meta.Tactic.Simp.SimpAll
 
 open Lean Lean.Meta
-open Lean.Elab.Tactic (mkSimpOnly)
 open Simp (UsedSimps)
 
 namespace Aesop

Aesop/Search/Main.lean

@@ -5,7 +5,6 @@ Authors: Jannis Limperg
 -/
 
 import Aesop.Check
-import Aesop.Frontend.Attribute
 import Aesop.Options
 import Aesop.RuleSet
 import Aesop.Script.Check
@@ -14,6 +13,7 @@ import Aesop.Search.Expansion
 import Aesop.Search.ExpandSafePrefix
 import Aesop.Search.Queue
 import Aesop.Tree
+import Aesop.Frontend.Extension
 
 open Lean
 open Lean.Elab.Tactic (liftMetaTacticAux TacticM)

Aesop/Search/Queue/Class.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Aesop.Tree
+import Aesop.Tree.Data
 
 open Lean
 

Aesop/Search/RuleSelection.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
+import Aesop.Tree.RunMetaM
 import Aesop.Search.SearchM
 
 open Lean

Aesop/Search/SearchM.lean

@@ -5,10 +5,10 @@ Authors: Jannis Limperg
 -/
 
 import Aesop.Options
-import Aesop.Search.Expansion.Simp
 import Aesop.Search.Queue.Class
 import Aesop.Stats.Basic
 import Aesop.RuleSet
+import Aesop.Tree.TreeM
 
 open Lean
 open Lean.Meta

Aesop/Tree/AddRapp.lean

@@ -7,6 +7,7 @@ Authors: Jannis Limperg
 import Aesop.Check
 import Aesop.Tree.Traversal
 import Aesop.Tree.TreeM
+import Aesop.Util.UnionFind
 
 open Lean
 open Lean.Meta

Aesop/Tree/Check.lean

@@ -9,6 +9,7 @@ import Aesop.Tree.State
 import Aesop.Tree.Traversal
 import Aesop.Tree.TreeM
 import Batteries.Lean.HashSet
+import Aesop.Tree.RunMetaM
 
 open Lean
 open Lean.Meta

Aesop/Tree/ExtractProof.lean

@@ -5,8 +5,8 @@ Authors: Jannis Limperg
 -/
 import Lean.Replay
 import Aesop.Tracing
-import Aesop.Tree.Tracing
 import Aesop.Tree.TreeM
+import Batteries.Lean.Meta.InstantiateMVars
 
 open Lean
 open Lean.Meta

Aesop/Tree/TreeM.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Aesop.Tree.RunMetaM
+import Aesop.Tree.Data
 
 open Lean
 open Lean.Meta

Aesop/Tree/UnsafeQueue.lean

@@ -6,7 +6,6 @@ Authors: Jannis Limperg
 
 import Aesop.Constants
 import Aesop.Rule
-import Batteries.Data.Array.Merge
 
 open Lean
 

Aesop/Util/Basic.lean

@@ -5,12 +5,9 @@ Authors: Jannis Limperg, Asta Halkjær From
 -/
 
 import Aesop.Nanos
-import Aesop.Util.UnionFind
 import Aesop.Util.UnorderedArraySet
-import Batteries.Data.String
 import Batteries.Lean.Expr
-import Batteries.Lean.Meta.DiscrTree
-import Batteries.Lean.PersistentHashSet
+import Batteries.Data.String.Basic
 import Lean
 
 open Lean

Aesop/Util/EqualUpToIds.lean

@@ -3,8 +3,7 @@ Copyright (c) 2023 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-import Lean.Elab.Tactic.Basic
-import Batteries.Lean.Meta.SavedState
+import Batteries.Lean.Meta.Basic
 
 open Lean Std Lean.Meta
 

AesopTest/EqualUpToIds.lean

@@ -6,6 +6,7 @@ Authors: Jannis Limperg
 
 import Aesop.Util.Basic
 import Aesop.Util.EqualUpToIds
+import Aesop.Tree.RunMetaM
 
 -- 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

AesopTest/EraseSimp.lean

@@ -5,7 +5,6 @@ Authors: Jannis Limperg
 -/
 
 import Aesop
-import Batteries.Linter.UnreachableTactic
 
 set_option aesop.check.all true
 set_option aesop.smallErrorMessages true

AesopTest/HeartbeatLimit.lean

@@ -5,7 +5,6 @@ Authors: Jannis Limperg
 -/
 
 import Aesop
-import Batteries.Linter.UnreachableTactic
 
 set_option aesop.check.all true
 set_option aesop.smallErrorMessages true

AesopTest/List.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
--- import Std
-import Batteries.Data.List.Lemmas
 -- Ported from mathlib3, file src/data/list/basic.lean,
 -- commit a945b3769cb82bc238ee004b4327201a6864e7e0