simpl tactic isn't interrupted properly

[HazardousPeach]

Describe the bug

For large or complex contexts, the simpl command can hang for a long time (indefinitely?) and isn't interruptible from coq-lsp.

To Reproduce
Since this requires complex contexts to reproduce, we'll reproduce it using CompCert.
Steps to reproduce the behavior:

1. Clone CompCert: git clone [email protected]:AbsInt/CompCert.git
2. Start the coq-lsp binary.
3. Send the initialize message, with the rootUri, rootPath, and workspace uri pointing to the toplevel of your CompCert clone.
4. Send the initalized message.
5. Send a openDoc message with an empty document.
6. Send a didChange message with the following document:

Require Import Coqlib.\nRequire Import Integers.\nRequire Import Values Memory.\nRequire Import Cminor CminorSel.\nRequire Import SelectOp.\nSection CMCONSTR.\nVariable ge: genv.\nVariable sp: val.\nVariable e: env.\nVariable m: mem.\nDefini tion unary_constructor_sound (cstr: expr -> expr) (sem: val -> val) : Prop :=\n  forall le a x,\n  eval_expr ge sp e m le a x ->\n  exists v, eval_expr ge sp e m le (cstr a) v /\\ Val.lessdef (sem x) v.\nLemma eval_mulimm_base:\n  forall n, unary_constructor_sound (mulimm_base n) (fun x => Val.mul x (Vint n)).\ninducti on n.\neconstructor.\nunfold mulimm_base.\nunfold Int.one_bits.\nunfold map.\nsimpl.

7. Wait a bit, noticing that the doc fails to finish checking.
8. Send another didChange message with the following document:

Require Import Coqlib.\nRequire Import Integers.\nRequire Import Values Memory.\nRequire Import Cminor CminorSel.\nRequire Import SelectOp.\nSection CMCONSTR.\nVariable ge: genv.\nVariable sp: val.\nVariable e: env.\nVariable m: mem.\nDefini tion unary_constructor_sound (cstr: expr -> expr) (sem: val -> val) : Prop :=\n  forall le a x,\n  eval_expr ge sp e m le a x ->\n  exists v, eval_expr ge sp e m le (cstr a) v /\\ Val.lessdef (sem x) v.\nLemma eval_mulimm_base:\n  forall n, unary_constructor_sound (mulimm_base n) (fun x => Val.mul x (Vint n)).\ninducti on n.\neconstructor.\nunfold mulimm_base.\nunfold Int.one_bits.\nunfold map.\nidtac.

(this is just replacing the final failing tactic with "idtac".

Expected behavior

coq-lsp should interrupt the original didChange request and respond to the new one.
This expected behavior is described by Emilio here: https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp/topic/Interrupting.20coq-lsp/near/350040107

Desktop:

• Arch Linux
• coq-lsp v8.16-git

[Blaisorblade]

(Just for the record, the underlying slow performance is a blow-up in the Coq computation: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Super-slow.2Fdiverging.20.60simpl.60.20without.20debug.20output).

[ejgallego]

Thanks a lot for this case folks, I have a fix ready, I'm wondering if we could produce a simpler test case to put in coq-lsp test suite that doesn't require pulling so many CompCert files?

[Alizter]

I think writing down a rose-tree and then a stupidly big term would create this effect with simpl.

[ejgallego]

I have tested this example with current main and I cannot reproduce anymore.