Panic in unreachable tactic linter

Stream: lean4

[Siddharth Bhat]

I just ran into this over at https://github.com/bollu/ssa/commit/a2df44f626d4d4bc0a5671a14660d542611e7cd7

The error is:

PANIC at Lean.PersistentHashMap.find! Lean.Data.PersistentHashMap:160:14: key is not in the map
backtrace:
/home/bollu/.elan/toolchains/leanprover--lean4---nightly-2023-05-18/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x9e)[0x7fb310788c4e]
./lake-packages/std/build/lib/libStd-Linter-UnreachableTactic.so(l_Std_Linter_UnreachableTactic_unreachableTacticLinter___elambda__1___lambda__1+0x62b)[0x7fb3082ff6eb]
./lake-packages/std/build/lib/libStd-Linter-UnreachableTactic.so(l_Std_Linter_UnreachableTactic_unreachableTacticLinter___elambda__1+0x430)[0x7fb308300410]
/home/bollu/.elan/toolchains/leanprover--lean4---nightly-2023-05-18/bin/../lib/lean/libleanshared.so(lean_apply_4+0x181)[0x7fb310795771]
...

I am going to MWE this; I was wondering if this has been seen before.

[Siddharth Bhat]

For whatever reason, it's the register_simp_attr that is the source of the crash. Commenting out all register_simp_attr in one particular file fixes the crash: https://github.com/bollu/ssa/commit/db63572a6901d29042a284108054a6324aff4ded

[Mario Carneiro]

my guess, based on that error is that what is failing is one of these two lines:

  let tactics := cats.find! `tactic |>.kinds
  let convs := cats.find! `conv |>.kinds

i.e. you are not in a scope that has defined the tactic or conv syntax categories yet. I don't really see how this could be possible, since the linter itself imports enough to make that work

[Mario Carneiro]

you might be running the linter in an environment other than the current one, e.g. if you used an empty environment this would fail

[Siddharth Bhat]

@Mario Carneiro I am unsure how I could be changing the environment. I am performing a standard lake build, on a file.that does not play tricks.

[Mario Carneiro]

what is the linter running on?

[Siddharth Bhat]

I don't know what your question means. Let me try to be helpful, as best as I understand the question: the linter runs as it usually does during compilation. I am compiling the module SSA.Projects.InstCombine.InstCombinePeepholeRewrites

[Mario Carneiro]

there was a prior error in the log:

error: stdout:
./././SSA.lean:4:0: error: invalid environment extension, 'SSA.teval' has already been used
error: stderr:
PANIC at Lean.PersistentHashMap.find! Lean.Data.PersistentHashMap:160:14: key is not in the map

My guess is that when the env extension insert failed it returned default : Environment causing the linter to fail

[Siddharth Bhat]

Ah, I see

[Siddharth Bhat]

Thanks!