From a5faf62110d5425b6d70cb70a34c1026bfe1d342 Mon Sep 17 00:00:00 2001 From: Michael Sammler Date: Mon, 19 Aug 2024 16:52:50 +0200 Subject: [PATCH] Update to Lean v4.10.0 --- lake-manifest.json | 16 +++++++++------- lakefile.lean | 6 +++--- lean-toolchain | 2 +- src/Iris/Algebra/OFE.lean | 2 +- src/Iris/BI/DerivedLaws.lean | 2 +- src/Iris/BI/Notation.lean | 8 +++++++- src/Iris/Instances/Classical/Instance.lean | 1 - src/Iris/Instances/Data/SetNotation.lean | 1 - src/Iris/ProofMode/Instances.lean | 4 ++-- src/Iris/ProofMode/Tactics/Clear.lean | 2 +- src/Iris/ProofMode/Tactics/Pure.lean | 2 +- src/Iris/ProofMode/Tactics/Specialize.lean | 4 ++-- src/Iris/Std/Expr.lean | 6 +++--- 13 files changed, 31 insertions(+), 25 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 97b04d0..ea4a9bd 100644 --- a/lake-manifest.json +++ b/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"} diff --git a/lakefile.lean b/lakefile.lean index 58035ff..33bbd1a 100644 --- a/lakefile.lean +++ b/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 diff --git a/lean-toolchain b/lean-toolchain index cfcdd32..7f0ea50 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.6.0-rc1 +leanprover/lean4:v4.10.0 diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean index 447d23c..5f4d702 100644 --- a/src/Iris/Algebra/OFE.lean +++ b/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 diff --git a/src/Iris/BI/DerivedLaws.lean b/src/Iris/BI/DerivedLaws.lean index 58d4a7e..304caf9 100644 --- a/src/Iris/BI/DerivedLaws.lean +++ b/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 diff --git a/src/Iris/BI/Notation.lean b/src/Iris/BI/Notation.lean index 32773e2..b75fea1 100644 --- a/src/Iris/BI/Notation.lean +++ b/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) diff --git a/src/Iris/Instances/Classical/Instance.lean b/src/Iris/Instances/Classical/Instance.lean index 55e6925..d94626c 100644 --- a/src/Iris/Instances/Classical/Instance.lean +++ b/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 diff --git a/src/Iris/Instances/Data/SetNotation.lean b/src/Iris/Instances/Data/SetNotation.lean index f5a79de..0eed8b3 100644 --- a/src/Iris/Instances/Data/SetNotation.lean +++ b/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 diff --git a/src/Iris/ProofMode/Instances.lean b/src/Iris/ProofMode/Instances.lean index f885940..625e458 100644 --- a/src/Iris/ProofMode/Instances.lean +++ b/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 diff --git a/src/Iris/ProofMode/Tactics/Clear.lean b/src/Iris/ProofMode/Tactics/Clear.lean index 3d8aac0..92b36f8 100644 --- a/src/Iris/ProofMode/Tactics/Clear.lean +++ b/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) diff --git a/src/Iris/ProofMode/Tactics/Pure.lean b/src/Iris/ProofMode/Tactics/Pure.lean index 9ffd469..369c4a4 100644 --- a/src/Iris/ProofMode/Tactics/Pure.lean +++ b/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 φ) diff --git a/src/Iris/ProofMode/Tactics/Specialize.lean b/src/Iris/ProofMode/Tactics/Specialize.lean index 77f4ef1..1814b50 100644 --- a/src/Iris/ProofMode/Tactics/Specialize.lean +++ b/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) diff --git a/src/Iris/Std/Expr.lean b/src/Iris/Std/Expr.lean index 7247231..cc7e30e 100644 --- a/src/Iris/Std/Expr.lean +++ b/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