leanprover-community / leanprover-community/lean

Segmentation fault when using `get_env` with `run_tactic`

Open
#803 1 comment 0 reactions 0 assignees View on GitHub

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.
    • Reduced the issue to a self-contained, reproducible test case.
Description

When iterating through declarations in an environment env obtained from io.run_tactic (tactic.get_env), lean crashes.

Steps to Reproduce
  1. 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)
	}
  1. Execute leanpkg configure; leanpkg build
  2. 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

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.