Closed fgdorais closed 1 week ago
This is perhaps limited to declarations in Init.Prelude. The following does not cause a segfault:
import Lean
structure Both (p q : Prop) : Prop where
fst : p
snd : q
def test : Lean.CoreM (List Lean.Name) := do
let .thmInfo tval ← Lean.getConstInfo `Both.fst | unreachable!
return tval.all
#eval test
Prerequisites
Description
In
v4.8.0-rc1
, theConstantInfo
forAnd.left
andAnd.right
are malformed and cause lean to segfault (at least onaarch64-apple-darwin
). Only the fieldTheoremVal.all
seems affected so this is perhaps related to #4035. Also note thatAnd.left
andAnd.right
are structure fields rather than standalone theorems.Context
Observed after updating code to
v4.8.0-rc1
when analias foo := And.left
declaration caused a server crash. Zulip mentionSteps to Reproduce
This file causes lean to segfault.
Version:
Lean (version 4.8.0-rc1, aarch64-apple-darwin, commit dcccfb73cb24, Release)
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.