PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none

[oOo0oOo]

This panic keeps coming up when processing various files. You can see it in the results here (Comparator column, yellow results):
https://github.com/oOo0oOo/LeanParanoia/blob/main/VERIFIER_COMPARISON.md

Full Error Message

PANIC Building LeanTestProject.AuxiliaryShadowing.MatcherShadowing
Build completed successfully (2 jobs).
Exporting #[test1] from LeanTestProject.AuxiliaryShadowing.MatcherShadowing
uncaught exception: process 'landrun' exited with code 134
stderr:
PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none
backtrace:
lean4export(+0x9f5698e) [0x6552441ca98e]
lean4export(lean_panic_fn+0x1c) [0x6552441cae2c]
lean4export(l_dumpConstant+0x9c) [0x65523c5d725c]
lean4export(l_List_forIn_x27_loop___at___main_spec__3___redArg+0xec) [0x65523c5c923c]
lean4export(l_main___lam__1+0x50e) [0x65523c5ca0ee]
lean4export(lean_apply_3+0x970) [0x6552441da3e0]
lean4export(l_M_run___redArg+0x1d) [0x65523c5cb84d]
lean4export(+0x2357609) [0x65523c5cb609]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x77ec09c29d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x77ec09c29e40]
lean4export(_start+0x2a) [0x65523c5c86aa]

System

Ubuntu 22.04.5, Lean v4.25.0, lean4export built from source (HEAD)

lean4export installed using:
https://github.com/oOo0oOo/LeanParanoia/blob/main/tests/benchmark/install_comparator.sh

Comparator is run here:
https://github.com/oOo0oOo/LeanParanoia/blob/968e428181a7ef8fec3af34216e426db21d56d70/tests/benchmark/test_tool_comparison.py#L250

[ammkrn]

I've opened a PR that will at least give more information about the failure; you're trying to export an Expr that references a declaration by name, but the referenced declaration doesn't exist in the environment being checked. The exporter doesn't currently say what the name of the bad declaration/name pair is, which is not very helpful. The PR may or may not be merged, but you can try using that branch to get some more info.

I took a quick look at your repo but I'm not sure whether this is a "should fail" case or not. It would be helpful if you could explain what you expect to happen and why.

[oOo0oOo]

Thanks for the quick reply. I did some tests using your branch and thanks to the improved error message i was able to find the bug in my code.

I will take some time tomorrow to give a proper reply.