language server crash when editing

Stream: general

[fonqL]

vscode: 1.84.2
Lean: 4.9.0
mwe:

@[specialize]
unsafe def map {m : Type v → Type w} [Monad m] (f : α → m β) (sz i : USize) (r : Array NonScalar) : m (Array PNonScalar) := do
  if i < sz then
    let v    := r.uget i lcProof
    let r    := r.uset i default lcProof
    let vNew ← f (unsafeCast v)         -- edit `v` in this line
    map f sz (i+1) (r.uset i (unsafeCast vNew) lcProof)
  else
    pure (unsafeCast r)


@[inline]
unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) :=
  let sz := USize.ofNat as.size
  unsafeCast <| map f sz 0 (unsafeCast as)

unsafe def f (arr: Array (IO Nat)) := mapMUnsafe id arr

Steps to reproduce:

1. Copy to vscode or online editor https://live.lean-lang.org
2. Edit the v variable in the comment line above:
   1. Put the cursor behind v, and press Backspace to delete v.
   2. Press (, and vscode auto insert the right bracket ).
3. Server has crashed. Continue to input a v (now the expression is (v)) or undo cannot make server work well again. The file or server must be restarted.

Note that if I remove one of the attributes or last two definitions, there's no problem.

[Kevin Buzzard]

Also crashes on 4.10.0-rc1. I interpreted the instructions as "put the cursor to the left of the v, and then press the "Delete" button on my keyboard (which deletes the character to the right of the cursor)", but it also crashes if I put my cursor to the right of the v and press the "Backspace" button (which deletes the character to the left of the cursor).

[Kim Morrison]

Please open an issue!

[Kim Morrison]

(@Marc Huisinga)

[Marc Huisinga]

I don't think this is a language server issue. lake build also crashes with error code 139 on the input with brackets and gdb produces the following stacktrace when the language server crashes:

