From 660eb9975a2c22c01beac7a7a23ff95cf399b77d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 1 May 2024 09:06:50 +1000 Subject: [PATCH] chore: restore #4006 (#4038) --- src/library/constructions/projection.cpp | 5 +---- tests/lean/run/2575.lean | 3 +-- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index 4ba99d67bc..b9b9644744 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -99,10 +99,7 @@ environment mk_projections(environment const & env, name const & n, buffer expr proj_val = mk_proj(n, i, c); proj_val = lctx.mk_lambda(proj_args, proj_val); declaration new_d; - // TODO: replace `if (false) {` with `if (is_prop) {`. - // Mathlib is crashing when prop fields are theorems. - // The crash is in the ir_interpreter. Kyle suspects this is an use-after-free bug in the interpreter. - if (false) { // if (is_prop) { + if (is_prop) { bool unsafe = use_unsafe(env, proj_type) || use_unsafe(env, proj_val); if (unsafe) { // theorems cannot be unsafe diff --git a/tests/lean/run/2575.lean b/tests/lean/run/2575.lean index 0ab4e8b299..c6d6f947c6 100644 --- a/tests/lean/run/2575.lean +++ b/tests/lean/run/2575.lean @@ -4,9 +4,8 @@ structure AtLeastThirtySeven where theorem AtLeastThirtySeven.lt (x : AtLeastThirtySeven) : 36 < x.val := x.le --- TODO: fix /-- -info: def AtLeastThirtySeven.le : ∀ (self : AtLeastThirtySeven), 37 ≤ self.val := +info: theorem AtLeastThirtySeven.le : ∀ (self : AtLeastThirtySeven), 37 ≤ self.val := fun self => self.2 -/ #guard_msgs in