diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index bc3c3a4..fddd6da 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -8,6 +8,22 @@ import REPL.Util.Pickle open Lean Elab +namespace Lean.Elab.Command + +@[inline] def CommandElabM.run (x : CommandElabM α) (ctx : Context) (s : State) : EIO Exception (α × State) := + (x ctx).run s + +@[inline] def CommandElabM.run' (x : CommandElabM α) (ctx : Context) (s : State) : EIO Exception α := + Prod.fst <$> x.run ctx s + +@[inline] def CommandElabM.toIO (x : CommandElabM α) (ctx : Context) (s : State) : IO (α × State) := do + match (← (x.run ctx s).toIO') with + | Except.error (Exception.error _ msg) => throw <| IO.userError (← msg.toString) + | Except.error (Exception.internal id _) => throw <| IO.userError <| "internal exception #" ++ toString id.idx + | Except.ok a => return a + +end Lean.Elab.Command + namespace REPL /-- @@ -20,7 +36,8 @@ structure CommandSnapshot where namespace CommandSnapshot -open Lean.Elab.Command in +open Lean.Elab.Command + /-- A copy of `Command.State` with the `Environment`, caches, and logging omitted. -/ structure CompactableCommandSnapshot where -- env : Environment @@ -35,6 +52,15 @@ structure CompactableCommandSnapshot where open System (FilePath) +/-- +Run a `CommandElabM` monadic function in the current `ProofSnapshot`, +updating the `Command.State`. +-/ +def runCommandElabM (p : CommandSnapshot) (t : CommandElabM α) : IO (α × CommandSnapshot) := do + let (a, cmdState) ← (CommandElabM.toIO · p.cmdContext p.cmdState) do t + return (a, { p with cmdState }) + + /-- Pickle a `CommandSnapshot`, discarding closures and non-essential caches. @@ -57,10 +83,14 @@ def unpickle (path : FilePath) : IO (CommandSnapshot × CompactedRegion) := unsa _root_.unpickle (Array Import × PHashMap Name ConstantInfo × CompactableCommandSnapshot × Command.Context) path let env ← (← importModules imports {} 0).replay (HashMap.ofList map₂.toList) - let p' := + let p' : CommandSnapshot := { cmdState := { cmdState with env } cmdContext } - return (p', region) + let (_, p'') ← p'.runCommandElabM do + for o in ← getOpenDecls do + if let .simple ns _ := o then do + activateScoped ns + return (p'', region) end CommandSnapshot @@ -228,7 +258,7 @@ def unpickle (path : FilePath) : IO (ProofSnapshot × CompactedRegion) := unsafe Core.Context × Meta.State × CompactableMetaContext × Term.State × CompactableTermContext × Tactic.State × Tactic.Context) path let env ← (← importModules imports {} 0).replay (HashMap.ofList map₂.toList) - let p' := + let p' : ProofSnapshot := { coreState := { coreState with env } coreContext metaState @@ -237,6 +267,10 @@ def unpickle (path : FilePath) : IO (ProofSnapshot × CompactedRegion) := unsafe termContext := { termContext with } tacticState tacticContext } - return (p', region) + let (_, p'') ← p'.runCoreM do + for o in ← getOpenDecls do + if let .simple ns _ := o then + activateScoped ns + return (p'', region) end ProofSnapshot diff --git a/test/Mathlib/test/H20231207.in b/test/Mathlib/test/H20231207.in deleted file mode 100644 index 060327c..0000000 --- a/test/Mathlib/test/H20231207.in +++ /dev/null @@ -1,33 +0,0 @@ -{"cmd": "import Mathlib\n\nopen Nat\nopen Real\nopen BigOperators"} - -{"cmd" : "theorem problem (x₁ x₂ x₃ : ℝ)\n (f : ℝ → ℝ)\n (h₀ : ∀ x, f x = Real.sqrt 2014 * x^3 - 4029 * x^2 + 2)\n (h₁ : f x₁ = 0)\n (h₂ : f x₂ = 0)\n (h₃ : f x₃ = 0)\n (h₄ : x₁ < x₂ ∧ x₂ < x₃) :\n ∃ (k : ℝ), x₂ * (x₁ + x₃) = k := by sorry", "env": 0} - -{"tactic": "have h2014 : (2014:ℝ) * Real.sqrt 2014 = (Real.sqrt 2014)^3 := by sorry", "proofState": 0} - -{"tactic": "have hfy (x y :ℝ) (hy : x = y / Real.sqrt 2014) : f x = y^3 / 2014 - 4029 * y^2 / 2014 + 2 := by sorry", "proofState": 1} - -{"tactic": "let g (y : ℝ) := y^3 - 4029 * y^2 + 4028", "proofState": 2} - -{"tactic": "have hfg (y : ℝ) : f (y / Real.sqrt 2014) = 0 ↔ g y = 0 := by sorry", "proofState": 3} - -{"tactic": "have hg1 : g 1 = 0 := by sorry", "proofState": 4} - -{"tactic": "let g' (y : ℝ) := 1 * y * y + -4028 * y + -4028", "proofState": 5} - -{"tactic": "have hg_fac (y : ℝ) : g y = (y-1)*g' y := by sorry", "proofState": 6} - -{"tactic": "let D := 16240896", "proofState": 7} - -{"tactic": "have hdiscr : discrim (1:ℝ) (-4028) (-4028) = Real.sqrt D * Real.sqrt D := by sorry", "proofState": 8} - -{"tactic": "let y₁ : ℝ := (4028 - Real.sqrt D)/2", "proofState": 9} - -{"tactic": "let y₃ : ℝ := (4028 + Real.sqrt D)/2", "proofState": 10} - -{"tactic": "have : g' y₁ = 0 := by sorry", "proofState": 11} - -{"tactic": "have hgy₁ : g y₁ = 0 := by sorry", "proofState": 12} - -{"tactic": "have : g' y₃ = 0 := by sorry", "proofState": 13} - -{"tactic": "sorry", "proofState": 14} diff --git a/test/Mathlib/test/H20231207.lean b/test/Mathlib/test/H20231207.lean deleted file mode 100644 index 4123268..0000000 --- a/test/Mathlib/test/H20231207.lean +++ /dev/null @@ -1,37 +0,0 @@ -import Mathlib - -open Nat -open Real -open BigOperators - -theorem problem (x₁ x₂ x₃ : ℝ) - (f : ℝ → ℝ) - (h₀ : ∀ x, f x = Real.sqrt 2014 * x^3 - 4029 * x^2 + 2) - (h₁ : f x₁ = 0) - (h₂ : f x₂ = 0) - (h₃ : f x₃ = 0) - (h₄ : x₁ < x₂ ∧ x₂ < x₃) : - ∃ (k : ℝ), x₂ * (x₁ + x₃) = k := by - -- -- 3.34s - have h2014 : (2014:ℝ) * Real.sqrt 2014 = (Real.sqrt 2014)^3 := by sorry - have hfy (x y :ℝ) (hy : x = y / Real.sqrt 2014) : f x = y^3 / 2014 - 4029 * y^2 / 2014 + 2 := by sorry - let g (y : ℝ) := y^3 - 4029 * y^2 + 4028 - have hfg (y : ℝ) : f (y / Real.sqrt 2014) = 0 ↔ g y = 0 := by sorry - have hg1 : g 1 = 0 := by sorry - let g' (y : ℝ) := 1 * y * y + -4028 * y + -4028 - have hg_fac (y : ℝ) : g y = (y-1)*g' y := by sorry - let D := 16240896 - -- 3.707s - have hdiscr : discrim (1:ℝ) (-4028) (-4028) = Real.sqrt D * Real.sqrt D := by sorry - -- 3.722s - let y₁ : ℝ := (4028 - Real.sqrt D)/2 - -- 3.747s - let y₃ : ℝ := (4028 + Real.sqrt D)/2 - -- 3.712s - have : g' y₁ = 0 := by sorry - -- 4.454s - have hgy₁ : g y₁ = 0 := by sorry - -- 5.342s - have : g' y₃ = 0 := by sorry - -- -- 6.475s - sorry diff --git a/test/Mathlib/test/H20231207_2.in b/test/Mathlib/test/H20231207_2.in deleted file mode 100644 index 8ed9e56..0000000 --- a/test/Mathlib/test/H20231207_2.in +++ /dev/null @@ -1,4 +0,0 @@ -{"cmd": "import Mathlib\n\nopen BigOperators\nopen Real\nopen Nat\n\n"} - -{"cmd": "theorem problem (x₁ x₂ x₃ : ℝ)\n (f : ℝ → ℝ)\n (h₀ : ∀ x, f x = Real.sqrt 2014 * x^3 - 4029 * x^2 + 2)\n (h₁ : f x₁ = 0)\n (h₂ : f x₂ = 0)\n (h₃ : f x₃ = 0)\n (h₄ : x₁ < x₂ ∧ x₂ < x₃) :\n ∃ (k : ℝ), x₂ * (x₁ + x₃) = k := by\n -- -- 3.34s\n have h2014 : (2014:ℝ) * Real.sqrt 2014 = (Real.sqrt 2014)^3 := by sorry\n have hfy (x y :ℝ) (hy : x = y / Real.sqrt 2014) : f x = y^3 / 2014 - 4029 * y^2 / 2014 + 2 := by sorry\n let g (y : ℝ) := y^3 - 4029 * y^2 + 4028\n have hfg (y : ℝ) : f (y / Real.sqrt 2014) = 0 ↔ g y = 0 := by sorry\n have hg1 : g 1 = 0 := by sorry\n let g' (y : ℝ) := 1 * y * y + -4028 * y + -4028\n have hg_fac (y : ℝ) : g y = (y-1)*g' y := by sorry\n let D := 16240896\n -- 3.707s\n have hdiscr : discrim (1:ℝ) (-4028) (-4028) = Real.sqrt D * Real.sqrt D := by sorry\n -- 3.722\n let y₁ : ℝ := (4028 - Real.sqrt D)/2\n -- 3.747\n let y₃ : ℝ := (4028 + Real.sqrt D)/2\n -- 3.712\n have : g' y₁ = 0 := by sorry\n -- 4.454\n have hgy₁ : g y₁ = 0 := by sorry\n -- 5.342\n have : g' y₃ = 0 := by sorry\n -- have hgy₃ : g y₃ = 0 := by sorry\n -- have : 4026 < Real.sqrt D := by sorry\n -- have hy₁_lt : y₁ < 1 := by sorry\n -- -- 12.737s\n -- have hy₃_gt : 1 < y₃ := by sorry\n -- let P : Cubic ℝ := ⟨Real.sqrt 2014, -4029, 0, 2⟩\n -- have hP (x : ℝ) : x ∈ P.roots.toFinset ↔ f x = 0 := by sorry\n -- have hnodup : Multiset.Nodup {x₁, x₂, x₃} := by sorry\n -- have hP_roots {a b c : ℝ} (ha : f a = 0) (hb : f b = 0) (hc : f c = 0) (hab : a < b) (hbc: b < c) : P.roots.toFinset = {a, b, c} := by sorry\n -- have hy₁_lt' : y₁ / Real.sqrt 2014 < 1 / Real.sqrt 2014 := by sorry\n -- have hy₃_lt' : 1 / Real.sqrt 2014 < y₃ / Real.sqrt 2014 := by sorry\n -- have heq : ({x₁, x₂, x₃} : Finset ℝ) = {y₁/Real.sqrt 2014, 1/Real.sqrt 2014, y₃ / Real.sqrt 2014} := by sorry\n -- have hmin {a b c : ℝ} (hab : a < b) (hbc : b < c) : a = Finset.min' {a,b,c} (Finset.insert_nonempty _ _) := by sorry\n -- have hx₁ : x₁ = y₁/Real.sqrt 2014 := by sorry\n -- have hmax {a b c : ℝ} (hab : a < b) (hbc : b < c) : c = Finset.max' {a,b,c} (Finset.insert_nonempty _ _) := by sorry\n -- have hx₃ : x₃ = y₃/Real.sqrt 2014 := by sorry\n -- have hx₂ : x₂ = 1/Real.sqrt 2014 := by sorry\n sorry\n", "env": 0} - diff --git a/test/Mathlib/test/H20231215_2.expected.out b/test/Mathlib/test/H20231215_2.expected.out index 6eed89f..1a83bcf 100644 --- a/test/Mathlib/test/H20231215_2.expected.out +++ b/test/Mathlib/test/H20231215_2.expected.out @@ -2,9 +2,9 @@ {"sorries": [{"proofState": 0, - "pos": {"line": 2, "column": 29}, - "goal": "⊢ factorial 9 % 10 = 0", - "endPos": {"line": 2, "column": 34}}], + "pos": {"line": 2, "column": 20}, + "goal": "⊢ 9! % 10 = 0", + "endPos": {"line": 2, "column": 25}}], "messages": [{"severity": "warning", "pos": {"line": 1, "column": 8}, diff --git a/test/Mathlib/test/H20231215_2.in b/test/Mathlib/test/H20231215_2.in index 64b7c34..72323c8 100644 --- a/test/Mathlib/test/H20231215_2.in +++ b/test/Mathlib/test/H20231215_2.in @@ -1,3 +1,3 @@ {"unpickleEnvFrom": "test/H20231215.olean"} -{"cmd": "theorem mathd_numbertheory_739 :\n factorial 9 % 10 = 0 := by sorry", "env": 0} +{"cmd": "theorem mathd_numbertheory_739 :\n 9! % 10 = 0 := by sorry", "env": 0} diff --git a/test/pickle_open_scoped.expected.out b/test/pickle_open_scoped.expected.out new file mode 100644 index 0000000..df23507 --- /dev/null +++ b/test/pickle_open_scoped.expected.out @@ -0,0 +1,18 @@ +{"env": 0} + +{"env": 1} + +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 22}, + "goal": "⊢ ◾", + "endPos": {"line": 1, "column": 27}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 7}, + "endPos": {"line": 1, "column": 14}, + "data": "declaration uses 'sorry'"}], + "env": 2} + +{"env": 1} + diff --git a/test/pickle_open_scoped.in b/test/pickle_open_scoped.in index e268d6d..dafcbc6 100644 --- a/test/pickle_open_scoped.in +++ b/test/pickle_open_scoped.in @@ -1,13 +1,8 @@ -{"cmd": "namespace X"} +{"cmd": "import Lean"} -{"cmd": "def f (x : Nat) := x + 37", "env": 0} +{"cmd": "open Lean.Compiler", "env": 0} -{"cmd": "scoped notation:10000 n \"!\" => f n", "env": 1} +{"cmd": "unsafe example : ◾ := sorry", "env": 1} -{"cmd": "end X", "env": 2} +{"pickleTo": "test/f.olean", "env": 1} -{"cmd": "open X", "env": 3} - -{"cmd": "example : 39 = 2 ! := rfl", "env": 4} - -{"pickleTo": "test/f.olean", "env": 4} diff --git a/test/pickle_open_scoped_2.expected.out b/test/pickle_open_scoped_2.expected.out new file mode 100644 index 0000000..f21692d --- /dev/null +++ b/test/pickle_open_scoped_2.expected.out @@ -0,0 +1,14 @@ +{"env": 0} + +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 22}, + "goal": "⊢ ◾", + "endPos": {"line": 1, "column": 27}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 7}, + "endPos": {"line": 1, "column": 14}, + "data": "declaration uses 'sorry'"}], + "env": 1} + diff --git a/test/pickle_open_scoped_2.in b/test/pickle_open_scoped_2.in index 24efb5c..6b587fc 100644 --- a/test/pickle_open_scoped_2.in +++ b/test/pickle_open_scoped_2.in @@ -1,3 +1,3 @@ {"unpickleEnvFrom": "test/f.olean"} -{"cmd": "example : 39 = 2 ! := rfl", "env": 1} +{"cmd": "unsafe example : ◾ := sorry", "env": 0} diff --git a/test/pickle_scoped_notation.in b/test/pickle_scoped_notation.in new file mode 100644 index 0000000..d0105bc --- /dev/null +++ b/test/pickle_scoped_notation.in @@ -0,0 +1,20 @@ +{"cmd": "import Lean"} + +{"cmd": "namespace X", "env": 0} + +{"cmd": "def f (x : Nat) := x + 37", "env": 1} + +{"cmd": "scoped notation:10000 n \"!\" => f n", "env": 2} + +{"cmd": "end X", "env": 3} + +{"cmd": "open X", "env": 4} + +{"cmd": "example : 39 = 2 ! := rfl", "env": 5} + +{"cmd": "open Lean.Compiler", "env": 5} + +{"cmd": "unsafe example : ◾ := sorry", "env": 7} + +{"pickleTo": "test/f.olean", "env": 7} + diff --git a/test/pickle_scoped_notation_2.in b/test/pickle_scoped_notation_2.in new file mode 100644 index 0000000..ecb15e8 --- /dev/null +++ b/test/pickle_scoped_notation_2.in @@ -0,0 +1,3 @@ +{"unpickleEnvFrom": "test/f.olean"} + +{"cmd": "example : 39 = 2 ! := rfl", "env": 0}