Stream: Coq devs & plugin devs

Topic: Test case failing with coqc but succeeds in vscoq/coqide


view this post on Zulip Arpan Agrawal (Oct 10 2023 at 08:41):

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)

view this post on Zulip Gaëtan Gilbert (Oct 10 2023 at 08:45):

what's the error?

view this post on Zulip Arpan Agrawal (Oct 10 2023 at 08:46):

File "./coq/examples/Intro.v", line 31, characters 0-22:
Error: Conversion test raised an anomaly:
Anomaly "Universe Intro.17 undefined."

view this post on Zulip Arpan Agrawal (Oct 10 2023 at 08:47):

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

view this post on Zulip Karl Palmskog (Oct 10 2023 at 08:47):

if you're manually using coqc, there may be some parameters missing that are implicitly sent via CoqIDE and VsCoq (to coqidetop.opt)

view this post on Zulip Arpan Agrawal (Oct 10 2023 at 09:18):

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?

view this post on Zulip Gaëtan Gilbert (Oct 10 2023 at 09:39):

can you show the code?

view this post on Zulip Michael Soegtrop (Oct 10 2023 at 10:16):

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.

view this post on Zulip Arpan Agrawal (Oct 10 2023 at 10:30):

@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

view this post on Zulip Gaëtan Gilbert (Oct 10 2023 at 10:53):

cannot reproduce
This is with coq 8.10? what ocaml version? flambda?

view this post on Zulip Arpan Agrawal (Oct 10 2023 at 10:56):

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

view this post on Zulip Paolo Giarrusso (Oct 10 2023 at 17:21):

vscoq(1?)/coqide check code asynchronously by default, and that skips some universe checking

view this post on Zulip Paolo Giarrusso (Oct 10 2023 at 17:23):

you can fix that by using the synchronous vscoq commands (I expect CoqIDE lets you do it too somehow):
image.png

view this post on Zulip Paolo Giarrusso (Oct 10 2023 at 17:23):

(that's from the command palette, Ctrl/Cmd-Shift-P for me)

view this post on Zulip Paolo Giarrusso (Oct 10 2023 at 17:26):

_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

view this post on Zulip Paolo Giarrusso (Oct 10 2023 at 17:29):

(even if in a way which is seldom relevant — this only applies to universes inside Qed proofs)

view this post on Zulip Gaëtan Gilbert (Oct 10 2023 at 17:51):

there's no "failing as they should with the same failure as coqc" since coqc is producing an anomaly

view this post on Zulip Paolo Giarrusso (Oct 10 2023 at 17:58):

what do you mean?

view this post on Zulip Paolo Giarrusso (Oct 10 2023 at 17:59):

since an anomaly isn't a success, I call it a failure, maybe you use "failure" more restrictively?

view this post on Zulip Gaëtan Gilbert (Oct 10 2023 at 18:22):

it's not "as they should", it shouldn't fail or at least not with an anomaly

view this post on Zulip Paolo Giarrusso (Oct 10 2023 at 20:52):

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

view this post on Zulip Arpan Agrawal (Oct 11 2023 at 07:04):

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)

view this post on Zulip Paolo Giarrusso (Oct 11 2023 at 07:08):

Ah, that's because Coq's using the module name as base, and in doubt coqtop uses Top

view this post on Zulip Paolo Giarrusso (Oct 11 2023 at 07:09):

The IDE these days can tell coqtop to use the right name, not sure back then

view this post on Zulip Paolo Giarrusso (Oct 11 2023 at 07:11):

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

view this post on Zulip Paolo Giarrusso (Oct 11 2023 at 07:13):

(of course Gaetan knows more than me, but he's also busier — maybe you can double-check this first?)

view this post on Zulip Gaëtan Gilbert (Oct 11 2023 at 07:17):

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

view this post on Zulip Arpan Agrawal (Oct 11 2023 at 07:23):

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.

view this post on Zulip Paolo Giarrusso (Oct 11 2023 at 07:59):

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?

view this post on Zulip Arpan Agrawal (Oct 11 2023 at 08:08):

Sync mode in vscoq succeeds, only coqc gives me the error

view this post on Zulip Gaëtan Gilbert (Oct 11 2023 at 09:00):

still can't reproduce
Screenshot_20231011_110014.png

view this post on Zulip Arpan Agrawal (Oct 11 2023 at 09:25):

Screenshot-from-2023-10-11-14-53-59.png

view this post on Zulip Arpan Agrawal (Oct 11 2023 at 09:35):

Just to be sure, you're on the coq-8.10 branch and not master, right?

view this post on Zulip Karl Palmskog (Oct 11 2023 at 09:37):

as per screenshot, Gaëtan is using the most recent release of 8.10, version 8.10.2 (from the general opam repo)

view this post on Zulip Karl Palmskog (Oct 11 2023 at 09:38):

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

view this post on Zulip Gaëtan Gilbert (Oct 11 2023 at 09:48):

I used the v8.10 branch (not the tag, but the only change is some native compile debug stuff)

view this post on Zulip Arpan Agrawal (Oct 11 2023 at 09:57):

Sorry, I meant the coq-8.10 branch of the pumpkin-pi github repository I linked to

view this post on Zulip Gaëtan Gilbert (Oct 11 2023 at 10:00):

yes
pumpkin-pi 354c0913fe2d94c98e7fbca466b5cb6f35529b4a

view this post on Zulip Arpan Agrawal (Oct 11 2023 at 10:13):

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

view this post on Zulip Arpan Agrawal (Oct 11 2023 at 10:27):

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

view this post on Zulip Gaëtan Gilbert (Oct 11 2023 at 10:31):

I can reproduce that

view this post on Zulip Gaëtan Gilbert (Oct 11 2023 at 10:33):

I think it means something is getting printed in an incorrect environment

view this post on Zulip Gaëtan Gilbert (Oct 11 2023 at 10:37):

(an environment where some variable is bound to the name _)


Last updated: Oct 13 2024 at 01:02 UTC