Incremental compilation for classical

Stream: metaprogramming / tactics

[Paul Lezeau]

It seems like classical currently doesn't support incremental compilation - the test case I've been playing around with is

example : ∀ (n : Nat), n < 101 → n < 101 := by
  classical
    sleep 10000
    intro n hn
    apply hn

I'd like to have a go at making it incremental - would anyone have any suggestions/advice on how to get started on this?

[Sebastian Ullrich]

Unfortunately this topic is inherently tricky. I was going to tell you to take a look at focus for a similar incremental tactic but at that point I had already basically written the PR myself :) lean#6575

[Paul Lezeau]

Fair enough - thanks!