You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hi, thanks for making this tool! I'm just getting started with it.
I have a file called proved_theorem.v which has:
Theorem trial: forall n: nat, 1 + n = S n.
Proof.
intros.
eauto.
Qed.
as its contents.
When I run alectryon --frontend coq --backend webpage proved_theorem.v -o proved_theorem.html, the resulting output file only has the interactive bubble on the line with the "Theorem". All the subsequent lines are missing the interactive bubbles.
(I do get
proved_theorem.v:(1:1)-(6:1): (WARNING/2) Orphaned message for sid b'0':
.proved_theorem.aux: No such file or directory)