Stream: Coq users

Topic: Adding doc comments breaks coqc


view this post on Zulip Joshua Grosso (Aug 14 2021 at 23:14):

Are there any known issues where PG can successfully work with a file that coqc dies on (with a lexer error), unless the doc comments are removed, in which case coqc works as well?

view this post on Zulip Joshua Grosso (Aug 15 2021 at 01:01):

Turns out I had some double-quotes in my doc comments that I forgot to close. It still seems weird to me that the code itself would be affected... I'm curious what everyone else thinks.

view this post on Zulip Paolo Giarrusso (Aug 15 2021 at 11:37):

Is this https://github.com/ProofGeneral/PG/issues/37 ?

view this post on Zulip Paolo Giarrusso (Aug 15 2021 at 11:39):

Architecturally, this seems a consequence of ProofGeneral having its separate parser, because Coq did not expose one when ProofGeneral was written — see also https://github.com/ProofGeneral/PG/issues/58.

view this post on Zulip Joshua Grosso (Aug 15 2021 at 19:14):

Paolo Giarrusso said:

Is this https://github.com/ProofGeneral/PG/issues/37 ?

A ha, it might be (I swear I searched the coq and PG issue lists, idk why it didn't come up :grimacing:) Thanks!

view this post on Zulip Paolo Giarrusso (Aug 16 2021 at 12:47):

I knew this existed and yet it took me forever to find it, so don't worry.


Last updated: Jan 29 2023 at 05:03 UTC