Stream: Coq users

Topic: gappa generates .v file with dollar signs


view this post on Zulip MIchael Hennebry (Nov 10 2023 at 03:05):

I used coqc and gappa from the coq platform:
$ coqc --version
The Coq Proof Assistant, version 8.17.1
compiled with OCaml 4.14.1
$ gappa --version
Gappa 1.4.1
$
I've been getting dollar signs in .v files even though gappa's return codes have been zero.
I'd like to know what is going on and how to fix it.
The gappa command, one line, was
time gappa -Bcoq -Echange-threshold=0 -Eprecision=200 -Eno-auto-dichotomy refine43s.g > refine43s.v ; echo returned $?
Finding a minimal example reduced the number of dollar signs to one.
coqc chokes on it:
$ coqc refine43s.v
File "./refine43s.v", line 158, characters 18-19:
Error: Syntax Error: Lexer: Undefined token

Changing the dollar sign to an underbar
allows coqc to run to completion with
a return code of zero.

I've attached refine43s.g to this post. Note the single comment:
The dollar sign goes away if the constraint on the hint goes away.
Here is refine43s.g :
refine43s.g
Here is refine43s.v:
refine43s.v

view this post on Zulip MIchael Hennebry (Nov 13 2023 at 19:51):

From the lack of response, I gather this forum doesn't have anyone with sufficient gappa expertise. Could someone suggest a better forum? Even if unable to diagnose, would someone be kind enough to check whether the problem is repeatable, i.e. run gappa on refine43s.g ?

view this post on Zulip Paolo Giarrusso (Nov 13 2023 at 19:56):

Let me tag the expert, @Guillaume Melquiond

view this post on Zulip Michael Soegtrop (Nov 14 2023 at 08:28):

I guess the issue is more that we first wanted to exclude that this is a strange OS / build issue. I can conform this on MacOS. I am using gappa since years without issues.

I can confirm the issue with the test files you supplied on macOS.

I would suggest to file a bug here:

https://gitlab.inria.fr/gappa/gappa/-/issues

If you want I can do this for you (you need an account only someone from INRIA can create).

view this post on Zulip Michael Hennebry (Nov 14 2023 at 16:47):

Thanks. Please do.

view this post on Zulip Michael Soegtrop (Nov 14 2023 at 17:03):

See https://gitlab.inria.fr/gappa/gappa/-/issues/14.


Last updated: Oct 13 2024 at 01:02 UTC