Zulip Chat Archive

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

Simon Hudon (Apr 18 2019 at 18:26):

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: Dec 20 2023 at 11:08 UTC