Prose inside a definition

[greedy]

I'd like to be able to write prose inside of record and inductive definitions for the purposes of discussing individual fields or constructors. When I tried to do this, I got an error because alectryon submitted each snippet between the (*| |*) to coq separately as if it were a complete sentence.

Processing

Inductive foo :=
(*| For `foo`, `bar`, means ... |*)
bar : nat -> foo.

with alectryon yields

ex.v:1: (ERROR/3) Coq raised an exception:
  > Syntax error: '.' expected after [gallina] (in [vernac_aux]).
The offending chunk is delimited by >>>…<<< below:
  > Inductive foo :=>>><<<
Results past this point may be unreliable.
ex.v:1: (ERROR/3) Coq raised an exception:
  > Syntax error: illegal begin of vernac.
The offending chunk is delimited by >>>…<<< below:
  > >>>bar<<< : nat -> foo.
Results past this point may be unreliable.

I tried to see what it would take to fix this, but I started to get the impression that content between prose are complete Coq sentences might be a core assumption of alectryon's processing model.

This is also mentioned in #75 as a feature of coqdoc that is not supported by alectryon's coqdoc frontend.

[greedy]

Oh, I see now that this just happens with the sertop drivers. With coqc_time there is no error and it renders the HTML as I'd expect. So perhaps it's not a core assumption of alectryon but just of the sertop driver.

[cpitclaudel]

So perhaps it's not a core assumption of alectryon but just of the sertop driver.

Exactly right! It was a nice simplifying assumption early on to exclude this case, but I had to abandon it to support with coqc_time and other drivers/languages. We're currently working on a new Rocq driver without that issue.

How soon do you need this feature? I think it would be a few hours at most to fix up sertop to support this, but maybe the new driver will be enough?

[greedy]

It's not an urgent need. I'm using alectryon with sphinx to build documentation of my development and for now I'll use the coqc_time driver. I've got plenty of time before the end of this project so the rocq driver will probably be ready by then.

[cpitclaudel]

Perfect, we'll keep you posted!