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

Loose bvar while generating equations #6374

Open
3 tasks done
hargoniX opened this issue Dec 12, 2024 · 0 comments
Open
3 tasks done

Loose bvar while generating equations #6374

hargoniX opened this issue Dec 12, 2024 · 0 comments
Labels
bug Something isn't working

Comments

@hargoniX
Copy link
Contributor

hargoniX commented Dec 12, 2024 •
edited
Loading

Prerequisites

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

Description

The following code:

import Lean.Elab.ElabRules
import Lean.Meta.Eqns

#eval show Lean.MetaM _ from do
  Lean.Meta.getEqnsFor? ``Lean.Elab.Command.elabElabRulesAux

crashes due to a loose bvar, the backtrace ends in whnf:

#1  0x00007f7bd6f98d03 in __pthread_kill_internal (threadid=<optimized out>, signo=6) at pthread_kill.c:78
#2  0x00007f7bd6f3fd1e in __GI_raise (sig=sig@entry=6) at ../sysdeps/posix/raise.c:26
#3  0x00007f7bd6f27942 in __GI_abort () at abort.c:79
#4  0x00007f7bdcd6510e in lean_panic_fn () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#5  0x00007f7bd8ac7aac in l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfImp___spec__3 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#6  0x00007f7bd8a57d75 in l___private_Lean_Meta_WHNF_0__Lean_Meta_reduceRec___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#7  0x00007f7bd8a89310 in l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfCore_go___spec__3___lambda__4 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so

comes there from simp:

349 0x00007f7bd955f95a in l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___rarg___lambda__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#350 0x00007f7bdcd78433 in lean_apply_5 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#351 0x00007f7bd9560481 in l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#352 0x00007f7bd9562f55 in l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#353 0x00007f7bd95629ba in l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAux___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#354 0x00007f7bd956563a in l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingImp___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#355 0x00007f7bd8f339f4 in l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_Simp_processCongrHypothesis___spec__2___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#356 0x00007f7bd8f348df in l_Lean_Meta_Simp_processCongrHypothesis () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#357 0x00007f7bd8f35743 in l_Array_forIn_x27Unsafe_loop___at_Lean_Meta_Simp_trySimpCongrTheorem_x3f___spec__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#358 0x00007f7bd8f3d575 in l_Lean_Meta_Simp_trySimpCongrTheorem_x3f___lambda__6 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#359 0x00007f7bd8f3f285 in l_Lean_Meta_Simp_trySimpCongrTheorem_x3f___lambda__7 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#360 0x00007f7bd8f40011 in l_Lean_Meta_Simp_trySimpCongrTheorem_x3f___lambda__8 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#361 0x00007f7bd8f412a8 in l_Lean_Meta_Simp_trySimpCongrTheorem_x3f___lambda__9 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#362 0x00007f7bd8f41751 in l_Lean_Meta_Simp_trySimpCongrTheorem_x3f___lambda__9___boxed () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so

called from the equations code:

#507 0x00007f7bd8f5f76a in l_Lean_Meta_Simp_simpImpl_go () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#508 0x00007f7bd8efa554 in lean_simp () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#509 0x00007f7bd8f61105 in l_Lean_Meta_Simp_main_go () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#510 0x00007f7bd8f62037 in l_Lean_Meta_Simp_main () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#511 0x00007f7bd9833ae5 in l___private_Lean_Meta_Tactic_Split_0__Lean_Meta_Split_simpMatchCore () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#512 0x00007f7bd983409d in l___private_Lean_Meta_Tactic_Split_0__Lean_Meta_Split_simpMatchTargetCore___lambda__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#513 0x00007f7bdcd782dd in lean_apply_5 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#514 0x00007f7bd9573f18 in l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#515 0x00007f7bd8b90be8 in l_Lean_MVarId_withContext___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp___spec__2___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#516 0x00007f7bd9865da4 in l_List_foldlM___at_Lean_Meta_Split_splitMatch___spec__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#517 0x00007f7bd98683c6 in l_Lean_Meta_Split_splitMatch___lambda__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#518 0x00007f7bdcd782dd in lean_apply_5 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#519 0x00007f7bd9573f18 in l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#520 0x00007f7bd8b90be8 in l_Lean_MVarId_withContext___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp___spec__2___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#521 0x00007f7bdab3c509 in l_Lean_Elab_Eqns_splitMatch_x3f_go () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#522 0x00007f7bdab3fc5c in l_Lean_Elab_Eqns_splitMatch_x3f___lambda__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#523 0x00007f7bdcd782dd in lean_apply_5 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#524 0x00007f7bd986e4d7 in l_Lean_commitWhenSome_x3f___at_Lean_Meta_splitTarget_x3f___spec__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#525 0x00007f7bdab79ae0 in l_Lean_Elab_Eqns_mkEqnTypes_go___lambda__2 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#526 0x00007f7bdab7a670 in l_Lean_Elab_Eqns_mkEqnTypes_go___lambda__3 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#527 0x00007f7bdab7b3ff in l_Lean_Elab_Eqns_mkEqnTypes_go___lambda__4 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so

Context

I discovered this in the CI of doc-gen, it has existed there since the 4.15-rc1 update but not before that.

Steps to Reproduce

Expected behavior: No loose bvars

Actual behavior: Loose bvars /o\

Versions

Lean 4.16.0-nightly-2024-12-12
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
@hargoniX hargoniX added the bug Something isn't working label Dec 12, 2024
@hargoniX hargoniX mentioned this issue Dec 12, 2024
Merged
leodemoura added a commit that referenced this issue Dec 13, 2024
@leodemoura
fix: unused let_fun elimination in simp
461ea67 
This PR fixes a bug in the simplifier. It was producing terms with
loose bound variables when eliminating unused `let_fun` expressions.

This issue was affecting the example at #6374. The example is now
timing out.
@leodemoura leodemoura mentioned this issue Dec 13, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Dec 13, 2024
@leodemoura
fix: unused let_fun elimination in simp (#6375)
945abe0 
This PR fixes a bug in the simplifier. It was producing terms with loose
bound variables when eliminating unused `let_fun` expressions.

This issue was affecting the example at #6374. The example is now timing
out.
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
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@hargoniX