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

Open
#8 2 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
25/100
Issue type
Bug
Clarity
Needs clarification
Activity status
Stale
Domain
compilers

Research direction

Start with tests/benchmark/test_tool_comparison.py around line 250 and the referenced install_comparator.sh to reproduce the comparator failure on the reported system. Use the backtrace's l_dumpConstant entry point to investigate the Option.get! panic; done means the reported files no longer cause the exporter process to exit with code 134.

Written by the indexing model from the issue text.

Description

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

Dominant language
Lean
Stars
40
Forks
26
Avg merge
51m
Merged PRs (30d)
5

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from leanprover/lean4export

All issues in leanprover/lean4export

Similar issues

More Compilers issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.