Update to Lean v4.10.0

lake-manifest.json

@@ -1,23 +1,25 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "ae9ae7f279421e45a9b87d67f2d28aaef299de5c",
-   "name": "std",
+   "scope": "",
+   "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.10.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/gebner/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
+   "scope": "",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"}],
- "name": "iris",
+ "name": "Iris",
  "lakeDir": ".lake"}

lakefile.lean

@@ -1,11 +1,11 @@
 import Lake
 open Lake DSL
 
-package iris where
+package Iris where
   srcDir := "./src/"
 
-require std from git "https://github.com/leanprover/std4" @ "main"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.10.0"
 require Qq from git "https://github.com/gebner/quote4" @ "master"
 
 @[default_target]
-lean_lib iris
+lean_lib Iris

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.0-rc1
+leanprover/lean4:v4.10.0

src/Iris/Algebra/OFE.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Std.Logic
+import Batteries.Logic
 
 namespace Iris
 

src/Iris/BI/DerivedLaws.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro
 -/
-import Std.Logic
+import Batteries.Logic
 import Iris.BI.Classes
 import Iris.BI.Extensions
 import Iris.BI.BI

src/Iris/BI/Notation.lean

@@ -31,7 +31,13 @@ partial def unpackIprop [Monad m] [MonadRef m] [MonadQuotation m] : Term → m T
   | `(?$P:ident)             => do `(?$P)
   | `(($P))                  => do `(($(← unpackIprop P)))
   | `($P $[ $Q]*)            => do ``($P $[ $Q]*)
-  | `(if $c then $t else $e) => do `(if $c then $(← unpackIprop t) else $(← unpackIprop e))
+  | `(if $c then $t else $e) => do
+    -- TODO: Why does `(if $c then $(← unpackIprop t) else $e) give
+    -- "invalid use of `(<- ...)`, must be nested inside a 'do'
+    -- expression" here, but not in the other cases?
+    let t ← unpackIprop t;
+    let e ← unpackIprop e;
+    `(if $c then $t else $e)
   | `(($P : $t))             => do ``(($(← unpackIprop P) : $t))
   | `($t)                    => `($t:term)
 

src/Iris/Instances/Classical/Instance.lean

@@ -3,7 +3,6 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König
 -/
-import Std.Tactic.RCases
 import Iris.BI
 import Iris.Instances.Data
 import Iris.Std.Equivalence

src/Iris/Instances/Data/SetNotation.lean

@@ -3,7 +3,6 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König
 -/
-import Std.Classes.SetNotation
 
 namespace Iris.Instances.Data
 

src/Iris/ProofMode/Instances.lean

@@ -511,7 +511,7 @@ instance fromPure_pure_sep_true (a1 a2 : Bool) (φ1 φ2 : Prop) [BI PROP] (P1 P2
     | true, false => persistent_and_affinely_sep_l.1
     | true, true => affinely_and.1.trans persistent_and_sep_1
 
-instance fromPure_pure_wand_true (a : Bool) (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP)
+instance fromPure_pure_wand_true (_ : Bool) (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP)
     [h1 : IntoPure P1 φ1] [h2 : FromPure true P2 φ2] [Affine P1] :
     FromPure true iprop(P1 -∗ P2) (φ1 → φ2) where
   from_pure := by
@@ -520,7 +520,7 @@ instance fromPure_pure_wand_true (a : Bool) (φ1 φ2 : Prop) [BI PROP] (P1 P2 :
       (and_mono_r (affine_affinely P1).2).trans <|
       affinely_and_r.1.trans <| affinely_mono <| (and_mono pure_imp_2 h1.1).trans imp_elim_l
 
-instance fromPure_pure_wand_false (a : Bool) (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP)
+instance fromPure_pure_wand_false (_ : Bool) (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP)
     [h1 : IntoPure P1 φ1] [h2 : FromPure false P2 φ2] :
     FromPure false iprop(P1 -∗ P2) (φ1 → φ2) where
   from_pure := by

src/Iris/ProofMode/Tactics/Clear.lean

@@ -20,7 +20,7 @@ def clearCore {prop : Q(Type)} (_bi : Q(BI $prop)) (e e' out goal : Q($prop))
   if out.isAppOfArity ``intuitionistically 3 then
     have out' : Q($prop) := out.appArg!
     have : $out =Q iprop(□ $out') := ⟨⟩
-    pure q(clear_intuitionistic $pf)
+    pure q(clear_intuitionistic (Q:=$goal) $pf)
   else
     let _ ← synthInstanceQ q(TCOr (Affine $out) (Absorbing $goal))
     pure q(clear_spatial $pf)

src/Iris/ProofMode/Tactics/Pure.lean

@@ -89,7 +89,7 @@ elab "ipure_intro" : tactic => do
   let (mvar, { e, goal, .. }) ← istart (← getMainGoal)
   mvar.withContext do
 
-  let b ← mkFreshExprMVarQ q(Bool)
+  let b : Q(Bool) ← mkFreshExprMVarQ q(Bool)
   let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop)
   let _ ← synthInstanceQ q(FromPure $b $goal $φ)
   let m : Q($φ) ← mkFreshExprMVar (← instantiateMVars φ)

src/Iris/ProofMode/Tactics/Specialize.lean

@@ -46,8 +46,8 @@ def SpecializeState.process1 :
       return { hyps := hyps', b := b2, out := out₂, pf }
     else
       -- otherwise specialize the universal quantifier
-      let α ← mkFreshExprMVarQ q(Type)
-      let Φ ← mkFreshExprMVarQ q($α → $prop)
+      let α : Q(Type) ← mkFreshExprMVarQ q(Type)
+      let Φ : Q($α → $prop) ← mkFreshExprMVarQ q($α → $prop)
       let _ ← synthInstanceQ q(IntoForall $out $Φ)
       let x ← elabTermEnsuringTypeQ (u := .succ .zero) arg α
       have out' : Q($prop) := Expr.headBeta q($Φ $x)

src/Iris/Std/Expr.lean

@@ -25,14 +25,14 @@ def modifyAppOptM (e : Expr) (args : Array <| Option Expr) : Expr :=
 
 /-- Get the `mdata` entry with the key `"name"`, if available. -/
 def getMDataName? : Expr → Option Name
-  | Expr.mdata md _ => md.get? "name"
+  | Expr.mdata md _ => md.get? (Name.mkSimple "name")
   | _ => none
 
 /-- Set the `mdata` entry of `e` with the key `"name"` to `name`. -/
 def setMDataName? (e : Expr) (name : Name) : Expr := match e with
   | Expr.mdata md e =>
-    mkMData (md.insert "name" name) e
+    mkMData (md.insert (Name.mkSimple "name") name) e
   | e =>
-    mkMData (KVMap.empty.insert "name" name) e
+    mkMData (KVMap.empty.insert (Name.mkSimple "name") name) e
 
 end Lean.Expr