[japgolly]

The code doesn't work. I pasted in the full code at the end into Lean Web, and it gives 4 errors and a warning (all in the lemmas).

[reinitctxoffset]

If you haven't already I'm dry a different version, minor versions can change a lot.