Zulip Chat Archive

Stream: general

Topic: Lean segfaulting


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Koundinya Vajjha (Apr 18 2019 at 18:13):

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

view this post on Zulip Mario Carneiro (Apr 18 2019 at 18:19):

no, there is a bug in your code

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Apr 18 2019 at 18:26):

I'll have a look

view this post on Zulip Mario Carneiro (Apr 18 2019 at 18:26):

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

view this post on Zulip Simon Hudon (Apr 18 2019 at 20:42):

I think I have a fix

view this post on Zulip Simon Hudon (Apr 18 2019 at 21:41):

@Mario Carneiro can you review and merge please?

view this post on Zulip 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',

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Jun 13 2019 at 18:36):

This happens in 3.5.0c too though.

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Jun 13 2019 at 18:38):

That's the most recent nightly.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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