Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
start974 opened this issue Jul 1, 2021 · 1 comment
Open

Comments

@start974
Copy link
Contributor

start974 commented Jul 1, 2021

(* 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
Copy link
Owner

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants