## Stream: general

### Topic: Lean segfaulting

#### Koundinya Vajjha (Apr 18 2019 at 18:06):

I just came across this and I am unsure of why this causes the Lean server to segfault on my machine:
I am writing a tactic to revert all propositions in a theorem.

open tactic

meta def revert_props : tactic unit :=
do ctx ← local_context,
lst ← mmap infer_type ctx,
foo ← mfilter is_prop lst,
g ← mmap revert foo,
skip

example (b c d e f : Prop) (h₁ : b ∧ c) (h₂ : d → e) (g : Prop) (h₃ : b ∧ f → g) :
true :=
begin
-- revert_props, -- causes a segfault
guard_target (b ∧ f → g) → (d → e) → b ∧ c → true,
intros,
trivial
end


I am concerned if mmap revert foo is the right way to do what I had in mind.

#### Mario Carneiro (Apr 18 2019 at 18:12):

I recall revert having a bug in it that causes a segfault, although I thought it was fixed

#### Koundinya Vajjha (Apr 18 2019 at 18:13):

Does this mean I can skip Q1 for tomorrow's ITP homework?

#### Mario Carneiro (Apr 18 2019 at 18:19):

no, there is a bug in your code

#### Mario Carneiro (Apr 18 2019 at 18:20):

the bug in lean is that it segfaults instead of just failing the tactic, but you called revert wrong

#### Mario Carneiro (Apr 18 2019 at 18:24):

@Simon Hudon Here's a MWE:

example (a b : Prop) : true :=
by do to_expr (a ∧ b) >>= revert


It looks like local_context::find_local_decl asserts that the input is a local constant rather than returning none like you might expect

I'll have a look

#### Mario Carneiro (Apr 18 2019 at 18:26):

maybe revert() in revert_tactic.cpp should have a check in the for loop

#### Simon Hudon (Apr 18 2019 at 20:42):

I think I have a fix

#### Simon Hudon (Apr 18 2019 at 21:41):

@Mario Carneiro can you review and merge please?

#### Wojciech Nawrocki (Jun 13 2019 at 16:35):

Just ran into this in Lean community edition nightly. A consistent repro - start with this in an empty file:

lemma segfault {α: Type u} {a a': α} (H : a = a') : a = a' := begin
revert a,
end


then change revert a, to revert a a',

#### Bryan Gin-ge Chen (Jun 13 2019 at 17:16):

I can reproduce this with 3.4.2 . It seems that it occurs the instant the file reads revert a a. If I paste a' instead of typing it then no crash occurs. Similarly, I can easily type in revert a' a (though changing it to revert a' a' crashes).

Curiously, I can't reproduce any of these crashes in the web editor. (This version uses community Lean).

#### Mario Carneiro (Jun 13 2019 at 18:33):

there is a bug in revert_lst in 3.4.2; this is fixed in community lean

#### Bryan Gin-ge Chen (Jun 13 2019 at 18:36):

This happens in 3.5.0c too though.

#### Wojciech Nawrocki (Jun 13 2019 at 18:37):

Yup, I can reproduce this on nightly-2019-05-17`. Maybe it's fixed in newer nightlies?

#### Bryan Gin-ge Chen (Jun 13 2019 at 18:38):

That's the most recent nightly.

#### Koundinya Vajjha (Jun 13 2019 at 19:18):

This has a separate instance where Lean segfaults.Is this fixed in community?
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20crashing

#### Bryan Gin-ge Chen (Jun 13 2019 at 19:18):

No, I don't think anyone has looked at it yet.

Edit: I opened an issue for this.

#### Bryan Gin-ge Chen (Jun 13 2019 at 19:21):

In particular, the version of 3.5.0c I used in my last comment in that thread was also the most recent nightly.

Last updated: May 13 2021 at 19:20 UTC