Zulip Chat Archive

Stream: general

Topic: crashes


Patrick Massot (Jun 24 2020 at 14:44):

It seems to me that Lean is crashing a lot since a couple of weeks, whereas this never happened before. I see stuff like: image.png

Gabriel Ebner (Jun 24 2020 at 15:05):

I've also noticed this. :sad: It would be extremely helpful if you could somewhat reliably reproduce it.

Patrick Massot (Jun 24 2020 at 15:15):

Of course I understand that, but it's hard to predict and reproduce.

Bhavik Mehta (Jun 24 2020 at 15:26):

Also noticed this

Alistair Tucker (Jun 30 2020 at 23:42):

I don't think I've seen Lean crash out before, but I've just upgraded from 3.7.2 to 3.16.5 and now this example will do it:

import data.real.basic

def β (T : ) : Type :=   
instance (T : ) : has_zero (β T) := ⟨λ t, 0
instance (T : ) : partial_order (β T) := by { unfold β, apply_instance, }

lemma v_nonneg {T : } (v : β T) : 0  v := sorry
example {T : } (t : ) (v : β T) : 0  v t := by apply v_nonneg

That's probably not quite minimal yet, but I've made it much shorter than it was originally!

Bhavik Mehta (Jun 30 2020 at 23:46):

Yup this gives a crash for me too

Patrick Massot (Jul 01 2020 at 00:13):

Same here. Big thanks to Alistair for managing to get a reproducible crash that nobody else could forge! Hopefully this will allow some expert (ie. Gabriel) to fix it.

Alex J. Best (Jul 01 2020 at 00:26):

It seems using

example {T : } (q : ) (v : β T) : 0  v q := by apply @v_nonneg T

instead doesn't crash lean.

Bryan Gin-ge Chen (Jul 01 2020 at 00:29):

It seems Alistair's code doesn't crash in Lean 3.10.0c (and older) and does crash starting with 3.11.0c.

Bryan Gin-ge Chen (Jul 01 2020 at 00:30):

So lean#211 is looking pretty suspicious right now.

Bryan Gin-ge Chen (Jul 01 2020 at 00:30):

Uh oh, it was one of my PRs. :sweat:

Johan Commelin (Jul 01 2020 at 00:31):

And it was one of the speedup PRs

Johan Commelin (Jul 01 2020 at 00:31):

I think

Bryan Gin-ge Chen (Jul 01 2020 at 00:41):

Here's the first part of the lldb backtrace for the crash from Alistair's file (in 3.16.5c):

* thread #3, stop reason = EXC_BAD_ACCESS (code=1, address=0x267df1db)
  * frame #0: 0x00000001000814da lean`lean::instantiate(lean::expr const&, unsigned int, unsigned int, lean::expr const*) + 42
    frame #1: 0x0000000100081898 lean`lean::instantiate(lean::expr const&, lean::expr const&) + 24
    frame #2: 0x000000010026e87b lean`lean::apply(lean::type_context_old&, lean::expr, lean::apply_cfg const&, lean::tactic_state const&, lean::vm_obj*, lean::vm_obj*) + 1355
    frame #3: 0x000000010026fa2b lean`lean::tactic_apply_core(lean::vm_obj const&, lean::vm_obj const&, lean::vm_obj const&) + 283
    frame #4: 0x000000010049a5dd lean`lean::vm_state::invoke_fn(void*, unsigned int) + 2317
    frame #5: 0x000000010049df8e lean`lean::vm_state::invoke_cfun(lean::vm_decl const&) + 254
    frame #6: 0x000000010049cb01 lean`lean::vm_state::run() + 4561

Bryan Gin-ge Chen (Jul 01 2020 at 00:42):

So I guess Lean is crashing somewhere in here.

Alex J. Best (Jul 01 2020 at 00:46):

Reverting the change from the commit @Bryan Gin-ge Chen mentioned to lean/src/library/type_context.h (but only that file), fixes this for me.

