Reduce binary size

[sullyj3]

On hold. We depend on import Lean via socket -> alloy -> lean. I don't think there's much to be done until lean 4's module system improves.

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Reducing.20executable.20size

---

Currently 87mb, which is ridiculous. We've eliminated batteries, so I think ever importing Lean or any submodule of Lean is what causes the blowup.

We're using two things from Lean:

• Lean.HashMap
  We can switch to Std.HashMap when it comes out. In the meantime we can just use an array of pairs, since the data is small.
• ToJson/FromJson
  Either vendor or replace with our own serialization depending on which is more complicated

[sullyj3]

Blocked on lean, possibly new module system will address this (see roadmap)