Displaying Proof Goals with Alectryon

This post exercises the Alectryon integration: every coq and rocq fence below is executed by Coq, and the proof state after each sentence is recorded. Not every sentence produces a state (the closing Qed., for instance, produces none), so only the steps that do are marked with a trailing dot. Hover a marked step, or tap it, to reveal the goals it produces.

A trivial proof

Goal True /\ True.True /\ True
  split.True
True
  -True exact I.
  -True exact I.
Qed.

The same proof written with a rocq fence

The rocq fence is normalized to alectryon just like the coq fence, so it is executed in the same session.

Goal 1 + 1 = 2.1 + 1 = 2
Proof.1 + 1 = 2 reflexivity. Qed.

Both blocks share one Coq session, in source order.