Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

PANIC with Nat.reducePow and exponentiation in variable #4947

Closed
3 tasks done
Parcly-Taxel opened this issue Aug 7, 2024 · 0 comments · Fixed by #4988
Closed
3 tasks done

PANIC with Nat.reducePow and exponentiation in variable #4947

Parcly-Taxel opened this issue Aug 7, 2024 · 0 comments · Fixed by #4988
Labels
bug Something isn't working P-high We will work on this issue

Comments

@Parcly-Taxel
Copy link
Contributor

Prerequisites

Please put an X between the brackets as you perform the following steps:

Description

When Nat.reducePow is used in simp and the variables in context contain Nat ^ Nat terms, the Lean kernel may PANIC.

Context

This was originally discovered while updating mathlib for the Carleson project. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/PANIC.20at.20Lean.2EExpr.2EappArg!.20application.20expected/near/457037665

Steps to Reproduce

  1. lake +leanprover/lean4:nightly-2024-08-05 new test; cd test; lake update
  2. In Test.lean put
universe u
class G (A : outParam Nat) where Z : Type u
export G (Z)
abbrev f (a : Nat) : Nat := 2 ^ a
variable [G (f 0)]
example {s : Z} : s = s := by simp only [Nat.reducePow]
  1. lake build Test

Expected behavior:
It should just say "Build completed successfully" without any PANIC.

Actual behavior:
The build does complete successfully, but there is a PANIC before it.

Backtrace:

