Leanprover-community/repl has duplicate states after 4.12

Stream: general

[Andrew Wells]

I have more details in comments on Github (https://github.com/leanprover-community/repl/pull/57). TLDR; it seems using IO.processCommandsIncrementally is running everything twice resulting in duplicate proofStates. Is this expected? If so, is the duplication expected to be consistent moving forwards (so that I should just update the tests in repl)?

[Kim Morrison]

No sorry, this is a a breakage that I have not found time to address, and so haven't published a version of the REPL for 4.12 or later.

If you would like to look into this and try resolving the problem, I would love a PR!