chore: bump to v4.2.0-rc2 (#72)

* fix: use replay from leanprover/lean4#2617

* chore: adapt to leanprover/lean4#2621

* bump to v4.2.0-rc2

Author: kim-em

Aesop/Search/Expansion/Simp.lean

@@ -44,9 +44,12 @@ def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) (includeFVars : Bool) :
   let env ← getEnv
   for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
     match thm with
-    | .decl declName => -- global definitions in the environment
+    | .decl declName inv => -- global definitions in the environment
       if env.contains declName && !Lean.Elab.Tactic.simpOnlyBuiltins.contains declName then
-        args := args.push (← `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident))
+        args := args.push (← if inv then
+          `(Parser.Tactic.simpLemma| ← $(mkIdent (← unresolveNameGlobal declName)):ident)
+        else
+          `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident))
     | .fvar fvarId => -- local hypotheses in the context
       if ! includeFVars then
         continue

Aesop/Tree/ExtractProof.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 Lean.Replay
 import Aesop.Tracing
 import Aesop.Tree.Tracing
 import Aesop.Tree.TreeM
@@ -52,14 +52,14 @@ local macro "throwPRError " s:interpolatedStr(term) : term =>
 -- ## Copying Declarations
 
 private def getNewConsts (oldEnv newEnv : Environment) :
-    Array ConstantInfo := Id.run do
+    HashMap Name ConstantInfo := Id.run do
   let oldMap₂ := oldEnv.constants.map₂
   let newMap₂ := newEnv.constants.map₂
   if oldMap₂.size == newMap₂.size then
-    #[]
+    HashMap.empty
   else
-    newMap₂.foldl (init := #[]) λ cs n c =>
-      if oldMap₂.contains n then cs else cs.push c
+    newMap₂.foldl (init := HashMap.empty) λ cs n c =>
+      if oldMap₂.contains n then cs else cs.insert n c
 
 -- For each declaration `d` that appears in `newState` but not in
 -- `oldState`, add `d` to the environment. We assume that the environment in
@@ -71,7 +71,7 @@ private def getNewConsts (oldEnv newEnv : Environment) :
 --    identical. (These contain imported decls.)
 private def copyNewDeclarations (oldEnv newEnv : Environment) : CoreM Unit := do
   let newConsts := getNewConsts oldEnv newEnv
-  setEnv $ newConsts.foldl (init := ← getEnv) λ env c => env.add c
+  setEnv (← (← getEnv).replay newConsts)
 
 open Match in
 private def copyMatchEqnsExtState (oldEnv newEnv : Environment) : CoreM Unit := do

lake-manifest.json

@@ -1,11 +1,12 @@
-{"version": 5,
+{"version": 6,
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "f2df4ab8c0726fce3bafb73a5727336b0c3120ea",
+    "rev": "85a0d4891518518edfccee16cbceac139efa460c",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
-    "inherited": false}}]}
+    "inherited": false}}],
+ "name": "aesop"}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc1
+leanprover/lean4:v4.2.0-rc2