ℹ [2/3] Built Test
info: stderr:
PANIC at Lean.Expr.appArg! Lean.Expr:896:15: application expected
backtrace:
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x9e)[0x768c2f84b32e]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Nat_reducePow+0x2c)[0x768c2ccc071c]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Nat_reducePow___boxed+0x31)[0x768c2ccc1831]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_9+0x5b6)[0x768c2f85cf46]applying
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_SimprocEntry_tryD+0x269)[0x768c2cf616e9]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_dsimprocCore___spec__1+0x3c36)[0x768c2cf7bfc6]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_dsimprocCore+0x64c)[0x768c2cf8468c]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_dsimprocArrayCore___spec__1+0x56f)[0x768c2cf8cd7f]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_dsimprocArrayCore+0x166)[0x768c2cf8e206]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_userPostDSimprocs+0xbc)[0x768c2cf8fa3c]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_userPostDSimprocs___boxed+0x22)[0x768c2cf8fcd2]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_9+0x420)[0x768c2f85cdb0]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_dandThen+0x7ab)[0x768c2ce74d4b]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_mkMethods___elambda__1+0x85)[0x768c2cf4b005]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_9+0x5b6)[0x768c2f85cf46]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_dandThen+0x107)[0x768c2ce746a7]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_9+0x659)[0x768c2f85cfe9]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_transform_visit_visitPost___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__3+0x133)[0x768c2cdcc363]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Expr_withAppAux___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__13+0x166a)[0x768c2cdda37a]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_transform_visit___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__2___lambda__1+0xfca)[0x768c2cdded0a]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_transform_visit___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__2___lambda__1___boxed+0xd8)[0x768c2cde00f8]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_10+0x44a)[0x768c2f85d8ba]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_ReaderT_bind___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__14___rarg+0x316)[0x768c2cddc146]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_9+0x483)[0x768c2f85ce13]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_withIncRecDepth___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__15+0x4a6)[0x768c2cddcb46]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_transform_visit___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__2+0xa8b)[0x768c2cdce03b]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Array_mapMUnsafe_map___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__10+0x25c)[0x768c2cdd63ec]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Expr_withAppAux___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__13+0xe01)[0x768c2cdd9b11]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_transform_visit___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__2___lambda__1+0xfca)[0x768c2cdded0a]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_transform_visit___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__2___lambda__1___boxed+0xd8)[0x768c2cde00f8]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_10+0x44a)[0x768c2f85d8ba]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_ReaderT_bind___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__14___rarg+0x316)[0x768c2cddc146]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_9+0x483)[0x768c2f85ce13]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_withIncRecDepth___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__15+0x4a6)[0x768c2cddcb46]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_transform_visit___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__2+0xa8b)[0x768c2cdce03b]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_transform___at___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___spec__1+0x112)[0x768c2cde0352]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___lambda__3+0x247)[0x768c2cde0917]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_dsimp+0x11c)[0x768c2cda35fc]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_congrArgs___spec__3___lambda__2+0xd5f)[0x768c2ce8d3bf]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_congrArgs___spec__3+0xf74)[0x768c2ce900b4]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_congrArgs+0x464)[0x768c2ce93b44]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Expr_withAppAux___at_Lean_Meta_Simp_congrDefault___spec__1+0x50b)[0x768c2cde43cb]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_congrDefault+0x80f)[0x768c2cde4e0f]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_congr+0x5b0)[0x768c2cdf75d0]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_simpStep+0x4db)[0x768c2cdf866b]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_simpLoop_visitPreContinue+0x47c)[0x768c2cdfc0cc]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_simpLoop+0x1f8b)[0x768c2cdffffb]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_simpImpl_go___lambda__2+0x32b)[0x768c2ce0595b]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_simpImpl_go+0x4b2)[0x768c2ce05eb2]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_simp+0xc0b)[0x768c2cdb20cb]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_main_go+0xb5)[0x768c2ce074e5]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_main+0x1bb1)[0x768c2ce097b1]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_Simp_main___boxed+0x22)[0x768c2ce0ba82]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_1+0x260)[0x768c2f8562c0]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1+0xe)[0x768c2e25ad8e]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed+0xf)[0x768c2e25af8f]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_1+0x149)[0x768c2f8561a9]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_profileit+0x74)[0x768c2f7ae804]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg+0x60)[0x768c2e25aeb0]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_simp+0x1c3)[0x768c2ce0dbd3]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_simpTargetCore+0x312)[0x768c2ce0e0f2]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_simpTarget___lambda__1+0x25c)[0x768c2ce0f64c]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_5+0x446)[0x768c2f859c96]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg+0x208)[0x768c2d8ba5d8]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_MVarId_withContextapplying___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp___spec__2___rarg+0x18)[0x768c2d4202e8]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_simpGoal___lambda__3+0x1a2)[0x768c2ce27f82]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_simpGoal___lambda__4+0x8e6)[0x768c2ce29696]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_simpGoal___lambda__4___boxed+0x74)[0x768c2ce2a414]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_5+0x4d7)[0x768c2f859d27]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg+0x208)[0x768c2d8ba5d8]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_MVarId_withContext___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp___spec__2___rarg+0x18)[0x768c2d4202e8]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Meta_simpGoal+0xce)[0x768c2ce2a37e]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Tactic_simpLocation_go+0x2f2)[0x768c2ea3eea2]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Tactic_simpLocation___lambda__2+0x369)[0x768c2ea40989]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_5+0x4d7)[0x768c2f859d27]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg+0x208)[0x768c2d8ba5d8]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_MVarId_withContext___at_Lean_Elab_Tactic_withMainContext___spec__1___rarg+0x59)[0x768c2e9c6ae9]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Tactic_withMainContext___rarg+0x28b)[0x768c2e9c6f0b]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Tactic_simpLocation+0x14f)[0x768c2ea40edf]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalSimp___lambda__1___boxed+0x9f)[0x768c2ea4295f]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_10+0x52e)[0x768c2f85d99e]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalSimp___lambda__3+0x4a6)[0x768c2ea41a56]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_9+0x420)[0x768c2f85cdb0]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Tactic_withSimpDiagnostics+0x94)[0x768c2ea41104]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_5+0x3e9)[0x768c2f859c39]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg+0x208)[0x768c2d8ba5d8]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_MVarId_withContext___at_Lean_Elab_Tactic_withMainContext___spec__1___rarg+0x59)[0x768c2e9c6ae9]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Tactic_withMainContext___rarg+0x28b)[0x768c2e9c6f0b]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_9+0x420)[0x768c2f85cdb0]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withInfoTreeContext___at_Lean_Elab_Tactic_evalTactic_eval___spec__2+0x251)[0x768c2e993961]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic_eval___lambda__2+0x254)[0x768c2e99bf34]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_9+0x483)[0x768c2f85ce13]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withoutTacticIncrementality___at_Lean_Elab_Tactic_evalTactic_eval___spec__3+0x2830)[0x768c2e997d40]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic_eval+0x50d)[0x768c2e99a30d]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic_expandEval+0xde1)[0x768c2e9a5a21]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic___lambda__3+0xed)[0x768c2e9aea0d]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic___lambda__4+0xb24)[0x768c2e9af584]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_9+0x420)[0x768c2f85cdb0]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic___spec__3+0x355)[0x768c2e9ad9c5]
/home/parclytaxel/.elan/toolchains/leanprover--lean4---nightly-2024-08-05/bin/../lib/lean/libleanshared.so(lean_apply_3+0x52c)[0x768c2f8582ac]
Build completed successfully.

