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

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

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 := {

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...

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)"

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

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": {

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.17.0
+leanprover/lean4:v4.18.0