cpitclaudel / alectryon

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

Syntax error: illegal begin of vernac. -- with indented comments #48

Open start974 opened 3 years ago

start974 commented 3 years ago
(* commentaire *)

(*|
    test
|*)
$ python alectryon.py test.v --frontend="coq+rst" --backend="webpage"
!! Coq raised an exception:
       Syntax error: illegal begin of vernac.
   Results past this point may be unreliable.
   The offending chunk is delimited by >>>.<<< below:
       (* commentaire *)

        >>>test<<<

This error doesn't occur if there is no comment before, or if we remove the indentation in the "rst comment".

cpitclaudel commented 3 years ago

Good catch, thanks a lot. This test thing is supposed to be a blockquote, right?

The issue is that the Coq to reST translator produces this:

.. coq::

   (* commentaire *)

    test

I think the fix is to use an empty comment to reset indentation, yielding this translation:

.. coq::

   (* commentaire *)

..

    test

This fix can be applied by hand as well in the meantime.