feat: incremental elaboration of Verso documents

[david-christiansen]

Based on leanprover/lean4#3849

The API is still a bit fiddly, so this code needs some cleanup prior to merge

[david-christiansen]

@Kha - I think this is still using the framework in the intended manner, though I lifted out the hairy parts to a helper. I'm not totally satisfied by how the different monads interact, but couldn't immediately think of a nicer way.

Is this about how you'd imagined it being, or am I missing some low-hanging fruit for simplification?

[david-christiansen]

Note to self after call: check getAndResetMessageLog, that avoids double-reported diagnostics from incrementality

[david-christiansen]

OK, I think this is as ready as it's getting, though some items may not work until leanprover/lean4#3940. Once that's in, I'll try again, but this is already better than it was.