search

leanprover-community / repl

A simple REPL for Lean 4, returning information about errors and sorries.
69 stars 16 forks source link

Infinite recursion on empty input #2

Closed gebner closed 1 year ago

gebner commented 1 year ago

I carelessly piped a single line into the repl and got infinite recursion in getLines. Input:

echo '{"cmd": "#eval \"Hello, world!\""}' | ./run
kim-em commented 1 year ago

Fixed (I discovered the same thing) in https://github.com/leanprover-community/repl/commit/11daea2ee742b512cc94b4a280849485254e592a.