Segmentation fault when using `get_env` with `run_tactic`

[lenianiva]

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.
  • 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)
	}

2. Execute leanpkg configure; leanpkg build
3. 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 855e5b7, 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
	}

[lenianiva]

A solution I have for now is to calculate the list l while the env exists:

meta def main : io unit := do {
		l <- io.run_tactic $ do {
			e <- tactic.get_env,
			return (environment.decl_map e (fun d, "a"))
		},
		let big := string.intercalate "," l in
		io.print_ln big
	}

Maybe this is an issue related to GC?