Merge pull request 'chore: Update Lean to v4.20.1' (#209) from chore/toolchain into dev

Reviewed-on: #209
2025-06-18 16:39:18 -07:00 · 2025-06-18 16:39:18 -07:00 · 9a8b5040f5
parent 8fd3649f32 66eb98397b
commit 9a8b5040f5
9 changed files with 46 additions and 50 deletions
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@ -4,6 +4,7 @@ import Pantograph.Protocol
 import Pantograph.Serial
 import Lean.Environment
 import Lean.Replay
+import Lean.Util.Path

 open Lean
 open Pantograph
@ -130,17 +131,19 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
      } }
    | _ => pure core
  let result ← if args.source?.getD false then
-      let srcSearchPath ← initSrcSearchPath
-      let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·)
+      try
+        let sourceUri? ← module?.bindM (Server.documentUriFromModule? ·)
        let declRange? ← findDeclarationRanges? name
        let sourceStart? := declRange?.map (·.range.pos)
        let sourceEnd? := declRange?.map (·.range.endPos)
        .pure {
          result with
-        sourceUri?,
+          sourceUri? := sourceUri?.map (toString ·),
          sourceStart?,
          sourceEnd?,
        }
+      catch _e =>
+        .pure result
    else
      .pure result
  return result
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@ -69,7 +69,7 @@ def createCoreContext (options: Array String): IO Core.Context := do
@[export pantograph_create_core_state]
 def createCoreState (imports: Array String): IO Core.State := do
  let env ← Lean.importModules
-    (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
+    (imports := imports.map (λ str => { module := str.toName }))
    (opts := {})
    (trustLevel := 1)
    (loadExts := true)
--- a/Test/Delate.lean
+++ b/Test/Delate.lean
@ -51,7 +51,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
    ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"),
    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :i)"),
