search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
236 stars 34 forks source link

Only the first line of the output HTML file is interactive #87

Open agrarpan opened 2 years ago

agrarpan commented 2 years ago

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 commented 2 years ago

After going through the codebase a little, it seems like this is related to https://github.com/ejgallego/coq-serapi/issues/212. Switching to coq8.15 fixes the issue. I still have the issue on coq8.10