Ruos

@semorrison Thanks for your prompt reply! I will try to find other ways to solve this issue.

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

> > > I also encountered a similar problem，like the figure below. And the error message is due to '**≤**'. > > > Seems you have solved the issues, what...

Nope, I just followed README. I think your repl works normally, you can check your proof sketch in user interactive mode in vscode.

**The memory of unused variable will not release anyway in repl, that's the biggest problem!** A more direct way to see what happes in repl: - Modify `./REPL/Main.lean` as follows:...

> what if you wait for 2 minutes or something. Does it still never get released? No, the memory wont release as long as the process is still alive

I just found a demonstration in functional programming in Lean tutorial and saw the following: > [Reference Counting and In-Place Updates](https://lean-lang.org/functional_programming_in_lean/programs-proofs/summary.html#reference-counting-and-in-place-updates) > Rather than using a tracing garbage collector, as...

Hi all, I find the way to implement tail recursion to replace repl loop, just modify two function definitions (`recordCommandSnapshot`, `repl`) in Main.lean as follows: ```lean /-- Only record the...

@FrederickPu This is the most interesting(or maybe annoying) part: the subprocess you create in python is not the exact the process executing `repl`, it actually executing `lake` (recall the launching...