From b6c3f7d8fdc93fa8304eb1e9b3d7117656e24dc5 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 8 Apr 2025 10:54:23 -0700 Subject: [PATCH 1/2] chore: Update Lean to v4.18.0 --- Pantograph/Delate.lean | 2 +- Pantograph/Environment.lean | 4 ++-- Pantograph/Goal.lean | 2 +- Repl.lean | 4 ++-- Test/Common.lean | 4 ++-- Test/Proofs.lean | 2 +- lean-toolchain | 2 +- 7 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index b6e016c..a745854 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -26,7 +26,7 @@ def analyzeProjection (env: Environment) (e: Expr): Projection := | _ => panic! "Argument must be proj" if (getStructureInfo? env typeName).isSome then let ctor := getStructureCtor env typeName - let fieldName := getStructureFields env typeName |>.get! idx + let fieldName := (getStructureFields env typeName)[idx]! let projector := getProjFnForField? env typeName fieldName |>.get! .field projector ctor.numParams else diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index 3907105..4f0a678 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -26,7 +26,7 @@ def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[ def module_of_name (env: Environment) (name: Name): Option Name := do let moduleId ← env.getModuleIdxFor? name if h : moduleId.toNat < env.allImportedModuleNames.size then - return env.allImportedModuleNames.get moduleId.toNat h + return env.allImportedModuleNames[moduleId.toNat] else .none @@ -75,7 +75,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol. let info? := env.find? name let .some info := info? | Protocol.throw $ Protocol.errorIndex s!"Symbol not found {args.name}" let module? := env.getModuleIdxFor? name >>= - (λ idx => env.allImportedModuleNames.get? idx.toNat) + (λ idx => env.allImportedModuleNames[idx.toNat]?) let value? := match args.value?, info with | .some true, _ => info.value? | .some false, _ => .none diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 9af1740..7f135f5 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -102,7 +102,7 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac @[export pantograph_goal_state_focus] protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do - let goal ← state.savedState.tactic.goals.get? goalId + let goal ← state.savedState.tactic.goals[goalId]? return { state with savedState := { diff --git a/Repl.lean b/Repl.lean index bcbe8f9..a735c88 100644 --- a/Repl.lean +++ b/Repl.lean @@ -62,7 +62,7 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do let desc ← ex.toMessageData.toString return Except.error $ ({ error := "exception", desc } : Protocol.InteractionError) if let .some token := cancelTk? then - runCancelTokenWithTimeout token (timeout := .mk options.timeout) + runCancelTokenWithTimeout token (timeout := .ofBitVec options.timeout) let (result, state') ← match ← (coreM'.run coreCtx coreState).toIO' with | Except.error (Exception.error _ msg) => Protocol.throw $ { error := "core", desc := ← msg.toString } | Except.error (Exception.internal id _) => Protocol.throw $ { error := "internal", desc := (← id.getName).toString } @@ -290,7 +290,7 @@ def execute (command: Protocol.Command): MainM Json := do let state ← getMainState let .some goalState := state.goalStates[args.stateId]? | Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}" - let .some goal := goalState.goals.get? args.goalId | + let .some goal := goalState.goals[args.goalId]? | Protocol.throw $ errorIndex s!"Invalid goal index {args.goalId}" let nextGoalState?: Except _ TacticResult ← liftTermElabM do -- NOTE: Should probably use a macro to handle this... diff --git a/Test/Common.lean b/Test/Common.lean index c32d62d..c8ffa5d 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -67,8 +67,8 @@ protected def Goal.devolatilize (goal: Goal): Goal := end Condensed -def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals.get! i -def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.goals.get! goalId) tactic +def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals[i]! +def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.get! goalId) tactic def TacticResult.toString : TacticResult → String | .success state => s!".success ({state.goals.length} goals)" diff --git a/Test/Proofs.lean b/Test/Proofs.lean index a760eb4..ceb8690 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -328,7 +328,7 @@ def test_or_comm: TestM Unit := do addTest $ assertUnreachable $ msg return () | .ok state => pure state - addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0]) + addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals[0]!]) let state3_1 ← match ← state2b.tacticOn (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state | other => do diff --git a/lean-toolchain b/lean-toolchain index 5499a24..b2153cd 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.17.0 +leanprover/lean4:v4.18.0 From 13b03b602b262ce44d42318540b4d74999e29b72 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 8 Apr 2025 10:59:37 -0700 Subject: [PATCH 2/2] chore: Update flake --- flake.lock | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/flake.lock b/flake.lock index 11c740e..d09589f 100644 --- a/flake.lock +++ b/flake.lock @@ -5,11 +5,11 @@ "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1741352980, - "narHash": "sha256-+u2UunDA4Cl5Fci3m7S643HzKmIDAe+fiXrLqYsR2fs=", + "lastModified": 1743550720, + "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "f4330d22f1c5d2ba72d3d22df5597d123fdb60a9", + "rev": "c621e8422220273271f52058f618c94e405bb0f5", "type": "github" }, "original": { @@ -44,11 +44,11 @@ ] }, "locked": { - "lastModified": 1741472588, - "narHash": "sha256-XnMeMZKuspEphP+fEq4soc3PY7Nz+gsMPjlsXbobyrA=", + "lastModified": 1743534244, + "narHash": "sha256-WnoYs2iyrfgh35eXErCOyos8E2YbW3LT1xm/EtT88/k=", "owner": "lenianiva", "repo": "lean4-nix", - "rev": "cffeb67d58e02b50ccb9acd51b0212dc653ed6ce", + "rev": "5eb7f03be257e327fdb3cca9465392e68dc28a4d", "type": "github" }, "original": { @@ -59,11 +59,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1742751704, - "narHash": "sha256-rBfc+H1dDBUQ2mgVITMGBPI1PGuCznf9rcWX/XIULyE=", + "lastModified": 1743975612, + "narHash": "sha256-o4FjFOUmjSRMK7dn0TFdAT0RRWUWD+WsspPHa+qEQT8=", "owner": "nixos", "repo": "nixpkgs", - "rev": "f0946fa5f1fb876a9dc2e1850d9d3a4e3f914092", + "rev": "a880f49904d68b5e53338d1e8c7bf80f59903928", "type": "github" }, "original": { @@ -75,11 +75,11 @@ }, "nixpkgs-lib": { "locked": { - "lastModified": 1740877520, - "narHash": "sha256-oiwv/ZK/2FhGxrCkQkB83i7GnWXPPLzoqFHpDD3uYpk=", + "lastModified": 1743296961, + "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=", "owner": "nix-community", "repo": "nixpkgs.lib", - "rev": "147dee35aab2193b174e4c0868bd80ead5ce755c", + "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa", "type": "github" }, "original": {