Arpan Agrawal (Nov 02 2023 at 16:48): Arpan Agrawal (Nov 02 2023 at 16:48):Did the way to register and lookup projections change between Coq 8.10 and Coq 8.11? I have a test case that succeeds on Coq 8.10 but results in a Not Found exception on Coq 8.11 on a call to Recordops.lookup_projections. I see some minor refactoring in the Record and Recordops modules in the Coq codebase between 8.10 and 8.11, but cannot figure out what I'm doing wrong.
Here's the github repo: https://github.com/agrarpan/pumpkin-pi/tree/coq-8.11
And a draft PR to compare changes: https://github.com/agrarpan/pumpkin-pi/pull/2
The test that's failing is plugin/coq/handshake.v
Thanks!
Arpan Agrawal (Nov 06 2023 at 21:03):Still stuck on this, does anyone know what changed?
Gaëtan Gilbert (Nov 06 2023 at 21:05):IDK
try wrapping the call with a printer to see what it's called on
what's the backtrace like?
Arpan Agrawal (Nov 06 2023 at 21:11):Its called on handshake.connectionRecordPP,
and here's the trace of the error with the -debug flag:
File "./coq/handshake.v", line 209, characters 0-90:
Error: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
frame @ file "toplevel/coqc.ml", line 67, characters 4-25
frame @ file "toplevel/coqc.ml", line 45, characters 2-81
frame @ file "list.ml", line 110, characters 12-15
frame @ file "toplevel/ccompile.ml", line 214, characters 2-39
frame @ file "toplevel/ccompile.ml", line 148, characters 18-89
frame @ file "toplevel/vernac.ml", line 170, characters 30-88
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "toplevel/vernac.ml", line 114, characters 6-19
frame @ file "lib/flags.ml", line 92, characters 19-40
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/flags.ml", line 17, characters 14-17
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "toplevel/vernac.ml", line 68, characters 31-52
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "stm/stm.ml", line 2689, characters 4-60
frame @ file "stm/stm.ml", line 2563, characters 4-105
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "stm/stm.ml", line 1006, characters 6-10
frame @ file "stm/stm.ml", line 2422, characters 16-43
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "vernac/vernacinterp.ml", line 260, characters 6-284
frame @ file "vernac/vernacinterp.ml", line 262, characters 18-43
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/flags.ml", line 17, characters 14-17
frame @ file "vernac/vernacinterp.ml", line 218, characters 20-60
frame @ file "vernac/vernacinterp.ml", line 28, characters 19-23
raise @ unknown
frame @ file "src/frontend.ml", line 333, characters 22-60
frame @ file "src/automation/lift/lift.ml", line 251, characters 17-59
frame @ file "src/automation/lift/liftconfig.ml", line 2001, characters 17-50
frame @ file "pretyping/recordops.ml", line 87, characters 29-63
raise @ file "map.ml", line 136, characters 10-25
Arpan Agrawal (Nov 06 2023 at 21:13):The same call works with Coq 8.10, on the same structure, so my suspicion is that the projections arent registering correctly in Coq 8.11, for some reason
But the only change I can see is the refactoring of Recordops.declare_structure to Record.declare_structure_entry, which I have already changed in my code
Gaëtan Gilbert (Nov 07 2023 at 11:05):https://github.com/agrarpan/pumpkin-pi/blob/df7c298c0b210dce523072d4d798b94784568eef/plugin/src/automation/lift/lift.ml#L336 is producing a Not_found in command
Lift HandshakeRecord.Handshake
HandshakeRecordPP.Handshake
in ConnectionRecordPP1.Connection
as connectionRecordPP.
so the declare_structure_entry later in the source doesn't run
Gaëtan Gilbert (Nov 07 2023 at 11:11):IDK why this would change though
also kind of hard to see the changes with this submodule setup (I hate submodules)
Arpan Agrawal (Nov 07 2023 at 17:20):Gaëtan Gilbert said:
https://github.com/agrarpan/pumpkin-pi/blob/df7c298c0b210dce523072d4d798b94784568eef/plugin/src/automation/lift/lift.ml#L336 is producing a Not_found in command
Lift HandshakeRecord.Handshake HandshakeRecordPP.Handshake in ConnectionRecordPP1.Connection as connectionRecordPP.so the declare_structure_entry later in the source doesn't run
Are you sure about this? That's not the case for me, I only get a Not_found at the last Lift command in the file. Also the declare_structure_entry in lift.ml doesnt run, but there is another call to declare_structure_entry in the submodules that does run.
Sorry about the structuring of the submodules, do you have any suggestions on how to manage these dependencies instead of loading them as submodules?
Thanks for looking into this!
Gaëtan Gilbert (Nov 07 2023 at 17:23):the Not_found is caught line 367 in lift.ml so nothing gets printed, but when I added some debug prints it was definitely there
Gaëtan Gilbert (Nov 07 2023 at 17:26):it's possible that one of the changes where a function takes an env instead of using the global one like
- let elim0 = Indrec.lookup_eliminator ind0 sort in
- let elim = Indrec.lookup_eliminator ind sort in
+ let elim0 = Indrec.lookup_eliminator env ind0 sort in
+ let elim = Indrec.lookup_eliminator env ind sort in
the env may be outdated so one of those functions may raise and the exception gets caught somewhere so you don't see an error?
I didn't test this hypothesis though
Gaëtan Gilbert (Nov 07 2023 at 17:26):you can try doing
- let elim0 = Indrec.lookup_eliminator ind0 sort in
- let elim = Indrec.lookup_eliminator ind sort in
+ let elim0 = Indrec.lookup_eliminator (Global.env()) ind0 sort in
+ let elim = Indrec.lookup_eliminator (Global.env()) ind sort in
instead (and same for the other similar changes)
Arpan Agrawal (Nov 07 2023 at 17:32):Will try this.
I also made a couple of draft PRs for the dependencies, to make seeing the changes easier:
https://github.com/agrarpan/coq-plugin-lib/pull/2
https://github.com/agrarpan/fix-to-elim/pull/1
Arpan Agrawal (Dec 01 2023 at 04:29):@Gaëtan Gilbert I managed to fix this, it was actually an issue much earlier, there was a change in the Coq API that I had incorrectly used in my code.
Thanks for your help!
I'm still curious about other ways to manage dependencies within the plugin other than through git submodules, please let me know if thats possible.
Thanks again.
Last updated: Oct 13 2024 at 01:02 UTC