cbv trips an internal assertion under -Dsym.debug=true
Maintainers usually reply within 1 day
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 35/100
- Issue type
- Bug
- Clarity
- Mostly clear
- Activity status
- Active
- Domain
- compilers
Research direction
Start by reproducing the supplied Lean example with -Dsym.debug=true, then compare it with the run without that option. Trace the failing Lean.Meta.Sym.AlphaShareBuilder assertion at Sym/AlphaShareBuilder:42; done means identifying and fixing the cause so the example succeeds with sym.debug enabled.
Written by the indexing model from the issue text.
Description
The following code:
import Std
open Std
def frequencies (xs : List Nat) : TreeMap Nat Nat (fun a b => compare b a) :=
xs.foldl (init := ∅) (fun freq x => freq.alter x (fun | none => some 1 | some n => some (n+1)))
def search (xs : List Nat) : Int :=
let fr := frequencies xs
let kv := fr.iter |>.map (fun (k, _) => k) |>.first?
kv.getD (-1)
example : search [3, 2] = 3 := by cbv
Resulted in this output:
error: <SymM default value>
PANIC at Lean.Meta.Sym.Internal.Sym.assertShared Lean.Meta.Sym.AlphaShareBuilder:42:2: assertion violation: isSameExpr prev.expr e
Expected: the proof succeeds, as it does without sym.debug (exit code 0)
- Dominant language
- Lean
- Stars
- 9.6k
- Forks
- 1.1k
- Avg merge
- 1d 35m
- Merged PRs (30d)
- 269
Getting set up
- No Dockerfile or Docker Compose file
- Has a pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/lean4
-
`IO.appPath` fails when `/proc` belongs to another PID namespacePossibly taken A pull request linked to this issue is open or already merged. Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15692 · 3 reactions ·
Maintainers usually reply within 1 day
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
leanprover/lean4#15683 ·
Maintainers usually reply within 1 day
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
leanprover/lean4#15681 ·
Maintainers usually reply within 1 day
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
leanprover/lean4#15677 ·
Maintainers usually reply within 1 day
-
`Child.takeStdin` loses `setsid`, so `Child.kill` only signals the child, not its process groupOpenbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15674 ·
Maintainers usually reply within 1 day
All issues in leanprover/lean4
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 82/100
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
swc-project/swc#12576 ·
Maintainers usually reply within 1 day
-
bug priority: P2
Difficulty 1/5 1-3 hours Newbie friendliness 84/100
Maintainers usually reply within 1 day
-
documentation stdlib
Difficulty 2/5 1-3 hours Newbie friendliness 67/100
Maintainers usually reply within 1 day
-
clang:static analyzer
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
llvm/llvm-project#233598 · 1 comment ·
Maintainers usually reply within 1 day