I have a test file (.v) for a plugin, but I run into this strange issue where I get an error when I try to run the test by calling coqc on it, but succeeds when I step through the file in vscoq or coqide. Does anyone know why this could be happening? (I have already rebuilt the plugin and even removed the repository entirely and recloned it)
what's the error?
File "./coq/examples/Intro.v", line 31, characters 0-22:
Error: Conversion test raised an anomaly:
Anomaly "Universe Intro.17 undefined."
I found a bug that resulted in this error (it failed both via coqc and stepping through the file). I fixed the bug, but it still fails via coqc
if you're manually using coqc
, there may be some parameters missing that are implicitly sent via CoqIDE and VsCoq (to coqidetop.opt
)
Could the implicit parameters result in an issue like a undefined universe? Is there a way to inspect the parameters being passed by the editors?
can you show the code?
Possibly you have a _CoqProject file. CoqIDE and VSCoq will take parameters from there automatically, while coqc
won't. You can look into the _CoqProject file what the parameters are.
@Gaëtan Gilbert its here: https://github.com/agrarpan/pumpkin-pi/tree/coq-8.10
And this is the file that has the test error: https://github.com/agrarpan/pumpkin-pi/blob/coq-8.10/plugin/coq/examples/Intro.v
cannot reproduce
This is with coq 8.10? what ocaml version? flambda?
Yes, with coq 8.10 and OCaml 4.09.1.
You need to run the build.sh script first and then coqc coq/examples/Intro.v should reproduce the error
vscoq(1?)/coqide check code asynchronously by default, and that skips some universe checking
you can fix that by using the synchronous vscoq commands (I expect CoqIDE lets you do it too somehow):
image.png
(that's from the command palette, Ctrl/Cmd-Shift-P
for me)
_but_ if this is the problem, the synchronous commands won't fix the error, they'll just start failing as they should with the same failure as coqc
: asynchronous proof checking is simply unsound
(even if in a way which is seldom relevant — this only applies to universes inside Qed
proofs)
there's no "failing as they should with the same failure as coqc" since coqc is producing an anomaly
what do you mean?
since an anomaly isn't a success, I call it a failure, maybe you use "failure" more restrictively?
it's not "as they should", it shouldn't fail or at least not with an anomaly
Ah sorry of course: the coqc anomaly is a bug, but vscoq/coqide should give the same results as coqc, and usually does in sync mode
So I looked at the evar_map being generated in Coq 8.10 (current) and Coq 8.9 (working version), and it seems like the issue is that the universes in the evar_map in 8.10 are called Top.17, Top.16 etc, while in 8.9 they are called Intro.17, Intro.16 etc
And the anomaly that coqc reports says that Universe.17 is undefined. So maybe coq expects to see Intro.17 instead of Top.17? Could this be the issue? (This might be completely incorrect, just a guess)
Ah, that's because Coq's using the module name as base, and in doubt coqtop uses Top
The IDE these days can tell coqtop to use the right name, not sure back then
But... Are you sure that either version is mixing Top and Intro ? That difference sounds more likely to be a coqtop vs coqc difference — I'd always expect coqc to use Intro not Top
(of course Gaetan knows more than me, but he's also busier — maybe you can double-check this first?)
coqc universes should have been Intro.XXX since ~forever
coqide started passing -topfile in 8.10 so it would make sense that coqide universes were Top before and Intro after
However I don't see how this leads to a bug, the universes appearing in terms should be the same ones that are in the evar map regardless of their name
Yeah, I just double checked and it is like you said. coqc universes are Intro.xxx in both 8.9 and 8.10 whereas coqtop universes are Top in 8.9 and Intro in 8.10.
And this is using a bunch of plugins which might have bugs, right? Have you been able to test if sync mode in the IDE gives the same failure?
Sync mode in vscoq succeeds, only coqc gives me the error
still can't reproduce
Screenshot_20231011_110014.png
Screenshot-from-2023-10-11-14-53-59.png
Just to be sure, you're on the coq-8.10 branch and not master, right?
as per screenshot, Gaëtan is using the most recent release of 8.10, version 8.10.2 (from the general opam repo)
branches in the Coq GitHub repo other than master
and (typically) the two most recent ones, e.g., v8.19
and v8.18
, are not considered usable or supported
I used the v8.10 branch (not the tag, but the only change is some native compile debug stuff)
Sorry, I meant the coq-8.10 branch of the pumpkin-pi github repository I linked to
yes
pumpkin-pi 354c0913fe2d94c98e7fbca466b5cb6f35529b4a
I just created a new opam switch with coq 8.10.2 and I don't get the error anymore. I don't know why this could be the case though
Although a test case that was working on the previous 8.10 switch now fails.
coqc coq/Test.v
now gives the error "Anomaly "index to an anonymous variable."
Not sure if this is a genuine bug in my code or a similar issue to the coq/examples/Intro.v file
I can reproduce that
I think it means something is getting printed in an incorrect environment
(an environment where some variable is bound to the name _
)
Last updated: Oct 13 2024 at 01:02 UTC