-
Notifications
You must be signed in to change notification settings - Fork 718
Open
Labels
kind: bugAn error, flaw, fault or unintended behaviour.An error, flaw, fault or unintended behaviour.needs: triageThe validity of this issue needs to be checked, or the issue itself updated.The validity of this issue needs to be checked, or the issue itself updated.
Description
Description of the problem
I am using Coq and Rocq on a Windows laptop (Windows 11). I've been having trouble with CoqIDE and RocqIDE crashing a lot, similar to this bug report which was closed but not really resolved. I realized that the issue seemed to be exacerbated by the "Find" or "Search" functionality (i.e. what appears when you hit Ctrl-F, not the "Search" command in the code). And indeed, this seems to be the root cause.
After some testing, I realized that the bug is extremely reproducible: open any .v file, open up the "Find" window, put anything in the search box (e.g. even a single character), and click "Next" exactly 61 times. Every time, on the 61st click, RocqIDE freezes up and needs to be shut down and restarted.
Small Rocq / Coq file to reproduce the bug
Version of Rocq / Coq where this bug occurs
9.0.1, 8.20.1
Interface of Rocq / Coq where this bug occurs
RocqIDE, CoqIDE
Last version of Rocq / Coq where the bug did not occur
No response
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
kind: bugAn error, flaw, fault or unintended behaviour.An error, flaw, fault or unintended behaviour.needs: triageThe validity of this issue needs to be checked, or the issue itself updated.The validity of this issue needs to be checked, or the issue itself updated.