chore: bump Std (#10378)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Feb 9, 2024 · 359fc77 · 359fc77
1 parent 3a4cb1b
commit 359fc77
Show file tree

Hide file tree

Showing 16 changed files with 19 additions and 4 deletions.
diff --git a/Mathlib/Lean/Expr/Basic.lean b/Mathlib/Lean/Expr/Basic.lean
@@ -6,6 +6,7 @@ Floris van Doorn, E.W.Ayers, Arthur Paulino
 -/
 import Lean.Meta.Tactic.Rewrite
 import Std.Lean.Expr
+import Std.Lean.Name
 import Std.Data.Rat.Basic
 import Std.Data.List.Basic
 

diff --git a/Mathlib/Lean/Meta/Simp.lean b/Mathlib/Lean/Meta/Simp.lean
@@ -5,6 +5,7 @@ Authors: Scott Morrison, Gabriel Ebner, Floris van Doorn
 -/
 import Std.Tactic.OpenPrivate
 import Std.Lean.Meta.DiscrTree
+import Lean.Elab.Tactic.Simp
 
 /-!
 # Helper functions for using the simplifier.

diff --git a/Mathlib/Lean/Name.lean b/Mathlib/Lean/Name.lean
@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import Std.Data.HashMap.Basic
 import Std.Lean.SMap
+import Std.Lean.Name
 
 /-!
 # Additional functions on `Lean.Name`.

diff --git a/Mathlib/Tactic/Congr!.lean b/Mathlib/Tactic/Congr!.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
+import Lean.Elab.Tactic.Config
 import Mathlib.Lean.Meta.CongrTheorems
 import Mathlib.Tactic.Relation.Rfl
 import Std.Logic

diff --git a/Mathlib/Tactic/LibrarySearch.lean b/Mathlib/Tactic/LibrarySearch.lean
@@ -5,7 +5,9 @@ Authors: Gabriel Ebner, Scott Morrison
 -/
 import Std.Util.Pickle
 import Std.Util.Cache
+import Std.Lean.Parser
 import Std.Tactic.SolveByElim
+import Std.Tactic.TryThis
 import Std.Data.MLList.Heartbeats
 import Mathlib.Lean.Meta
 import Mathlib.Lean.Meta.DiscrTree

diff --git a/Mathlib/Tactic/Monotonicity/Basic.lean b/Mathlib/Tactic/Monotonicity/Basic.lean
@@ -5,6 +5,7 @@ Authors: Simon Hudon
 -/
 import Mathlib.Tactic.Monotonicity.Attr
 import Std.Tactic.SolveByElim
+import Std.Lean.Parser
 
 /-! # Monotonicity tactic
 

diff --git a/Mathlib/Tactic/NormNum/Core.lean b/Mathlib/Tactic/NormNum/Core.lean
@@ -7,6 +7,7 @@ import Std.Lean.Parser
 import Std.Lean.Meta.DiscrTree
 import Mathlib.Tactic.NormNum.Result
 import Mathlib.Util.Qq
+import Lean.Elab.Tactic.Location
 
 /-!
 ## `norm_num` core functionality

diff --git a/Mathlib/Tactic/PushNeg.lean b/Mathlib/Tactic/PushNeg.lean
@@ -9,6 +9,7 @@ import Mathlib.Logic.Basic
 import Mathlib.Init.Order.Defs
 import Mathlib.Tactic.Conv
 import Mathlib.Init.Set
+import Lean.Elab.Tactic.Location
 
 set_option autoImplicit true
 

diff --git a/Mathlib/Tactic/Relation/Trans.lean b/Mathlib/Tactic/Relation/Trans.lean
@@ -5,7 +5,6 @@ Authors: Siddhartha Gadgil, Mario Carneiro
 -/
 import Mathlib.Lean.Meta
 import Mathlib.Lean.Elab.Tactic.Basic
-import Lean.Elab.Tactic.Location
 
 /-!
 # `trans` tactic

diff --git a/Mathlib/Tactic/Rewrites.lean b/Mathlib/Tactic/Rewrites.lean
@@ -13,6 +13,7 @@ import Mathlib.Control.Basic
 import Mathlib.Data.MLList.Dedup
 import Mathlib.Lean.Expr.Basic
 import Mathlib.Lean.Meta.DiscrTree
+import Lean.Elab.Tactic.Location
 
 /-!
 # The `rewrites` tactic.

diff --git a/Mathlib/Tactic/Says.lean b/Mathlib/Tactic/Says.lean
@@ -5,6 +5,8 @@ Authors: Kim Liesinger
 -/
 import Std.Data.String.Basic
 import Std.Tactic.GuardMsgs
+import Std.Tactic.TryThis
+import Std.Linter.UnreachableTactic
 import Qq.Match
 
 /-!

diff --git a/Mathlib/Tactic/Simps/Basic.lean b/Mathlib/Tactic/Simps/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-
+import Lean.Elab.Tactic.Simp
 import Mathlib.Tactic.Simps.NotationClass
 import Std.Classes.Dvd
 import Std.Data.String.Basic

diff --git a/Mathlib/Tactic/Widget/Calc.lean b/Mathlib/Tactic/Widget/Calc.lean
@@ -5,6 +5,7 @@ Authors: Patrick Massot
 -/
 import Lean.Elab.Tactic.Calc
 import Std.CodeAction
+import Std.Data.Json
 
 import Mathlib.Data.String.Defs
 import Mathlib.Tactic.Widget.SelectPanelUtils

diff --git a/Mathlib/Tactic/Widget/Conv.lean b/Mathlib/Tactic/Widget/Conv.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Robin Böhne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robin Böhne, Wojciech Nawrocki, Patrick Massot
 -/
+import Std.Data.Json
 import Mathlib.Tactic.Widget.SelectPanelUtils
 import Mathlib.Data.String.Defs
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "2a1b7546b2df0f8e65a70d3b228c30d91752acc4",
+   "rev": "6132dd32b49f17b1d300aba3fb15966e8f489432",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "4746cab6320a0d87ec951105ccd42e656fb15e89",
+   "rev": "204c8f47bd79fba6b53d72536826a97fd58c016a",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

diff --git a/test/says.lean b/test/says.lean
@@ -1,6 +1,8 @@
 import Mathlib.Tactic.Says
 import Mathlib.Tactic.RunCmd
 import Aesop
+import Std.Tactic.ShowTerm
+import Std.Tactic.SimpTrace
 
 set_option autoImplicit true
 /--