Eric Wieser

I have not at any point tried to build lean itself locally, and was relying on CI to do that. Presumably once this build passes, I can create a mathlib...

Build is full of failures with trivial goals that `simp` isn't closing: ```lean /home/runner/work/lean/lean/library/init/data/list/lemmas.lean:25:3: error: tactic failed, there are unsolved goals state: case list.cons α : Type u, t_hd :...

It's also possible that Python needs to improve its support for reading mutable buffers from files / streams without copying. It's not clear to me why there can't be a...

The problem here is specifically negative indices, right? Nice catch

Right, so it fails for indices where `0

I had a local patch, but the timings ended up way worse as a result of fixing it. I'll try to take another look

I've edited the issue text to cross out the cases we've deemed invalid, along with a reason.

@bashtage, I've no idea what `-bound % bound` actually does when `bound` is an unsigned integer

That last comment might be helpful written in the code.

As far as I can tell 20 is nonsense, `ret` cannot be `NULL` on that line.