Versions

4.11.0-nightly-2024-08-05, Ubuntu 24.04. The issue does not occur on 4.10.0.
@Parcly-Taxel Parcly-Taxel added the bug Something isn't working label Aug 7, 2024
Parcly-Taxel added a commit to Parcly-Taxel/lean4 that referenced this issue Aug 9, 2024
@Parcly-Taxel
fix: guard against Nat.reducePow panicking
25e18b8 
In the Carleson project a non-fatal PANIC occurring in the application
of certain applications of `Nat.reducePow` was discovered
(https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/PANIC.20at.20Lean.2EExpr.2EappArg!.20application.20expected/near/457037665).
We fix this regression from leanprover#4637.

Fixes leanprover#4947.
@Parcly-Taxel Parcly-Taxel mentioned this issue Aug 9, 2024
Closed
Parcly-Taxel added a commit to Parcly-Taxel/lean4 that referenced this issue Aug 9, 2024
@Parcly-Taxel
fix: guard against Nat.reducePow panicking
e4f50f7 
In the Carleson project a non-fatal PANIC occurring in the application
of certain applications of `Nat.reducePow` was discovered
(https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/PANIC.20at.20Lean.2EExpr.2EappArg!.20application.20expected/near/457037665).
We fix this regression from leanprover#4637.

Fixes leanprover#4947.
@leanprover-bot leanprover-bot added the P-high We will work on this issue label Aug 9, 2024
leodemoura added a commit that referenced this issue Aug 12, 2024
@leodemoura
fix: panic at reducePow
aa4dfbb 
closes #4947
@leodemoura leodemoura mentioned this issue Aug 12, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Aug 12, 2024
@leodemoura
fix: panic at reducePow (#4988)
7d74475 
closes #4947
Parcly-Taxel added a commit to Parcly-Taxel/lean4 that referenced this issue Aug 12, 2024
@Parcly-Taxel
fix: guard against Nat.reducePow panicking
3ac2a1c 
In the Carleson project a non-fatal PANIC occurring in the application
of certain applications of `Nat.reducePow` was discovered
(https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/PANIC.20at.20Lean.2EExpr.2EappArg!.20application.20expected/near/457037665).
We fix this regression from leanprover#4637.

Fixes leanprover#4947.
Parcly-Taxel pushed a commit to Parcly-Taxel/lean4 that referenced this issue Aug 12, 2024
@leodemoura @Parcly-Taxel
fix: panic at reducePow (leanprover#4988)
bc77c7d 
closes leanprover#4947
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working P-high We will work on this issue
Projects
None yet
Milestone
No milestone
2 participants
@Parcly-Taxel @leanprover-bot