search

cpitclaudel / alectryon

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

Alectryon coqdoc frontend bails on `(** printing ` directives #40

Closed mattam82 closed 3 years ago

mattam82 commented 3 years ago

Just use a .v file with

(** printing Derive %\coqdockw{Derive}% *)

coqdoc uses it to configure itself, so it doesn't appear in the output, while alectryon understands it as a comment. This produces a Coqdoc mismatch assertion failure.

cpitclaudel commented 3 years ago

Ah, good catch, thanks! Do you have a list of these special assertions?

mattam82 commented 3 years ago

I think there's only (** printing and (** remove printing

cpitclaudel commented 3 years ago

Should be fixed, I hope; can you check?

mattam82 commented 3 years ago

Yep, it works fine now! Remaining problem: (* begin hide *) (* end hide *) are not recognized, that would be very helpful to me to understand it as (* . none *)

mattam82 commented 3 years ago

image

lthms commented 3 years ago

On a related note, there is also (* begin details *) ((* begin details : Summary of the section *) is also valid) that has been added recently to coqdoc.

cpitclaudel commented 3 years ago

One problem with begin hide … end hide is that it doesn't respect sentences, so you can hide half of a sentence — Alectryon doesn't support that.

mattam82 commented 3 years ago

Could we have a leniency option that doesn't support "inline" hide? I'm not using that feature afaik.

cpitclaudel commented 3 years ago

Sure. I won't have time to implement it right away, but it should be easy. Look in cli.py, though maybe some of that code should move to a separate coqdoc.py..