rcases is slow

Stream: general

[Kenny Lau]

The tactic rcases seems to be slow to parse:

-- parsing took 2.05s
-- elaboration of test_rcases took 140ms
set_option profiler true
theorem test_rcases (h : ∀ n : ℕ, ∃ m : ℕ, m = n) : true :=
begin
  rcases (h 0) with ⟨n, hn⟩,
  rcases (h 0) with ⟨n, hn⟩,
  rcases (h 0) with ⟨n, hn⟩,
  rcases (h 0) with ⟨n, hn⟩,
  rcases (h 0) with ⟨n, hn⟩,
  rcases (h 0) with ⟨n, hn⟩,
  rcases (h 0) with ⟨n, hn⟩,
  rcases (h 0) with ⟨n, hn⟩,
  rcases (h 0) with ⟨n, hn⟩,
  rcases (h 0) with ⟨n, hn⟩,
  trivial
end

[Kenny Lau]

The elaboration speed seems to be normal relative to my computer

[Mario Carneiro]

that's no surprise, the rcases parser is the most complex tactic parser I'm aware of

[Mario Carneiro]

I think the general lesson is that the interactive tactic parser could use some optimization

[Kenny Lau]

I don't think it was that slow in Lean 3.4

[Mario Carneiro]

can you test it e.g. with elan?