Skip to content

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

@agrarpan

Description

@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!

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions