Incremental elaboration of calc tactic

Stream: lean4

[Jad Ghalayini]

I am working on a large proof development to formalize refinement of programs in SSA. A lot of my proofs consist of relatively large (~500 lines) calc blocks, which take a very long time to update when I make small incremental changes. Even with liberal use of stop and commenting out steps, I still often need to wait up to 10 seconds every change. I've heard that a few versions ago some tactic elaboration became incremental; is there any chance calc could make use of this feature somehow?

[Sebastian Ullrich]

There is a chance. Could you please open an issue?