Alex J. Best (Jul 01 2020 at 00:47):

Actually strictly speaking I didn't revert the change, I changed the Semireducible on line 787 to All

Bryan Gin-ge Chen (Jul 01 2020 at 00:50):

Is tests/lean/run/mario_type_context.lean slow or fast with your change?

Bryan Gin-ge Chen (Jul 01 2020 at 00:50):

Oh, I guess it will fail if it's going to be slow.

Alex J. Best (Jul 01 2020 at 00:51):

I didn't run the testsuite yet ;)

Alex J. Best (Jul 01 2020 at 00:51):

🐌 elan run my_link lean run/mario_type_context.lean
parsing took 0.0398ms
elaboration of bar took 0.0157ms
type checking of bar took 0.0161ms
/Users/alex/lean/tests/lean/run/mario_type_context.lean:17:0: warning: declaration 'bar' uses sorry
compilation of bar took 0.266ms
decl post-processing of bar took 0.323ms
parsing took 3.59ms
type checking of foo took 0.0562ms
compilation of foo took 0.002ms
decl post-processing of foo took 0.00186ms
elaboration: tactic compilation took 40.3ms
[bar α = bar α, bar α = bar α, eq.refl (bar α = bar α), h]
elaboration: tactic execution took 1ms
num. allocated objects:  67
num. allocated closures: 190
    1ms   100.0%   trace_fmt
    1ms   100.0%   tactic.trace
    1ms   100.0%   _interaction._lambda_3
    1ms   100.0%   scope_trace
    1ms   100.0%   _interaction._lambda_2
    1ms   100.0%   tactic.istep._lambda_1
    1ms   100.0%   tactic.istep
    1ms   100.0%   tactic.step
    1ms   100.0%   _interaction
elaboration of foo took 74.6ms
/Users/alex/lean/tests/lean/run/mario_type_context.lean:19:0: warning: declaration 'foo' uses sorry
cumulative profiling times:
    compilation 0.267ms
    decl post-processing 0.321ms
    elaboration 74.6ms
    elaboration: tactic compilation 40.3ms
    elaboration: tactic execution 1ms
    parsing 3.62ms
    type checking 0.0711ms

Alex J. Best (Jul 01 2020 at 00:52):

Seems pretty quick to me?

Alex J. Best (Jul 01 2020 at 00:53):

Which version should mario be slow under?

Bryan Gin-ge Chen (Jul 01 2020 at 00:54):

It should be slow / fail in 3.10.0c and before.

Alex J. Best (Jul 01 2020 at 00:54):

Hmm doesn't seem to fail under 3.9.0 to me.

Bryan Gin-ge Chen (Jul 01 2020 at 00:56):

Weird, I see this in 3.9.0c:

try_for tactic failed, timeout
state:
α : Type u_1,
_inst_1 : comm_ring α,
h : bar α = bar α
 true

Bryan Gin-ge Chen (Jul 01 2020 at 00:57):

At the do.

Alex J. Best (Jul 01 2020 at 00:57):

Looks like mine is picking up mathlib defs, maybe thats a problem

Bryan Gin-ge Chen (Jul 01 2020 at 00:58):

That's really weird. There aren't any imports in that file.

ROCKY KAMEN-RUBIO (Jul 01 2020 at 01:00):

Patrick Massot said:

It seems to me that Lean is crashing a lot since a couple of weeks, whereas this never happened before. I see stuff like: image.png

I've been running into this error as well. I assumed it was my old computer running out of RAM, but clearer more space didn't fix it. I'll see if I can reproduce it with my own code.

Alistair Tucker said:

I don't think I've seen Lean crash out before, but I've just upgraded from 3.7.2 to 3.16.5 and now this example will do it:

import data.real.basic

def β (T : ) : Type :=   
instance (T : ) : has_zero (β T) := ⟨λ t, 0
instance (T : ) : partial_order (β T) := by { unfold β, apply_instance, }

