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
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 ?
Let me tag the expert, @Guillaume Melquiond
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).
Thanks. Please do.
See https://gitlab.inria.fr/gappa/gappa/-/issues/14.
Last updated: Oct 13 2024 at 01:02 UTC