Open ohyeat opened 9 months ago
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 '≤'. 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.
No idea why you can't, maybe you can check the input method on your computer.
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.
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.
When I was testing repl using the following example (it's actually the predefined theorem
Metric.uniformity_basis_dist
in mathlib4Mathlib/Topology/MetricSpace/PseudoMetric.lean
):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
The "pos" in error message indicates that the error occurred due to the mathcal character 𝓤. I tried another example
and got the same error message in repl
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!