leanprover/lean4

`And.left` and `And.right` have malformed constant info

Closed this issue · 1 comments

fgdorais commented

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Check that your issue is not already filed.
    • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

In v4.8.0-rc1, the ConstantInfo for And.left and And.right are malformed and cause lean to segfault (at least on aarch64-apple-darwin). Only the field TheoremVal.all seems affected so this is perhaps related to #4035. Also note that And.left and And.right are structure fields rather than standalone theorems.

Context

Observed after updating code to v4.8.0-rc1 when an alias foo := And.left declaration caused a server crash. Zulip mention

Steps to Reproduce

This file causes lean to segfault.

import Lean

def test : Lean.CoreM (List Lean.Name) := do
  let .thmInfo tval ← Lean.getConstInfo `And.left | unreachable!
  return tval.all

#eval test

Version: Lean (version 4.8.0-rc1, aarch64-apple-darwin, commit dcccfb73cb24, Release)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

fgdorais commented

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