Only the first line of the output HTML file is interactive

[agrarpan]

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)

Am I doing something wrong?
Thanks!

[agrarpan]

After going through the codebase a little, it seems like this is related to rocq-archive/coq-serapi#212. Switching to coq8.15 fixes the issue. I still have the issue on coq8.10