I am having regular freezes/crashes of VsCoq on one of my files, to the point where it becomes difficult to develop it. I’m really not sure what the problem is (nor if this is really a VsCoq problem), but calling
coqc from the terminal on the same file does not seem to trigger the same issue.
The faulty file is the following : https://github.com/MevenBertrand/metacoq/blob/case-representation-bidir/pcuic/theories/bidirectional/BDStrengthening.v . The problem triggers when I step directly to an advanced point in the file. VsCoq seems to choke on some uses of
lia, and either crashes or freezes my computer to the point where I have to kill the process to regain control – in some cases the only way to do this is to shut down. This does not trigger when working on other files (for instance the ones in the same folder) that I would say have similar lengths and features (including uses of
lia). Also, stepping down slowly through the file seems to mitigate the error, although it is not always enough.
Does this ring a bell to anyone? How could I debug this to at least pinpoint what is responsible for the problem and report a meaningful issue?
I don't see anything unusual except maybe the many
Last updated: Jan 30 2023 at 19:04 UTC