lemma v_nonneg {T : } (v : β T) : 0  v := sorry
example {T : } (t : ) (v : β T) : 0  v t := by apply v_nonneg

That's probably not quite minimal yet, but I've made it much shorter than it was originally!

This also crashed for me.

Bryan Gin-ge Chen (Jul 01 2020 at 01:18):

I've created an issue at lean#372.

Bryan Gin-ge Chen (Jul 01 2020 at 01:38):

@Alex J. Best Ah, I get what you mean about the test now. I forgot that it got modified when Johan removed most of algebra from core.

Alex J. Best (Jul 01 2020 at 01:40):

@Bryan Gin-ge Chen yeah I figured that was most likely what had happened but didn't check the commit history, thanks for confirming!

Gabriel Ebner (Jul 01 2020 at 07:04):

Thanks for finding a reproducible testcase! If one of you could make a #mwe (i.e., not referencing mathlib), then I could also include it in the test suite.

Gabriel Ebner (Jul 01 2020 at 07:41):

Guys, I'll fix the segfault for you. But please define your instances correctly. The fix is to add a single letter:

instance (T : ) : partial_order (β T) := by { dunfold β, apply_instance, }

Johan Commelin (Jul 01 2020 at 07:43):

delta instead of dunfold would/should also work, right?

Gabriel Ebner (Jul 01 2020 at 07:43):

Fun fact: with semireducible transparency, Lean can reduce @β.partial_order x but not @β.partial_order ?m_1. The second reduces to eq.mpr ..., but no further.

Gabriel Ebner (Jul 01 2020 at 07:44):

The no id or eq.mpr rule in instances almost requires a linter.

Yury G. Kudryashov (Jul 01 2020 at 07:46):

In data fields of instances.

Gabriel Ebner (Jul 01 2020 at 07:49):

Also not directly at the top, like here.

Gabriel Ebner (Jul 01 2020 at 07:59):

Minimized:

def foo (n : ) := Type
def beta (n : ) : foo n :=
by unfold foo; exact   
lemma baz (n : ) : beta n := id
example :  := by apply baz

Gabriel Ebner (Jul 01 2020 at 08:04):

lean#373

Patrick Massot (Jul 01 2020 at 08:25):

Thanks Gabriel! I really hope this is the sources of the crashes we've been seeing for a couple of weeks.

Bryan Gin-ge Chen (Jul 01 2020 at 08:33):

Has the recent instability always involved apply? This crash now seems like a specific bug in that tactic.

Grayson Burton (Aug 12 2020 at 23:12):

This makes Lean segfault on Windows (both Lean itself and the language server)

inductive convex_hull : set α
| intrv (v₁  convex_hull) : convex_hull v₁

@Bhavik Mehta got unreachable code was reached but Lean kept working for them apparently

Bhavik Mehta (Aug 12 2020 at 23:12):

Oh - this version gives me a SIGSEGV error!

Bhavik Mehta (Aug 12 2020 at 23:13):

The slightly older version you had gave me the unreachable code error and lean didn't crash

Grayson Burton (Aug 12 2020 at 23:14):

the older version, for reference:

inductive convex_hull (s : set α) : set α
| of_set :  v  s, convex_hull v
| intrv (v₁ v₂  convex_hull) : convex_hull v₁

Bhavik Mehta (Aug 12 2020 at 23:15):

did you put variables {α : Type*} at the top when you tried it? I did in both cases

Grayson Burton (Aug 12 2020 at 23:15):

Nope. The entire file was each respective snippet every time I tested.

Alex J. Best (Aug 12 2020 at 23:16):

I get random segfaults with and without defining alpha, and a lot of unreachable codes

Rob Lewis (Aug 13 2020 at 07:45):

Please open an issue at leanprover-community/lean!

Grayson Burton (Aug 13 2020 at 08:48):

https://github.com/leanprover-community/lean/issues/438 Got distracted, finally made it :)


Last updated: Dec 20 2023 at 11:08 UTC