leanprover-community / leanprover-community/lean
Segmentation fault when using `get_env` with `run_tactic`
Nobody has claimed this yet.
- Dominant language
- C++
- Stars
- 434
- Forks
- 79
- PR merge metrics
- No merged PRs in 30d
Description
Prerequisites
- Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
- Specifically, check out the wishlist, open RFCs,
or feature requests.
- Specifically, check out the wishlist, open RFCs,
- Reduced the issue to a self-contained, reproducible test case.
- Checked that your issue isn't already filed.
Description
When iterating through declarations in an environment env obtained from io.run_tactic (tactic.get_env), lean crashes.
Steps to Reproduce
- Create a lean package like this:
# leanpkg.toml
[package]
name = "bugfinder"
version = "0.1"
lean_version = "leanprover-community/lean:3.50.3"
path = "src"
[dependencies]
mathlib = {path = "../mathlib-lean350"}
where mathlib is placed in the directory shown above.
-- src/main.lean
import system.io
import tactic.basic
meta def main : io unit := do {
e <- io.run_tactic (tactic.get_env),
let l := environment.decl_filter_map e (fun d, some "a") in
l.mmap' (fun s, io.print s)
}
- Execute
leanpkg configure; leanpkg build - Execute
lean --run src/main.lean. It should segfault after printing out a bunch of a's.
Expected behavior: It should print out a string of a's and then exit.
Actual behavior:
Job 1, 'lean --run src/main.lean' terminated by signal SIGSEGV (Address boundary error)
Reproduces how often: Every time it executes
Versions
- Lean (version 3.50.3, commit 855e5b74e3a5, Release)
- Mathlib: 21e3562c5e12d846c7def5eff8cdbc520d7d4936
- OS: ArchLinux (252.5-1-arch)
Additional Information
It seems like writing it like this crashes too:
meta def main : io unit := do {
l <- io.run_tactic $ do {
e <- tactic.get_env,
return (environment.decl_filter_map e (fun d, some "a"))
},
l.mmap' io.print_ln
}
Contributor 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.
Research direction
Start with the reproducible package in leanpkg.toml and src/main.lean, then run leanpkg configure, leanpkg build, and lean --run src/main.lean on the versions listed. Investigate the interaction between io.run_tactic, tactic.get_env, and environment.decl_filter_map. Done means the program prints the declarations and exits without SIGSEGV.
Written by the indexing model from the issue text.
Assessment
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100