leanprover-community
current repl maybe cannot recognize mathcal letter?
When I was testing repl using the following example (it's actually the predefined theorem Metric.uniformity_basis_dist in mathlib4 Mathlib/Topology/MetricSpace/PseudoMetric.lean):
import Mathlib
open Set Filter TopologicalSpace Bornology
open scoped BigOperators ENNReal NNReal Uniformity Topology
universe u v w
variable {α : Type u} {β : Type v} {X ι : Type*}
variable [PseudoMetricSpace α]
open Lean Meta Qq Function
variable {x y z : α} {δ ε ε₁ ε₂ : ℝ} {s : Set α}
open Metric
example {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
(𝓤 α).HasBasis (fun _ : ℕ => True) fun n : ℕ => { p : α × α | dist p.1 p.2 < r ^ n } :=
Metric.mk_uniformity_basis (fun _ _ => pow_pos h0 _) fun _ε ε0 =>
let ⟨n, hn⟩ := exists_pow_lt_of_lt_one ε0 h1
⟨n, trivial, hn.le⟩
The above proof gets no warning or error message in interaction mode in vscode.
But when I test them via repl, I got the following feedback
> lake exe repl
{"cmd": "import Mathlib\nopen Set Filter TopologicalSpace Bornology\nopen scoped BigOperators ENNReal NNReal Uniformity Topology\nuniverse u v w\nvariable {\u03b1 : Type u} {\u03b2 : Type v} {X \u03b9 : Type*}\nvariable [PseudoMetricSpace \u03b1]\nopen Lean Meta Qq Function\nvariable {x y z : \u03b1} {\u03b4 \u03b5 \u03b5\u2081 \u03b5\u2082 : \u211d} {s : Set \u03b1}\nopen Metric\n"}
{"env": 0}
{"cmd": "example :\n (\ud835\udce4 \u03b1).HasBasis (fun \u03b5 : \u211d => 0 < \u03b5) fun \u03b5 => { p : \u03b1 \u00d7 \u03b1 | dist p.1 p.2 < \u03b5 } := by\n rw [toUniformSpace_eq]\n exact UniformSpace.hasBasis_ofFun (exists_gt _) _ _ _ _ _\n", "env": 0}
{"messages":
[{"severity": "error",
"pos": {"line": 2, "column": 5},
"endPos": null,
"data": "expected token"}],
"env": 1}
The "pos" in error message indicates that the error occurred due to the mathcal character 𝓤. I tried another example
import Mathlib
open Set Filter TopologicalSpace Bornology
open scoped BigOperators ENNReal NNReal Uniformity Topology
universe u v w
variable {α : Type u} {β : Type v} {X ι : Type*}
variable [PseudoMetricSpace α]
open Lean Meta Qq Function
variable {x y z : α} {δ ε ε₁ ε₂ : ℝ} {s : Set α}
open Metric
example {p : α → Prop} :
(∀ᶠ y in 𝓝 x, p y) ↔ ∃ ε > 0, ∀ ⦃y⦄, dist y x < ε → p y :=
mem_nhds_iff
and got the same error message in repl
> lake exe repl
{"cmd": "import Mathlib\nopen Set Filter TopologicalSpace Bornology\nopen scoped BigOperators ENNReal NNReal Uniformity Topology\nuniverse u v w\nvariable {\u03b1 : Type u} {\u03b2 : Type v} {X \u03b9 : Type*}\nvariable [PseudoMetricSpace \u03b1]\nopen Lean Meta Qq Function\nvariable {x y z : \u03b1} {\u03b4 \u03b5 \u03b5\u2081 \u03b5\u2082 : \u211d} {s : Set \u03b1}\nopen Metric\n"}
{"env": 0}
{"cmd": "example {p : \u03b1 \u2192 Prop} :\n (\u2200\u1da0 y in \ud835\udcdd x, p y) \u2194 \u2203 \u03b5 > 0, \u2200 \u2983y\u2984, dist y x < \u03b5 \u2192 p y :=\n mem_nhds_iff\n", "env": 0}
{"messages":
[{"severity": "error",
"pos": {"line": 2, "column": 13},
"endPos": null,
"data": "expected token"}],
"env": 1}
The error message also indicates the error occurred due to a mathcal letter '𝓝', therefore I guess the issue is about the unicode transformation on mathcal letter that the repl cannot handle.
If my guess is correct? How can I solve this issue? Thanks!
I solved the issue. It occurred when I encoded the string before feed into repl using python function json.dumps without setting ensure_ascii=False.
I also encountered a similar problem，like the figure below. And the error message is due to '≤'.
Seems you have solved the issues, what is your input format of repl finally？
I also encountered a similar problem，like the figure below. And the error message is due to '≤'.
Seems you have solved the issues, what is your input format of repl finally？
How did you feed the proof sketch into the repl? If you just copy the sketch into repl via terminal, will you meet the same issue?
I also encountered a similar problem，like the figure below. And the error message is due to '≤'.
Seems you have solved the issues, what is your input format of repl finally？
How did you feed the proof sketch into the repl? If you just copy the sketch into repl via terminal, will you meet the same issue?
Yes, I just copy the sketch into repl via terimal, then encountered the issue.
I also encountered a similar problem，like the figure below. And the error message is due to '≤'.
How did you feed the proof sketch into the repl? If you just copy the sketch into repl via terminal, will you meet the same issue?
Yes, I just copy the sketch into repl via terimal, then encountered the issue.
I also encountered a similar problem，like the figure below. And the error message is due to '≤'.
How did you feed the proof sketch into the repl? If you just copy the sketch into repl via terminal, will you meet the same issue?
Yes, I just copy the sketch into repl via terimal, then encountered the issue.
No idea why you can't, maybe you can check the input method on your computer.
Thanks a lot. I am new to Lean and Lake, I want to know that did you change the settings of the repo, like "lakefile.lean, lake-manifest.json" files, or just clone the repo and run "lake exe repl"?
Nope, I just followed README. I think your repl works normally, you can check your proof sketch in user interactive mode in vscode.
As a follow up: I faced a similar issue with imports, for me it was a version mismatch in the lean toolchain between the lake environment I was running the repl from and the version that was used to build the lean repl.
