Joshua Grosso (Aug 14 2021 at 23:14): 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?
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.
Paolo Giarrusso (Aug 15 2021 at 11:37):Is this https://github.com/ProofGeneral/PG/issues/37 ?
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.
Joshua Grosso (Aug 15 2021 at 19:14):Paolo Giarrusso said:
A ha, it might be (I swear I searched the coq and PG issue lists, idk why it didn't come up :grimacing:) Thanks!
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: Apr 19 2024 at 22:01 UTC