crashes

Stream: general

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Bhavik Mehta]

Also noticed this

[Alistair Tucker]

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]

Yup this gives a crash for me too

[Patrick Massot]

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]

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]

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]

So lean#211 is looking pretty suspicious right now.

[Bryan Gin-ge Chen]

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

[Johan Commelin]

And it was one of the speedup PRs

[Johan Commelin]

I think

[Bryan Gin-ge Chen]

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]

So I guess Lean is crashing somewhere in here.

[Alex J. Best]

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]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Alex J. Best]

I didn't run the testsuite yet ;)

[Alex J. Best]

🐌 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]

Seems pretty quick to me?

[Alex J. Best]

Which version should mario be slow under?

[Bryan Gin-ge Chen]

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

[Alex J. Best]

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

[Bryan Gin-ge Chen]

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]

At the do.

[Alex J. Best]

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

[Bryan Gin-ge Chen]

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

[ROCKY KAMEN-RUBIO]

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]

I've created an issue at lean#372.

[Bryan Gin-ge Chen]

@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]

@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]

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]

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]

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

[Gabriel Ebner]

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]

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

[Yury G. Kudryashov]

In data fields of instances.

[Gabriel Ebner]

Also not directly at the top, like here.

[Gabriel Ebner]

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]

lean#373

[Patrick Massot]

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]

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

[Grayson Burton]

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]

Oh - this version gives me a SIGSEGV error!

[Bhavik Mehta]

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

[Grayson Burton]

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]

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

[Grayson Burton]

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

[Alex J. Best]

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

[Rob Lewis]

Please open an issue at leanprover-community/lean!

[Grayson Burton]

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