0x00007f8d62c38d90 in lean_inc_ref_cold () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
(gdb) bt
#0  0x00007f8d62c38d90 in lean_inc_ref_cold () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#1  0x00007f8d62b3a181 in lean::lift_loose_bvars(lean::expr const&, unsigned int, unsigned int) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#2  0x00007f8d62b3a1dd in lean::lift_loose_bvars(lean::expr const&, unsigned int) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#3  0x00007f8d62b40ec4 in std::__1::__function::__func<lean::instantiate_rev(lean::expr const&, unsigned int, lean::expr const*)::$_1, std::__1::allocator<lean::instantiate_rev(lean::expr const&, unsigned int, lean::expr const*)::$_1>, lean::optional<lean::expr> (lean::expr const&, unsigned int)>::operator()(lean::expr const&, unsigned int&&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#4  0x00007f8d62b3d947 in lean::replace_rec_fn::apply(lean::expr const&, unsigned int) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#5  0x00007f8d62b3db09 in lean::replace_rec_fn::apply(lean::expr const&, unsigned int) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#6  0x00007f8d62b3d6a0 in lean::replace(lean::expr const&, std::__1::function<lean::optional<lean::expr> (lean::expr const&, unsigned int)> const&, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#7  0x00007f8d62b3f510 in lean::instantiate_rev(lean::expr const&, unsigned int, lean::expr const*) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#8  0x00007f8d62bc58ec in lean::csimp_fn::beta_reduce(lean::expr, unsigned int, lean::expr const*, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#9  0x00007f8d62bca691 in lean::csimp_fn::reduce_cases_cnstr(lean::buffer<lean::expr, 16ul> const&, lean::inductive_val const&, lean::expr const&, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#10 0x00007f8d62bc64ba in lean::csimp_fn::visit_cases(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#11 0x00007f8d62bc2ff2 in lean::csimp_fn::visit_app(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#12 0x00007f8d62bc01b2 in lean::csimp_fn::visit(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#13 0x00007f8d62bc2bb5 in lean::csimp_fn::visit_let(lean::expr) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#14 0x00007f8d62bc014f in lean::csimp_fn::visit(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#15 0x00007f8d62bc5a11 in lean::csimp_fn::beta_reduce_cont(lean::expr, unsigned int, unsigned int, lean::expr const*, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#16 0x00007f8d62bc594f in lean::csimp_fn::beta_reduce(lean::expr, unsigned int, lean::expr const*, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#17 0x00007f8d62bc5754 in lean::csimp_fn::beta_reduce(lean::expr, lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#18 0x00007f8d62bc9a22 in lean::csimp_fn::try_inline(lean::expr const&, lean::expr const&, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#19 0x00007f8d62bc3452 in lean::csimp_fn::visit_app(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#20 0x00007f8d62bc8ef9 in lean::csimp_fn::merge_app_app(lean::expr const&, lean::expr const&, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#21 0x00007f8d62bc31a7 in lean::csimp_fn::visit_app(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#22 0x00007f8d62bc01b2 in lean::csimp_fn::visit(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#23 0x00007f8d62bccb1a in lean::csimp_fn::apply_at(lean::expr const&, lean::expr const&, lean::expr const&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#24 0x00007f8d62bc7b9f in lean::csimp_fn::float_cases_on_core(lean::expr const&, lean::expr const&, lean::expr const&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#25 0x00007f8d62bc30fa in lean::csimp_fn::visit_app(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#26 0x00007f8d62bc01b2 in lean::csimp_fn::visit(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#27 0x00007f8d62bc5bf0 in lean::csimp_fn::beta_reduce_cont(lean::expr, unsigned int, unsigned int, lean::expr const*, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#28 0x00007f8d62bc594f in lean::csimp_fn::beta_reduce(lean::expr, unsigned int, lean::expr const*, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#29 0x00007f8d62bc5754 in lean::csimp_fn::beta_reduce(lean::expr, lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#30 0x00007f8d62bc3085 in lean::csimp_fn::visit_app(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#31 0x00007f8d62bc01b2 in lean::csimp_fn::visit(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#32 0x00007f8d62bc2bb5 in lean::csimp_fn::visit_let(lean::expr) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#33 0x00007f8d62bc014f in lean::csimp_fn::visit(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#34 0x00007f8d62bbf4b8 in lean::csimp_fn::visit_lambda(lean::expr, bool, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#35 0x00007f8d62bbe788 in lean::csimp_fn::operator()(lean::expr const&) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#36 0x00007f8d62bbe11d in lean::csimp_core(lean::environment const&, lean::local_ctx const&, lean::expr const&, bool, lean::csimp_cfg const&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#37 0x00007f8d62bf7ed3 in lean::specialize_fn::mk_new_decl(lean::pair_ref<lean::name, lean::expr> const&, lean::buffer<lean::expr, 16ul> const&, lean::buffer<lean::expr, 16ul> const&, lean::specialize_fn::spec_ctx&) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#38 0x00007f8d62bf0d40 in lean::specialize_fn::specialize(lean::expr const&, lean::buffer<lean::expr, 16ul> const&, lean::specialize_fn::spec_ctx&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#39 0x00007f8d62bef53a in lean::specialize_fn::visit_app(lean::expr const&) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#40 0x00007f8d62bef175 in lean::specialize_fn::visit(lean::expr const&) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#41 0x00007f8d62befe21 in lean::specialize_fn::visit_let(lean::expr) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#42 0x00007f8d62bef1e8 in lean::specialize_fn::visit(lean::expr const&) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#43 0x00007f8d62befa0f in lean::specialize_fn::visit_lambda(lean::expr) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#44 0x00007f8d62bef1a6 in lean::specialize_fn::visit(lean::expr const&) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#45 0x00007f8d62bee86f in lean::specialize_fn::operator()(lean::pair_ref<lean::name, lean::expr> const&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#46 0x00007f8d62bedc0e in lean::specialize(lean::environment, lean::list_ref<lean::pair_ref<lean::name, lean::expr> > const&, lean::csimp_cfg const&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#47 0x00007f8d62ba4558 in lean::compile(lean::environment const&, lean::options const&, lean::list_ref<lean::name>) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so

[Kim Morrison]

@fonqL, would you be able to open an issue for this? Given Marc's investigation, it would be best to describe what happens when you run lean on this file, leaving out live.lean-lang.org and the editing instructions.

[fonqL]

Sorry for my late reply.
4703

[Kim Morrison]

No worries, thanks very much for reporting!