Running `tests/lean/run/treemap.lean` with `-D Elab.async=false` causes errors

[zwarich]

On c2876a1, running

time build/release/stage1/bin/lean tests/lean/run/treemap.lean -D Elab.async=false

gives errors like this:

tests/lean/run/treemap.lean:550:0: warning: declaration uses 'sorry'
⟨2, 4⟩
tests/lean/run/treemap.lean:549:0: error: ❌️ Docstring on `#guard_msgs` does not match generated message:

warning: declaration uses 'sorry'
---
info: ⟨2, 4⟩
tests/lean/run/treemap.lean:558:0: warning: declaration uses 'sorry'
(2, 4)
tests/lean/run/treemap.lean:557:0: error: ❌️ Docstring on `#guard_msgs` does not match generated message:

warning: declaration uses 'sorry'
---
info: (2, 4)
tests/lean/run/treemap.lean:606:0: warning: declaration uses 'sorry'
2
tests/lean/run/treemap.lean:605:0: error: ❌️ Docstring on `#guard_msgs` does not match generated message:

warning: declaration uses 'sorry'
...

These errors do not occur without -D Elab.async=false.

[Kha]

I'm not sure we want to guarantee stability of message ordering under this option