-    ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"),
+    ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.20) (:mv _uniq.21) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.15) (:lit 5) (:mv _uniq.16)))"),
  ]
  entries.foldlM (λ suites (source, levels, target) =>
    let termElabM := do
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@ -96,10 +96,10 @@ def test_symbol_location (env : Environment) : TestT IO Unit := do

    -- Extraction of source doesn't work for symbols in `Init` for some reason
    checkTrue "file" result.sourceUri?.isNone
-    checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
-    checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88
+    checkEq "sourceStart" (result.sourceStart?.map (·.column)) <| .some 0
+    checkEq "sourceEnd" (result.sourceEnd?.map (·.column)) <| .some 88
    let { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩
-    checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
+    checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero", "Init.Grind.Tactics"]
    checkTrue "constNames" $ constNames.contains "Nat.succ_add"

 def test_matcher (env : Environment) : TestT IO Unit := do
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@ -104,7 +104,7 @@ example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
  simp
 def test_tactic_timeout : Test := do
  step "goal.start" ({ expr := "(1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3" }: Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.319" }: Protocol.GoalStartResult)
+   ({ stateId := 0, root := "_uniq.355" }: Protocol.GoalStartResult)
  -- timeout of 10 milliseconds
  step "options.set" ({ timeout? := .some 10 } : Protocol.OptionsSet)
   ({ }: Protocol.OptionsSetResult)
@ -277,9 +277,9 @@ def test_frontend_process_sorry : Test := do
 def test_import_open : Test := do
  let header := "import Init\nopen Nat\nuniverse u"
  let goal1: Protocol.Goal := {
-    name := "_uniq.67",
+    name := "_uniq.77",
    target := { pp? := .some "n + 1 = n.succ" },
-    vars := #[{ name := "_uniq.66", userName := "n", type? := .some { pp? := .some "Nat" }}],
+    vars := #[{ name := "_uniq.76", userName := "n", type? := .some { pp? := .some "Nat" }}],
  }
  step "frontend.process"
    ({
@ -294,7 +294,7 @@ def test_import_open : Test := do
     ],
   }: Protocol.FrontendProcessResult)
  step "goal.start" ({ expr := "∀ (n : Nat), n + 1 = Nat.succ n"} : Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.65" }: Protocol.GoalStartResult)
+   ({ stateId := 0, root := "_uniq.75" }: Protocol.GoalStartResult)
  step "goal.tactic" ({ stateId := 0, tactic? := .some "intro n" }: Protocol.GoalTactic)
   ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult)
  step "goal.tactic" ({ stateId := 1, tactic? := .some "apply add_one" }: Protocol.GoalTactic)
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@ -25,8 +25,8 @@ def test_instantiate_mvar: TestM Unit := do
      addTest $ assertUnreachable e
      return ()
  let t ← Lean.Meta.inferType expr
-  addTest $ LSpec.check "typing" ((toString (← serializeExpressionSexp t)) =
-    "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))")
+  checkEq "typing" (toString (← serializeExpressionSexp t))
+    "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.15) (:lit 5) (:mv _uniq.16)))"
  return ()

 def startProof (expr: String): TestM (Option GoalState) := do
@ -118,8 +118,9 @@ def test_m_couple_simp: TestM Unit := do
  let serializedState1 ← state1.serializeGoals (options := { ← read with printDependentMVars := true })
  addTest $ LSpec.check "apply Nat.le_trans" (serializedState1.map (·.target.pp?) =
    #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
+  let n := state1.goals[2]!
  addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) =
-    #[#["_uniq.38"], #["_uniq.38"], #[]])
+    #[#[toString n.name], #[toString n.name], #[]])

  let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
    | .success state _ => pure state
@ -158,10 +159,10 @@ def test_m_couple_simp: TestM Unit := do
      addTest $ assertUnreachable "(5 root)"
      return ()
  let rootStr: String := toString (← Lean.Meta.ppExpr root)
-  addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
+  checkEq "(5 root)" rootStr "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
  let unfoldedRoot ←  unfoldAuxLemmas root
-  addTest $ LSpec.check "(5 root)" ((toString (← Lean.Meta.ppExpr unfoldedRoot)) =
-    "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
+  checkEq "(5 root)" (toString (← Lean.Meta.ppExpr unfoldedRoot))
+    "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
  return ()

 def test_proposition_generation: TestM Unit := do
@ -258,7 +259,7 @@ def test_partial_continuation: TestM Unit := do

  -- Continuation should fail if the state does not exist:
  match state0.resume coupled_goals with
-  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope")
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.44, _uniq.45, _uniq.42, _uniq.51] are not in scope")
  | .ok _ => addTest $ assertUnreachable "(continuation failure)"
  -- Continuation should fail if some goals have not been solved
  match state2.continue state1 with
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@ -7,9 +7,6 @@ open Lean

 namespace Pantograph.Test.Serial

-def tempPath : IO System.FilePath := do
-  Prod.snd <$> IO.FS.createTempFile
-
 structure MultiState where
  coreContext : Core.Context
  env: Environment
@ -35,7 +32,7 @@ def test_environment_pickling : TestM Unit := do
  let coreDst : Core.State := { env := ← getEnv }

  let name := `mystery
-  let envPicklePath ← tempPath
+  IO.FS.withTempFile λ _ envPicklePath => do
  let ((), _) ← runCoreM coreSrc do
    let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default
    let value: Expr := .lam `p (.sort 0) (.lam `h (.bvar 0) (.bvar 0) .default) .default
@ -56,13 +53,10 @@ def test_environment_pickling : TestM Unit := do
    let anotherName := `mystery2
    checkTrue s!"Doesn't have symbol {anotherName}" (env'.find? anotherName).isNone

-  IO.FS.removeFile envPicklePath
-
 def test_goal_state_pickling_simple : TestM Unit := do
  let coreSrc : Core.State := { env := ← getEnv }
  let coreDst : Core.State := { env := ← getEnv }
-  let statePath ← tempPath
-
+  IO.FS.withTempFile λ _ statePath => do
  let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default
  let stateGenerate : MetaM GoalState := runTermElabMInMeta do
    GoalState.create type
@ -78,8 +72,6 @@ def test_goal_state_pickling_simple : TestM Unit := do
    let types ← metaM.run'
    checkTrue "Goals" $ types[0]!.equal type

-  IO.FS.removeFile statePath
-
 structure Test where
  name : String
  routine: TestM Unit
--- a/flake.lock
+++ b/flake.lock
@ -5,11 +5,11 @@
        "nixpkgs-lib": "nixpkgs-lib"
      },
      "locked": {
-        "lastModified": 1743550720,
-        "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=",
+        "lastModified": 1749398372,
+        "narHash": "sha256-tYBdgS56eXYaWVW3fsnPQ/nFlgWi/Z2Ymhyu21zVM98=",
        "owner": "hercules-ci",
        "repo": "flake-parts",
-        "rev": "c621e8422220273271f52058f618c94e405bb0f5",
+        "rev": "9305fe4e5c2a6fcf5ba6a3ff155720fbe4076569",
        "type": "github"
      },
      "original": {
@ -44,11 +44,11 @@
        ]
      },
      "locked": {
-        "lastModified": 1743534244,
-        "narHash": "sha256-WnoYs2iyrfgh35eXErCOyos8E2YbW3LT1xm/EtT88/k=",
+        "lastModified": 1750275702,
+        "narHash": "sha256-CpwSdtwvrQCR+ZfXZweFHJMG583EYijCRGEeGrgBsjU=",
        "owner": "lenianiva",
        "repo": "lean4-nix",
-        "rev": "5eb7f03be257e327fdb3cca9465392e68dc28a4d",
+        "rev": "95a315f6e7d5e463090ae4977d5e2e6c3b4ef0d0",
        "type": "github"
      },
      "original": {
@ -59,11 +59,11 @@
    },
    "nixpkgs": {
      "locked": {
-        "lastModified": 1743975612,
-        "narHash": "sha256-o4FjFOUmjSRMK7dn0TFdAT0RRWUWD+WsspPHa+qEQT8=",
+        "lastModified": 1750151854,
+        "narHash": "sha256-3za+1J9FifMetO7E/kwgyW+dp+8pPBNlWKfcBovnn6M=",
        "owner": "nixos",
        "repo": "nixpkgs",
-        "rev": "a880f49904d68b5e53338d1e8c7bf80f59903928",
+        "rev": "ad5c70bcc5cc5178205161b7a7d61a6e80f6d244",
        "type": "github"
      },
      "original": {
@ -75,11 +75,11 @@
    },
    "nixpkgs-lib": {
      "locked": {
-        "lastModified": 1743296961,
-        "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=",
+        "lastModified": 1748740939,
+        "narHash": "sha256-rQaysilft1aVMwF14xIdGS3sj1yHlI6oKQNBRTF40cc=",
        "owner": "nix-community",
        "repo": "nixpkgs.lib",
-        "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa",
+        "rev": "656a64127e9d791a334452c6b6606d17539476e2",
        "type": "github"
      },
      "original": {
--- a/2
+++ b/2
@ -1 +1 @@
-leanprover/lean4:v4.19.0
+leanprover/lean4:v4.20.1